origin_question_resolved
plain-language theorem explainer
The theorem assembles the defining equation of the golden ratio, its uniqueness, the strict bounds on its recognition cost J, the cascade inequality on the phi-ladder, and strict positivity of costs for nonzero rungs. A researcher tracing the T0-T8 forcing chain would cite it to close the origin question. The proof is a term-mode conjunction that directly invokes five upstream results.
Claim. Let φ be the positive real root of r² = r + 1. Then φ satisfies φ² = φ + 1, is the unique positive solution to that equation, obeys 0 < J(φ) < 1 where J is the recognition cost, the cost on the φ-ladder satisfies J(φ^{a+b}) ≤ 2J(φ^a) + 2J(φ^b) + 2J(φ^a)J(φ^b) for all integers a, b, and J(φ^n) > 0 whenever n ≠ 0.
background
The module StillnessGenerative derives that the ground state x = 1 is unstable and generative from T0-T8 with no added assumptions. The φ-ladder is the discrete skeleton {φ^n | n ∈ ℤ} (OntologyPredicates.phi_ladder and Astrophysics.NucleosynthesisTiers.phi_ladder). J is the recognition cost from LawOfExistence; Jcost denotes its restriction to ladder values. Upstream phi_equation states: THEOREM: φ² = φ + 1 (the defining equation). MODULE_DOC records the chain: T5 gives unique zero-defect state, T4 forces content, T7 forces departure via 8-tick non-degeneracy, T6 forces ratio φ, and the finite barrier J(φ) < 1 permits the Fibonacci cascade.
proof idea
The proof is a one-line term-mode wrapper. It supplies the five conjuncts by direct reference to PhiForcing.phi_equation, the lambda that applies PhiForcing.phi_forced, the pair phi_cost_pos with phi_perturbation_bounded, ladder_cascade_bound, and the lambda that applies phi_ladder_positive_cost.
why it matters
The declaration resolves the origin question by confirming every sub-question listed in its doc-comment via T0-T8: creation by T4, φ by T6, crossable barrier by J(φ) < 1, full ladder by Fibonacci cascade, and unavoidability by T7. It completes the StillnessGenerative module and supplies the symmetry-breaking interpretation that feeds the Recognition framework. No used_by edges appear, yet the result underpins the claim that x = 1 is the maximally creative source.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.