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)
183theorem gap_size_pos : 0 < gap_size := by
proof body
Term-mode proof.
184 rw [gap_size_eq]; norm_num
185
186/-! ## §5. Master certificate -/
187
188/-- **PULSAR PERIOD FROM RECOGNITION-RUNG MASTER CERTIFICATE
189(Track AS7).**
190
191Eight clauses, each derived from `Constants.phi` real-arithmetic
192+ the canonical 8-tick recycling shift:
193
1941. `normal_median_rung_eq` : normal pulsar median rung = 4.
1952. `ms_median_rung_eq` : millisecond pulsar median rung = 4.
1963. `recycling_rung_shift_eq` : canonical 8-tick shift = 8.
1974. `period_geometric` : adjacent rungs differ by exactly φ.
1985. `bimodal_ratio_pos` : bimodal ratio is positive.
1996. `bimodal_ratio_gt_thirty` : ratio strictly greater than 30
200 (sharp bimodality).
2017. `bimodal_ratio_lt_phi_nine` : ratio strictly less than `φ^9`.
2028. `gap_size_eq` : structural gap of 7 unstable rungs between
203 the two families.
204-/
depends on (36)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
bimodal_ratio_gt_thirty
in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung
decl_use
-
bimodal_ratio_lt_phi_nine
in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung
decl_use
-
bimodal_ratio_pos
in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung
decl_use
-
gap_size
in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung
decl_use
-
gap_size_eq
in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung
decl_use
-
ms_median_rung_eq
in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung
decl_use
-
normal_median_rung_eq
in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung
decl_use
-
period_geometric
in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung
decl_use
-
recycling_rung_shift_eq
in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung
decl_use
-
rung
in IndisputableMonolith.Compat.Constants
decl_use
-
tick
in IndisputableMonolith.Constants
decl_use
-
tick
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
sharp
in IndisputableMonolith.Cost.Ndim.Projector
decl_use
-
Constants
in IndisputableMonolith.CPM.LawOfExistence
decl_use
-
rung
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
canonical
in IndisputableMonolith.Foundation.ArithmeticOf
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
-
canonical
in IndisputableMonolith.Gap45.Beat
decl_use
-
gap
in IndisputableMonolith.Gap45.Derivation
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
gap
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
rung
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
gap
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
… and 6 more