t4_to_t5_bridge_holds
plain-language theorem explainer
Given a T4 recognition-forced certificate on the Boolean floor, this definition assembles the full T4-to-T5 realization bridge: the discrete floor and the continuous positive-ratio surface are identified as Law-of-Logic realizations with matching extracted arithmetic, so the RCL uniqueness theorem applies on the continuous side. Anyone citing the T5 uniqueness step or the complete T0–T8 chain needs this bridge. The body is a structure constructor wiring floor data, orbit equivalences, and the RCL surface lemma.
Claim. From any certificate that recognition is forced on the normalized two-point Boolean floor (nontrivial distinction and a recognition witness), one obtains a T4-to-T5 realization bridge: the Boolean floor is a Law-of-Logic realization; every continuous positive-ratio cost surface is an admissible realization of the same interface; Universal Forcing identifies their extracted arithmetic (orbit equivalence); and the Recognition Composition Law is the unique functional form of logic on that continuous surface.
background
The Unified Forcing Chain module argues that T0–T8 are forced from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$). T4 asserts that a nontrivial discrete distinction on the Boolean carrier already supplies a recognition witness and relation; T5 asserts that reciprocity, composition, normalization, and calibration force $J(x)=\frac12(x+1/x)-1$ on $(0,\infty)$.
The bridge structure packages the passage from the pre-analytic floor to the continuous surface T5 needs. A Law-of-Logic realization extracts arithmetic (orbits) from a recognition setting. The continuous positive-ratio realization is the setting where the d'Alembert-form composition law
$F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$
lives. Upstream, law_of_logic_forces_jcost states that any reciprocal, normalized, calibrated, continuous $F$ satisfying composition equals $J$; RCL_is_unique_functional_form_of_logic supplies the RCL surface used here.
Reciprocity ($J(x)=J(1/x)$) and the reciprocal automorphism on positive reals are the algebraic backbone linking ledger events to the continuous cost.
proof idea
Pure structure assembly, not a tactic proof. Fields normalized_floor, t4_floor_recognition, and t4_floor_distinction are copied from the T4 certificate. Floor and normalized-floor realizations are wrapped as T4ToT5.floorRealization and T4ToT5.floorRealizationFromNormalized. Positive-ratio realizations are pointwise T4ToT5.positiveRatioRealization.
Arithmetic invariance is the orbit equivalence: both floor and positive-ratio realizations are equivalent to the same logic-natural arithmetic via orbitEquivLogicNat, so their orbits match by trans and symm. The normalized variant does the same with the normalized floor realization. The RCL surface field is a direct application of RCL_is_unique_functional_form_of_logic on each continuous cost $C$.
why it matters
T5 (unique $J$) is the landmark that pins the cost functional to $J(x)=\cosh(\log x)-1$ via the full RCL surface. Without a bridge from the discrete T4 recognition floor to that continuous surface, the forcing chain would jump settings. This definition closes that gap inside UnifiedForcingChain and is consumed by complete_forcing_chain and by the parallel complete_forcing_chain_t8 in TMinus1ToT8Bridge.
In the primer chain: T4 (recognition from ledger + observables) feeds T5 (unique $J$ from d'Alembert + normalization + calibration). Downstream T6 forces $\varphi$ as the self-similar fixed point on the discrete ledger; T7–T8 force the eight-tick octave and $D=3$. The module's stronger claim is complete inevitability, not mere compatibility; this bridge is one of the named step certificates that make the chain unconditional once T4 is in hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.