T6_Phi_Forced
plain-language theorem explainer
T6 packages the claim that the golden ratio φ = (1+√5)/2 is the unique positive solution of x² = x + 1. Anyone citing the forcing spine after J-uniqueness uses this record as the φ-forcing interface. It is a bare Prop structure (three fields: equation, positivity, uniqueness), inhabited elsewhere by the PhiForcing lemmas.
Claim. The T6 interface asserts three facts about the forced scale $\varphi$: $\varphi^2 = \varphi + 1$, $\varphi > 0$, and uniqueness: every real $r > 0$ with $r^2 = r + 1$ equals $\varphi$.
background
The module exposes the public T−1 through T8 forcing spine and stops before private operator/measurement layers. T5 fixes the unique reciprocal cost $J(x) = (x + x^{-1})/2 - 1$. T6 is the next step: once a discrete ledger carries a self-similar cost hierarchy, the only admissible scaling ratio is the golden ratio.
In the Recognition framework, $\varphi$ is not an input constant. Upstream PhiForcing and PhiRing define $\varphi = (1+\sqrt{5})/2$ and prove the golden equation by direct algebra on $\sqrt{5}$. The UnifiedForcingChain copy of this structure states the same package: "φ is not chosen; it's the unique solution to $x^2 = x + 1$ with $x > 0$."
The three fields are pure real-analysis content: the defining quadratic, positivity, and uniqueness among positive reals. No ledger or cost data appears in the signature itself.
proof idea
No proof body: this is a structure ... : Prop interface. Inhabitation is supplied by t6_holds, which fills the three fields from PhiForcing.phi_equation, PhiForcing.phi_pos, and a derived uniqueness lemma (t6_phi_unique_from_derived). The equation proofs upstream unfold the closed form of $\varphi$ and finish with field_simp / nlinarith on $\sqrt{5}$.
why it matters
T6 is the φ-forcing landmark in the T0–T8 chain (primer T6: φ forced as the self-similar fixed point). Downstream, T5_To_T6_Forced_Bridge attaches this record to the T5 uniqueness package via a self-similarity bridge, so φ is not inserted independently of T5. CompleteForcingChainT8 and CompleteForcingChain both carry a t6 field of this type.
spine_to_extras_bridge_holds consumes a T6_Phi_Forced witness to derive φ-recursion constants (t6_to_phi_constants_canonical_bridge_holds). That feeds mass-ladder yardsticks, $c=1$, $\hbar = \varphi^{-5}$, $G = \varphi^5/\pi$, and the eight-tick/D=3 steps (T7, T8). Without this interface the later constant and dimension forcing has no typed φ source.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.