T5_To_T6_Forced_Bridge
plain-language theorem explainer
Packages the T5→T6 producer bridge: given uniqueness of the reciprocal cost J, it records both the self-similarity certificate and the forced golden-ratio surface φ² = φ + 1. Anyone assembling the public T−1…T8 spine cites this so T6 is not inserted independently of T5. It is a pure Prop structure with two fields; inhabitance is discharged by a one-line constructor theorem.
Claim. Given a proof that the canonical reciprocal cost $J$ is unique (reciprocal, normalized, composition-law, calibrated, continuous on $(0,\infty)$), the T5→T6 producer bridge asserts two facts: (i) the T5-indexed self-similarity certificate is available, and (ii) $\varphi$ is forced, i.e. $\varphi^2 = \varphi + 1$, $\varphi > 0$, and $\varphi$ is the unique positive root of that equation.
background
This module is the public theory-only T−1 through T8 forcing spine. T5 asserts uniqueness of the canonical reciprocal cost $J(x) = \tfrac12(x + 1/x) - 1$ on $(0,\infty)$ under reciprocity, normalization, the Recognition Composition Law, calibration, and continuity. T6 asserts that the golden ratio $\varphi$ is forced as the unique positive solution of $r^2 = r + 1$.
The intermediate self-similarity bridge (indexed by a T5 package) re-exports T5 uniqueness so the $\varphi$ layer cannot float free of J-uniqueness, and records that bare closed-observable data alone do not force hierarchy fields. The present structure is the producer bridge that sits on top of that certificate and exposes the actual T6 surface as downstream output.
Upstream, T5 is obtained from CostUniqueness lemmas and law_of_logic_forces_jcost; the honesty note in the module stresses that T5 does not consume the T−1…T4 floor beyond cosmetic re-export.
proof idea
No proof body: this is a Prop-valued structure definition. Inhabitation is supplied by the sibling theorem t5_to_t6_forced_bridge_holds, a one-line constructor that sets self_similarity from t5_to_t6_bridge_holds h5 and t6 from t6_holds (or the explicit PhiForcing fields phi_equation, phi_pos, uniqueness). The structure merely bundles those two already-proved surfaces under a single T5-indexed interface.
why it matters
In the forcing chain, T5 is J-uniqueness and T6 is φ forced as the self-similar fixed point. This producer bridge is the formal glue that makes T6 a downstream output of T5 rather than an independent insertion, matching the UnifiedForcingChain doc: "T6 is no longer inserted independently of the T5→T6 bridge."
It is consumed by CompleteForcingChainT8 and CompleteForcingChain, and by the inhabitance theorems t5_to_t6_forced_bridge_holds in both the public bridge module and UnifiedForcingChain. Without it, the spine could skip from unique J to φ without recording the self-similarity certificate. Framework landmark: T6 in the T0–T8 chain, with φ the scale ratio of the realized hierarchy used later for mass ladders and constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.