one_plus_phi_eq_phi_sq
plain-language theorem explainer
The algebraic identity 1 + φ = φ² holds as the base case of the Fibonacci cascade that populates the phi-ladder. Workers deriving ledger entries from T6 closure or showing rung population would cite this relation. The proof is a one-line wrapper that invokes the defining quadratic equation for φ.
Claim. $1 + φ = φ^2$, where φ is the positive real root of the quadratic forced by Recognition Science T5 and T6.
background
The module derives that the unique zero-defect ground state x=1 is unstable and generates structure via the phi-ladder. Key upstream result is the theorem φ² = φ + 1, which states the defining equation of φ. The Recognition Composition Law (CostAxioms.Composition) and T6 closure force non-trivial ledger entries to lie on geometric scales φ^n. The module doc-comment lists the derivation chain: Law of Existence, T4 forcing, T7 eight-tick requirement, and T6 closure together imply every non-trivial entry satisfies the Fibonacci relation.
proof idea
One-line wrapper that applies the phi_equation theorem via the linarith tactic on the supplied hypothesis.
why it matters
This supplies the base case for the Fibonacci cascade φ^n + φ^{n+1} = φ^{n+2} that appears in the module doc-comment under step 7. It directly supports the subsequent Ledger Composition Populates remark, which states that additive composition on closed geometric scales creates the next rung without invoking cost bounds. The result sits inside the T0-T8 forcing chain and the stillness-generative argument that x=1 cannot remain uniform.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.