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)
214def summary : List String := [
proof body
Definition body.
215 "8-tick quantizes θ to 8 values",
216 "J-cost minimum at θ = 0",
217 "No axion required (but compatible)",
218 "Predicts θ = 0 exactly"
219]
220
221/-! ## Strong CP Certificate (machine-verified) -/
222
223/-- **THEOREM (Strong CP Certificate)**: The J-cost is globally minimized at θ = 0.
224 The minimum is achieved exactly; all other allowed values (multiples of π/4)
225 have strictly positive J-cost.
226 Proof: thetaJCost(θ) = 1 − cos θ ≥ 0 = thetaJCost(0) for all θ. -/
depends on (21)
Lean names referenced from this declaration's body.
-
all
in IndisputableMonolith.Aesthetics.NarrativeGeodesic
decl_use
-
all
in IndisputableMonolith.Anthropology.KinshipGraphCohomology
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
compatible
in IndisputableMonolith.Complexity.SAT.Backprop
decl_use
-
tick
in IndisputableMonolith.Constants
decl_use
-
tick
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
all
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
required
in IndisputableMonolith.Foundation.DomainBootstrap
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
all
in IndisputableMonolith.Musicology.ModalPreferenceFromPhi
decl_use
-
thetaJCost
in IndisputableMonolith.StandardModel.StrongCP
decl_use