Encyclopedia Physics Physics Recognition Hamiltonian Spectrum

ARTICLE 4 claims 4 theorems

Physics Recognition Hamiltonian Spectrum

A machine-checked library shows how a forced cost function arranges physical states into five energy bands.

The spectrum's shape

In quantum physics, a Hamiltonian is the operator that gives the energy levels of a system. Its spectrum is the list of those levels. Recognition Science builds a Hamiltonian from its cost function J, and the spectrum of that Hamiltonian turns out to have a simple, fixed shape: one ground state at zero energy and four families of excited states above it.

The cost function J(r) = (r + 1/r)/2 - 1 measures the recognition cost of a ratio r between two states. At r = 1 the cost is zero, which is the vacuum. For any other positive r the cost is strictly positive, so every excited state sits above the ground state. The gap between the vacuum and the lowest excited state is the spectral gap, the energy you must supply to create any particle at all.

On a continuous line of ratios the gap shrinks to zero, because you can approach r = 1 arbitrarily closely. The framework's library proves that on a discrete lattice with spacing a, the gap is strictly positive: there is a real energy cost to the smallest step away from the vacuum. That is the structural claim behind a mass gap, the same kind of gap that Yang-Mills theory requires.

The five sectors are named by what they describe: vacuum, goldstone, massive scalar, massive vector, and massive tensor. The library proves there are exactly five of them, by enumeration, and packages the whole set into a single certificate object that carries the five-sector count, the zero vacuum cost, the positive excited costs, and the lattice gap all at once.

In Recognition Science, the framework models the five sectors as the complete menu of particle types that a recognition ledger can host. The certificate is the formal statement that this menu is closed: no sixth sector appears, and the gap that separates the vacuum from everything else is real on any discrete grid.

THEOREM vacuum_jcost · IndisputableMonolith/Physics/RecognitionHamiltonianSpectrum.lean
/-- Vacuum sector: J = 0. -/
theorem vacuum_jcost : Jcost 1 = 0 := Jcost_unit0
THEOREM excited_jcost · IndisputableMonolith/Physics/RecognitionHamiltonianSpectrum.lean
/-- Excited sectors: J > 0. -/
theorem excited_jcost {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
THEOREM lattice_gap_witness · IndisputableMonolith/Physics/RecognitionHamiltonianSpectrum.lean
theorem lattice_gap_witness (a : ℝ) (ha : 0 < a) : latticeSpacingGap a ha := by
  unfold latticeSpacingGap
  refine ⟨Jcost (1 + a) / 2, ?_, ?_⟩
  · apply div_pos
    · exact Jcost_pos_of_ne_one _ (by linarith) (by linarith)
    · norm_num
  · linarith [Jcost_pos_of_ne_one (1 + a) (by linarith) (by linarith)]
THEOREM spectralSectorCount · IndisputableMonolith/Physics/RecognitionHamiltonianSpectrum.lean
theorem spectralSectorCount : Fintype.card SpectralSector = 5 := by decide

What this page does not claim

Not a proof that the Yang-Mills mass gap exists in conventional physics. Not a derivation of the numerical value of any particle mass from this spectrum alone. Not a claim that the five sectors are the only possible sectors in any Hamiltonian, only in this recognition-based one.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/RecognitionHamiltonianSpectrum.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND