pith. machine review for the scientific record. sign in
def definition def or abbrev

hamiltonianSpectrumCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  58def hamiltonianSpectrumCert : HamiltonianSpectrumCert where
  59  five_sectors := spectralSectorCount

proof body

Definition body.

  60  vacuum := vacuum_jcost
  61  excited := excited_jcost
  62  lattice_gap := lattice_gap_witness
  63
  64end IndisputableMonolith.Physics.RecognitionHamiltonianSpectrum

depends on (6)

Lean names referenced from this declaration's body.