T4_To_T5_Realization_Bridge
plain-language theorem explainer
Interface packaging the T4-to-T5 step: from a forced Boolean recognition floor one obtains LogicRealization data, Peano-arithmetic invariance across positive-ratio realizations, and an RCL surface (multiplicative consistency of the derived cost with bilinear combiner). Cited by the complete T−1..T8 spine and the cost-bridge that re-exports the surface. Pure structure definition; inhabitants are built by t4_to_t5_bridge_holds.
Claim. Given a forced T4 Boolean recognition floor, the T4-to-T5 realization bridge asserts: nonempty recognition on $\mathrm{Bool}$ and a pair of distinct Booleans; a nonempty floor $\mathrm{LogicRealization}$; for every comparison operator $C$ satisfying the laws of logic, a nonempty positive-ratio realization; the Peano carriers extracted from the floor and positive-ratio realizations are equivalent; and the derived cost of $C$ admits multiplicative consistency $F(xy)+F(x/y)=P(F(x),F(y))$ with $P(u,v)=2u+2v+c\,uv$ for some $c$.
background
The module is the public T−1 through T8 forcing spine. T4 is the recognition witness on the discrete Boolean floor; T5 is uniqueness of the canonical reciprocal cost $J$. The hypothesis T4_Recognition_Forced packages floor distinction, nonempty Boolean recognition, a recognition structure with universe $\mathrm{Bool}$, and a zero-cost recognition clause.
A comparison operator is a map $\mathbb{R}{>0}\times\mathbb{R}{>0}\to\mathbb{R}$. Its derived cost fixes the second argument at $1$. Satisfying the laws of logic means the four Aristotelian constraints plus scale invariance, route independence, and non-triviality. A LogicRealization supplies carrier, cost type, comparison, and identity/step data from which Universal Forcing extracts Peano arithmetic.
Multiplicative consistency (d'Alembert) is $F(xy)+F(x/y)=P(F(x),F(y))$ for positive $x,y$. The RCL surface here specializes $P$ to the bilinear form $2u+2v+c,uv$, the algebraic shape of the Recognition Composition Law before $J$-uniqueness.
proof idea
Definitional structure with empty proof body: six Prop fields, no tactics. The canonical inhabitant is the noncomputable def t4_to_t5_bridge_holds, which copies floor recognition and distinction from the T4 hypothesis, wraps T4ToT5.floorRealization and T4ToT5.positiveRatioRealization, and supplies the arithmetic-equivalence and RCL-surface witnesses from the T4ToT5 construction namespace. Downstream cost-bridge theorems only re-export rcl_surface.
why it matters
Occupies the T4→T5 arrow in both CompleteForcingChainT8 and UnifiedForcingChain.CompleteForcingChain, and is the hypothesis of T4_To_T5_Cost_Bridge. Framework landmark: T5 $J$-uniqueness ($J(x)=(x+x^{-1})/2-1$), with RCL as the functional equation surface.
Honesty note on the parent chain: T5 uniqueness is proved from CostUniqueness lemmas and law_of_logic_forces_jcost; it consumes nothing from this bridge beyond re-exporting rcl_surface. Deleting T−1..T4 would break no T5 proof. The open gap is that the floor's own cost cannot itself satisfy the RCL surface in a way that feeds uniqueness—the bridge records interface data, it does not close that feed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.