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)
62def summary : String :=
proof body
Definition body.
63 "QFT from Recognition Science (Tier 2):\n" ++
64 "✅ Spin-Statistics: 8-tick phase mechanism\n" ++
65 "✅ Fermion/Boson symmetry: odd/even phase ledger entries\n" ++
66 "✅ Pauli Exclusion: ledger single-occupancy\n" ++
67 "✅ CPT Invariance: Ledger symmetry\n" ++
68 "✅ Noether's Theorem: cost stationarity\n" ++
69 "✅ S-Matrix Unitarity: ledger conservation\n" ++
70 "✅ Decoherence: Gap-45 threshold\n" ++
71 "✅ Higgs Mechanism: J-cost symmetry breaking\n" ++
72 "✅ Gauge Invariance: ledger redundancy\n" ++
73 "✅ UV Cutoff: τ₀ discreteness scale\n"
74
75end IndisputableMonolith.QFT
depends on (14)
Lean names referenced from this declaration's body.
-
tick
in IndisputableMonolith.Constants
decl_use
-
tick
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
scale
in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS
decl_use
-
phase
in IndisputableMonolith.Foundation.EightTick
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
Fermion
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
Fermion
in IndisputableMonolith.Masses.SMVerification
decl_use
-
phase
in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge
decl_use
-
Spin
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
Statistics
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
S
in IndisputableMonolith.Relativity.ILG.Action
decl_use
-
Fermion
in IndisputableMonolith.RSBridge.Anchor
decl_use