t4_to_t5_cost_bridge_holds
plain-language theorem explainer
Given recognition forced (T4) and a T4→T5 realization bridge, this packages the T5 cost-uniqueness record: unique reciprocal, normalized, calibrated, continuous cost on positive reals is the canonical J-cost. Cited by the complete T−1..T8 forcing-chain assemblers. Term-mode structure fill: T5 fields come from CostUniqueness and law_of_logic_forces_jcost; the bridge only re-exports its RCL surface.
Claim. Assume recognition is forced on the Boolean floor, and a T4$\to$T5 realization bridge is given (admissible positive-ratio Law-of-Logic realization with an RCL surface). Then a T4$\to$T5 cost bridge holds: the canonical continuous $J$-comparison satisfies the laws of logic; the bridge's RCL surface applies to that comparison; and T5 holds, i.e. the unique reciprocal, normalized, calibrated, continuous cost obeying the Recognition Composition Law is $J(x)=(x+x^{-1})/2-1$.
background
The module aims at a complete inevitability chain from an absolute floor through T0–T8, driven by the Recognition Composition Law plus normalization and calibration. T5 is the uniqueness step for the cost functional $J$.
T4 asserts that a non-trivial discrete distinction on the Boolean carrier already supplies a recognition witness and relation (pre-analytic floor). The realization bridge lifts that floor to a setting-independent Law-of-Logic realization and exposes a continuous positive-ratio RCL surface on which the composition law can be stated.
Upstream, law_of_logic_forces_jcost is the uniqueness engine: any reciprocal, normalized, composition-law, calibrated, continuous cost equals $J$, under an Aczél smoothness package (continuous d'Alembert solutions are $C^\infty$). Supporting facts include reciprocal symmetry $J(x)=J(x^{-1})$, normalization, calibration, and continuity of $J$ on $\mathbb{R}_+$.
proof idea
Term-mode constructor for the cost-bridge structure. Comparison-laws field is the pre-proved fact that the canonical $J$-comparison satisfies the laws of logic. RCL-surface fields are pure re-exports: apply the realization bridge's surface to that comparison, mark the surface available, and identify it by rfl.
The embedded T5 record is filled entirely from CostUniqueness: reciprocal, normalized, composition law, calibrated, continuous-on-positives. Uniqueness is a direct call to law_of_logic_forces_jcost after installing the caller's Aczél package as an instance. Nothing inside that uniqueness argument reads the T4 floor or the bridge beyond the surface re-export.
why it matters
Closes the named T4→T5 arrow inside complete_forcing_chain and complete_forcing_chain_t8, so the chain assembler can populate T5 from the realization bridge rather than as a free sibling. Framework landmark: T5 J-uniqueness, $J(x)=\cosh(\log x)-1$, forced by RCL plus normalization and calibration (primer T5).
The doc-comment's honesty note is load-bearing: this is conditional packaging, not a derivation of T5 from T−1..T4. Deleting the floor breaks no T5 proof; the continuous comparison surface and composition law are imported (SI2/C6-style hypotheses). The floor's own discrete cost cannot satisfy the composition law. Downstream chain claims that read as "T4 forces T5" should be read as "T5 is attached at the T4 layer with an RCL surface certificate," not as a forcing step from the Boolean floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.