one_plus_phi_eq_phi_sq

formal source

 329  ring
 330
 331/-- Equivalent form: 1 + φ = φ² (the base case of the Fibonacci cascade). -/
 332theorem one_plus_phi_eq_phi_sq : 1 + PhiForcing.φ = PhiForcing.φ ^ 2 := by
 333  linarith [PhiForcing.phi_equation]
 334
 335/-- **Ledger Composition Populates**: If the ledger has entries at
 336    scales φ^n and φ^{n+1}, additive ledger composition (from T6
 337    closure) creates an entry at scale φ^{n+2}.
 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. -/