theorem proved term proof

`closure_populates_next`

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

formal statement (Lean)

 341theorem closure_populates_next (n : ℤ) :
 342    PhiForcingDerived.ledgerCompose (PhiForcing.φ ^ n) (PhiForcing.φ ^ (n + 1)) =
 343    PhiForcing.φ ^ (n + 2) := by

proof body

Term-mode proof.

 344  unfold PhiForcingDerived.ledgerCompose
 345  exact fibonacci_cascade n
 346
 347/-- **Rung Generation**: Every rung k ≥ 2 is the ledger composition
 348    of the two preceding rungs. Starting from rung 0 (= 1, ground state)
 349    and rung 1 (= φ, forced by T4 + T6), repeated application generates
 350    all rungs: 0,1 → 2 → 3 → 4 → ...
 351
 352    This is not a cost bound — it is a structural IDENTITY from closure. -/

depends on (31)

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
rung in IndisputableMonolith.Compat.Constants decl_use
all in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
rung in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
ledgerCompose in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
Generation in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
fibonacci_cascade in IndisputableMonolith.Foundation.StillnessGenerative decl_use
Generation in IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization 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
all in IndisputableMonolith.Musicology.ModalPreferenceFromPhi decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
Generation in IndisputableMonolith.Physics.CKM decl_use
Generation in IndisputableMonolith.Physics.ThreeGenerations decl_use
two in IndisputableMonolith.QFT.SpinStatistics decl_use
Generation in IndisputableMonolith.RecogSpec.RSLedger decl_use
rung in IndisputableMonolith.RSBridge.Anchor decl_use

… and 1 more