pith. machine review for the scientific record. sign in
theorem proved term proof

one_plus_phi_eq_phi_sq

show as:
view Lean formalization →

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)

 332theorem one_plus_phi_eq_phi_sq : 1 + PhiForcing.φ = PhiForcing.φ ^ 2 := by

proof body

Term-mode proof.

 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. -/

depends on (18)

Lean names referenced from this declaration's body.