T4_To_T5_Cost_Bridge
plain-language theorem explainer
Packages the T4→T5 cost bridge: given a T4 recognition floor and its realization bridge, the RCL surface is available, equals the bridge surface, and T5 (uniqueness of the reciprocal cost J) holds. Cited by anyone assembling the public T−1..T8 spine or CompleteForcingChain. It is a Prop structure, not a derivation; the honesty note records that T5 is proved from cost-uniqueness alone and does not consume the discrete floor.
Claim. Given a forced T4 recognition floor $h_4$ and a realization bridge from it, the following hold as a packaged proposition: (i) for every comparison operator $C$ satisfying the laws of logic there exist a bilinear form $P$ and a constant $c$ such that the derived cost of $C$ has multiplicative consistency under $P$ with $P(u,v)=2u+2v+c\,uv$; (ii) that surface equals the bridge's RCL surface; (iii) the canonical cost $J(x)=(x+x^{-1})/2-1$ is the unique reciprocal, normalized, calibrated, continuous cost satisfying the Recognition Composition Law.
background
The module exposes the public T−1 through T8 forcing spine and stops before private operator layers. T4 asserts a Boolean two-point recognition floor: distinction exists, a recognition structure on Bool is nonempty, and zero-cost recognition is compatible with that floor. The intermediate realization bridge records floor recognition, a logic realization, positive-ratio realization for every law-of-logic comparison, and arithmetic invariants.
T5 is the uniqueness package for the canonical reciprocal cost $J(x)=(x+x^{-1})/2-1$: reciprocity, normalization, the Recognition Composition Law (RCL) $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, calibration, continuity on $(0,\infty)$, and uniqueness among Aczél-smooth competitors. Upstream, law_of_logic_forces_jcost already proves that any reciprocal normalized calibrated continuous cost satisfying RCL equals $J$.
The RCL surface field is the d'Alembert-style multiplicative consistency of the derived cost under a bilinear $P(u,v)=2u+2v+c,uv$. That surface is imported from the realization bridge, not derived from the Boolean floor cost.
proof idea
This declaration is a structure (Prop bundle), not a proved theorem. Its three fields are: availability of the RCL surface for every law-of-logic comparison; definitional equality of that surface with the realization bridge's surface; and a full T5_J_Unique record.
The companion constructor t4_to_t5_cost_bridge_holds fills the fields by re-exporting bridge.rcl_surface, taking rfl for the equality, and building t5 from CostUniqueness lemmas plus law_of_logic_forces_jcost. The honesty note is explicit: nothing from the T−1..T4 floor enters the uniqueness argument beyond that re-export.
why it matters
This is the public T4→T5 arrow in the forcing spine (primer landmark T5: J-uniqueness). Downstream it is consumed by CompleteForcingChainT8 and by UnifiedForcingChain.CompleteForcingChain, so the complete chain no longer treats T5 as a free sibling of T4.
The 2026 audit honesty note is the real content: T5 is proved entirely from cost-uniqueness and law_of_logic_forces_jcost; deleting T−1..T4 breaks no T5 proof. The discrete floor cost cannot satisfy the composition law T5 needs (PrimitiveDistinction), so the continuous positive-ratio comparison surface remains an imported hypothesis (SI2/C6), not a consequence of the floor. The structure packages a conditional chain; it is not a forcing proof of T5 from T4. Repair pointer: Foundation.RecognitionLedgerFloor upgrades the carrier but is not yet wired into this bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.