closure_populates_next

formal source

 338
 339    This is the POPULATION theorem — not a cost bound, but a structural
 340    consequence of closure. The composed entry EXISTS. -/
 341theorem closure_populates_next (n : ℤ) :
 342    PhiForcingDerived.ledgerCompose (PhiForcing.φ ^ n) (PhiForcing.φ ^ (n + 1)) =
 343    PhiForcing.φ ^ (n + 2) := by
 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. -/
 353theorem every_rung_from_fibonacci (k : ℤ) (_hk : 2 ≤ k) :
 354    PhiForcingDerived.ledgerCompose (PhiForcing.φ ^ (k - 2)) (PhiForcing.φ ^ (k - 1)) =
 355    PhiForcing.φ ^ k := by
 356  unfold PhiForcingDerived.ledgerCompose
 357  have h := fibonacci_cascade (k - 2)
 358  convert h using 2 <;> ring_nf
 359
 360/-- **Ledger Symmetry**: J(x) = J(1/x) means that for every
 361    positive rung φ^n, the reciprocal rung φ^{-n} has the same cost.
 362    The ledger's double-entry structure (T3) forces both to exist. -/
 363theorem ledger_symmetry_negative_rungs (n : ℤ) :
 364    Jcost (PhiForcing.φ ^ n) = Jcost (PhiForcing.φ ^ (-n)) := by
 365  rw [show PhiForcing.φ ^ (-n) = (PhiForcing.φ ^ n)⁻¹ from zpow_neg PhiForcing.φ n]
 366  exact Jcost_symm (zpow_pos PhiForcing.phi_pos n)
 367
 368/-! ## Part X: Main Theorem — Stillness Is Creative (Fully Derived)
 369
 370All premises now trace back to T0–T8. No structures are introduced as axioms.
 371The logical chain: