Explain the theorem excited_jcost from IndisputableMonolith.Physics.RecognitionHamiltonianSpectrum.

permalink: https://pith.science/recognition/ask/explain-the-theorem-excited-jcost-from-indisputablemonolith-ade6af41 · first asked 2026-05-30 · browse all asks

confidence: high in recognition cached

The theorem excited_jcost in module IndisputableMonolith.Physics.RecognitionHamiltonianSpectrum states:

 theorem excited_jcost {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
     0 < Jcost r := Jcost_pos_of_ne_one r hr hne

This asserts that the recognition cost function Jcost is strictly positive for every positive real ratio r distinct from unity. In the Recognition Hamiltonian Spectrum, the vacuum sector is defined by Jcost 1 = 0 (see vacuum_jcost). The excited_jcost theorem therefore separates all excited sectors (J > 0) from the ground state. The module packages this into HamiltonianSpectrumCert, whose excited field is exactly the universal quantification given by excited_jcost. The same positivity is reused to witness a positive spectral gap on any discretized lattice with spacing a > 0 (see lattice_gap_witness). The five-sector decomposition (vacuum, goldstone, massiveScalar, massiveVector, massiveTensor) follows independently from spectralSectorCount.

cited recognition theorems

RecognitionHamiltonianSpectrum.excited_jcost The theorem whose statement and proof obligation are to be explained.
RecognitionHamiltonianSpectrum.vacuum_jcost Provides the contrasting vacuum case Jcost 1 = 0 used to interpret excited sectors.
RecognitionHamiltonianSpectrum.spectralSectorCount Establishes the five canonical sectors in which the excited_jcost positivity applies.
RecognitionHamiltonianSpectrum.lattice_gap_witness Applies the positivity from excited_jcost to construct an explicit positive gap on the lattice.

outside recognition

Aspects Recognition does not yet address:

The lemma Jcost_pos_of_ne_one (the justification of excited_jcost) is imported from IndisputableMonolith.Cost and is not defined in the supplied slice.

recognition modules consulted

The Recognition library is at github.com/jonwashburn/shape-of-logic. The model is restricted to the supplied Lean source and instructed not to invent theorem names. Treat output as a starting point, not a verified proof.