T6_Phi_Forced
plain-language theorem explainer
T6 packages the claim that the golden ratio φ is forced: it solves x² = x + 1, is positive, and is the unique positive real solution. Anyone citing the Unified Forcing Chain (T0–T8) or the T5→T6 self-similarity bridge uses this record as the T6 node. It is a Prop-structure interface; inhabitants are built by assembling PhiForcing lemmas, not by a local proof body.
Claim. The T6 assertion is the conjunction of three facts about the forced scale $\varphi$: $\varphi^2 = \varphi + 1$, $\varphi > 0$, and uniqueness—if $r \in \mathbb{R}$ satisfies $r > 0$ and $r^2 = r + 1$, then $r = \varphi$. Equivalently, in a discrete ledger with self-similar cost structure the only positive scaling ratio is $\varphi = (1+\sqrt{5})/2$.
background
The module UnifiedForcingChain aims at a complete inevitability spine from an absolute floor through T0–T8, all driven by the Recognition Composition Law plus normalization and calibration of the cost. After T5 pins the unique cost $J(x) = (x+x^{-1})/2 - 1$ (equivalently $\cosh(\log x)-1$), T6 is the next rung: self-similarity in a discrete ledger forces a single scale factor.
That scale is the golden ratio $\varphi$ from PhiForcing / PhiRing. Upstream, phi_equation states $\varphi^2 = \varphi + 1$ by direct expansion of $\varphi = (1+\sqrt{5})/2$. Positivity and uniqueness among positive reals are the remaining fields of this record. The same three-field shape appears in the TMinus1ToT8Bridge copy of T6, so the chain can be assembled either in the unified module or via the bridge layer.
Self-similarity here means the ledger’s cost structure is scale-invariant under a fixed ratio; the quadratic $x^2 = x+1$ is the fixed-point equation of that recursion. No continuous free parameter survives once positivity is imposed.
proof idea
There is no proof body: this declaration is a structure ... : Prop bundling three fields. Inhabitation is external. The standard constructor (e.g. t6_holds in the bridge) sets phi_equation to PhiForcing.phi_equation, phi_positive to PhiForcing.phi_pos, and phi_unique to a derived uniqueness lemma (t6_phi_unique_from_derived) that any positive root of $x^2-x-1=0$ equals the named $\varphi$. Algebraically those lemmas expand the closed form and use square-root and ring identities; the structure only records the resulting Prop.
why it matters
T6 is the named landmark “φ forced as the self-similar fixed point” in the T0–T8 forcing chain. Downstream it is required by CompleteForcingChain and CompleteForcingChainT8, by T5_To_T6_Forced_Bridge (self-similarity plus a T6 witness), and by t6_holds / spine_to_extras_bridge_holds, which route T6 into φ-constant derivations (c, ℏ, G, α band) and the extras layer.
Without this record the chain stops after unique $J$: mass ladders, eight-tick timing (T7), and $D=3$ (T8) all need a forced dimensionless scale. The doc-comment’s claim is sharp: φ is not a modeling choice; it is the unique positive solution of the self-similarity equation. Open work sits on the T5→T6 arrow (self-similarity bridge), not on the three algebraic fields themselves once PhiForcing is accepted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.