t6_phi_unique_from_derived
plain-language theorem explainer
Any positive real solving r² = r + 1 equals the Recognition-Science golden ratio φ. Citers of T6 (φ forced by self-similarity) use this uniqueness clause. The proof excludes r = 1, rewrites the golden equation as additive ledger closure, 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 positive golden ratio fixed by the Recognition-Science phi-forcing package.
background
The Unified Forcing Chain module aims to show that every step T-1 through T8 is forced from the cost foundation (Recognition Composition Law plus normalization and calibration). T6 is the step that pins the golden ratio: self-similarity in a discrete ledger forces a unique positive scale ratio.
Upstream, phi_forcing_complete states that φ is the unique positive ratio for a geometric scale sequence closed under additive ledger composition: scales {1, r, r², …} with compose(a,b) = a + b and the closure identity 1 + r = r² imply r = φ (with r ≠ 1). The present theorem is the T6-format packaging of that uniqueness: the hypothesis is written as the golden equation r² = r + 1 rather than as the ledger-closure form.
Constants.phi and PhiForcing.φ are definitionally the same positive root; the bridge only has to align the two namings after the derived forcing theorem fires.
proof idea
Introduce r > 0 and the golden equation r² = r + 1. First rule out r = 1 by substitution and a numeric contradiction (1 ≠ 1 + 1). Rewrite the equation as the additive closure form 1 + r = r² via linear arithmetic. Feed positivity, r ≠ 1, and closure into PhiForcingDerived.phi_forcing_complete to obtain r = Constants.phi. Finish by simp-aligning Constants.phi with PhiForcing.φ.
why it matters
This is the uniqueness half of T6 in the forcing chain (primer landmark: φ forced as the self-similar fixed point). Downstream, both UnifiedForcingChain.t6_holds and TMinus1ToT8Bridge.t6_holds assemble T6_Phi_Forced by packaging the golden equation, positivity, and this uniqueness proof. The T5-to-T6 forced bridge likewise installs it as the t6 field once self-similarity is supplied from unique J.
Without uniqueness, T6 would only assert that φ solves the fixed-point equation; the chain needs that no other positive scale works, so later steps (eight-tick octave, D = 3, and constants built from φ) inherit a single rung base. The declaration is a thin format bridge from the derived complete forcing theorem into the T0–T8 interface, not a new analytic argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.