theorem proved term proof

`sync_period_factored`

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

formal statement (Lean)

 265theorem sync_period_factored : 360 = 8 * 45 := by norm_num

proof body

Term-mode proof.

 266
 267/-- If r_ref = ell0 * phi^360, the prediction is tied to the sync period
 268    from D=3 forcing. This makes r_ref a zero-parameter consequence of
 269    the forcing chain (modulo the 4-rung offset). -/

depends on (18)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
period in IndisputableMonolith.Astrophysics.PulsarEmissionRegimesFromRS decl_use
rung in IndisputableMonolith.Compat.Constants decl_use
ell0 in IndisputableMonolith.Constants decl_use
ell0 in IndisputableMonolith.Constants.Derivation decl_use
rung in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
rung in IndisputableMonolith.RSBridge.Anchor decl_use