t6_phi_unique_from_derived
plain-language theorem explainer
Any positive real satisfying the golden equation r^{2} = r + 1 equals the Recognition Science constant φ. T6 packaging theorems cite this as the uniqueness half of "φ forced by self-similar hierarchy." The proof rules out r = 1 by arithmetic, rewrites the equation into ledger-closure form, and applies the complete phi-forcing theorem.
Claim. For every real $r > 0$, if $r^2 = r + 1$, then $r = \varphi$, where $\varphi$ is the golden-ratio constant of Recognition Science (the unique positive self-similar scale ratio).
background
The module is the public T-1 through T8 forcing spine. T6 asserts that φ is forced by a realized self-similar hierarchy: geometric scales closed under additive ledger composition.
Upstream, the complete phi-forcing theorem states that φ is the unique positive ratio for a geometric scale sequence {1, r, r², ...} closed under additive ledger composition compose(a,b) = a + b. Concretely: any r > 0 with r ≠ 1 and 1 + r = r² equals phi.
In the forcing chain, T5 supplies J-uniqueness (J(x) = (x + x^{-1})/2 - 1); T6 then forces φ as the self-similar fixed point. The two names for the constant (PhiForcing.φ and Constants.phi) are definitionally identical.
proof idea
Introduce r > 0 with r² = r + 1. First exclude r = 1: substitution yields 1 = 2, contradicted by norm_num. Rewrite the hypothesis as the closure identity 1 + r = r² via linarith. Feed positivity, r ≠ 1, and closure into phi_forcing_complete, which returns r = Constants.phi. Finish by simp, identifying PhiForcing.φ with Constants.phi.
why it matters
This bridge puts the derived phi-forcing result into the exact uniqueness format demanded by T6. Downstream, t6_holds installs it as the phi_unique field of T6_Phi_Forced; the UnifiedForcingChain copies do the same for the full spine, and the T5-to-T6 forced bridge consumes it when assembling self-similarity into T6.
In the primer landmarks this is precisely T6: φ forced as the self-similar fixed point after T5 J-uniqueness. It closes the uniqueness half of the golden-ratio step that later feeds the eight-tick octave (T7) and D = 3 (T8). The claim is fully proved; no scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.