t6_holds
plain-language theorem explainer
T6 packages the claim that φ = (1+√5)/2 is forced: it solves x² = x+1, is positive, and is the unique positive real root. Forcing-chain and constants-from-φ arguments cite this as the T6 surface. The proof is a three-field structure assembly from PhiForcing and a derived uniqueness lemma.
Claim. The T6 package holds: $\varphi$ satisfies $\varphi^2 = \varphi + 1$, $\varphi > 0$, and for every real $r > 0$ with $r^2 = r + 1$ one has $r = \varphi$. Equivalently, in a discrete ledger with self-similar cost, the only positive scaling ratio is the golden ratio.
background
The Unified Forcing Chain module aims to show every step T-1 through T8 is forced from the Recognition Composition Law plus normalization and calibration, rather than merely compatible. In that ladder, T5 pins the unique cost $J(x) = (x+x^{-1})/2 - 1$; T6 is the next step: self-similarity on a discrete ledger forces the scaling ratio $\varphi$.
The T6 surface is the structure with three fields: the golden equation $\varphi^2 = \varphi + 1$, positivity $\varphi > 0$, and uniqueness among positive reals. Upstream, PhiForcing already proves the equation and positivity for the concrete definition $\varphi = (1+\sqrt{5})/2$; a derived bridge supplies uniqueness in the T6 format. The module doc states the slogan: "$\varphi$ forced ← self-similarity in discrete ledger."
proof idea
Term-mode structure construction, not a tactic script. Fill phi_equation by PhiForcing.phi_equation (algebraic verification of $\varphi^2 = \varphi + 1$ from the closed form). Fill phi_positive by PhiForcing.phi_pos. Fill phi_unique by the in-module bridge t6_phi_unique_from_derived, which rephrases the derived uniqueness theorem into the $\forall r > 0$ quantifier required by the T6 structure. No new arithmetic is done here.
why it matters
T6 is the φ-forcing landmark in the T0–T8 chain: after unique $J$ (T5), the self-similar fixed point is forced rather than chosen. Downstream, t5_to_t6_forced_bridge_holds consumes T5 and exposes this theorem as the bridge output, so T6 is no longer inserted independently of the T5→T6 step.
It is an ingredient of constants_from_phi and constants_from_phi_canonical (via the spine-to-extras bridge), which derive $c=1$, $\hbar = \varphi^{-5}$, $G = \varphi^5/\pi$ in RS-native units. It also feeds ultimate_inevitability and ultimate_inevitability_canonical, the module’s complete-inevitability root theorems, and the classical-negation-plus-unique-minimizer package. Without a proved T6 surface, the φ-ladder mass formula and constant derivations have no forcing anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.