T4_To_T5_Cost_Bridge
plain-language theorem explainer
Packages the T4→T5 step of the unified forcing chain: given a T4 recognition floor and its realization bridge, it records that an RCL surface is available and carries the T5 uniqueness certificate for J. Anyone assembling CompleteForcingChain cites it to wire t5 after t4_to_t5. It is a Prop structure (field bundle), not a derivation; the honesty note stresses T5 is proved from cost-uniqueness lemmas, not from the discrete floor.
Claim. Given a forced T4 recognition floor and a T4$\to$T5 realization bridge, the cost bridge is the proposition that (i) the canonical continuous $J$-comparison obeys the Law of Logic, (ii) that comparison admits a multiplicative consistency surface $P(u,v)=2u+2v+c\,uv$, (iii) every Law-of-Logic comparison has such an RCL surface, (iv) that surface equals the bridge's RCL surface, and (v) the T5 uniqueness package holds: $J(x)=\frac12(x+1/x)-1$ is the unique reciprocal, normalized, calibrated, continuous cost satisfying the Recognition Composition Law.
background
In the Unified Forcing Chain, levels T−1 through T8 are presented as inevitabilities from a cost foundation. T4 asserts that a non-trivial discrete distinction on the Boolean floor already supplies a recognition witness. The prior realization bridge lifts that floor to a setting-independent Law-of-Logic realization and exposes an RCL surface on continuous positive-ratio comparisons.
T5 is the classical uniqueness statement for the J-cost: reciprocity $J(x)=J(1/x)$, normalization $J(1)=0$, calibration of the second derivative at 1, continuity on $(0,\infty)$, and the Recognition Composition Law
$J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
The authoritative engine is law_of_logic_forces_jcost (Aczél-packaged): those hypotheses force $J(x)=\frac12(x+x^{-1})-1$. Multiplicative consistency means $F(xy)+F(x/y)=P(F(x),F(y))$ for a combiner $P$.
The module's stronger claim is a complete inevitability chain. This structure sits on the T4→T5 arrow and is the place where packaging is separated from forcing.
proof idea
No proof body: this is a structure definition (a bundled Prop). Fields name the certificates a holder must supply. The companion theorem t4_to_t5_cost_bridge_holds fills them: Law-of-Logic for the canonical J-comparison; RCL surface for that comparison by applying the realization bridge's rcl_surface; rcl_surface_available by re-exporting bridge.rcl_surface; definitional equality of surfaces; and t5 built from CostUniqueness facts plus law_of_logic_forces_jcost, without consuming bridge data inside the uniqueness argument.
why it matters
This is the T5 packaging slot in CompleteForcingChain and CompleteForcingChainT8: without it, t5 would sit as a free sibling of the T4→T5 arrow rather than a named downstream of the realization bridge. Framework landmark: T5 J-uniqueness, the step that pins $J(x)=\cosh(\log x)-1$ before T6 forces $\varphi$ as the self-similar fixed point.
The 2026 honesty note is load-bearing. T5 is proved entirely from cost-uniqueness lemmas; deleting T−1..T4 breaks no T5 proof. The continuous positive-ratio surface and composition law are imported hypotheses (SI2/C6 in RS_v1), not consequences of the discrete floor. PrimitiveDistinction shows the floor's own cost cannot satisfy the composition law. Downstream holders re-export the same caveat. The declaration earns its place as explicit conditional packaging, closing a cosmetic gap in the chain narrative rather than a mathematical forcing gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.