T0_T2_To_T3_Bridge
plain-language theorem explainer
Certificate that the pre-analytic ledger layer follows once logic-from-cost and discreteness are in hand. It packages empty-join neutrality, additive recognition work on independent Boolean joins, the two-state floor split, and the resulting T3 ledger record. Downstream complete-chain aggregates cite it to wire T0+T2 into T3 without ad-hoc case analysis. The object is a Prop-valued structure, not a proved theorem.
Claim. Given a $T_{-1}\to T_0$ bridge, a $T_0$ (logic-from-cost) certificate, and a $T_2$ (discreteness) certificate, a $T_0/T_2\to T_3$ bridge is a package asserting: (i) joining the empty consistent floor state is neutral, $\mathrm{join}(\bot,\Gamma)=\Gamma$ for every Boolean floor state $\Gamma$; (ii) recognition-work cost is additive on independent joins; (iii) every floor state is $\bot$ or $\top$; (iv) the $T_3$ ledger certificate holds (empty entry balanced, empty-join neutrality and cost-neutrality, independent additivity).
background
The Unified Forcing Chain module aims to show T0–T8 as forced from the cost foundation (Recognition Composition Law plus normalization and calibration), starting from an absolute floor. At the pre-analytic level, configurations live in a ConfigSpace: empty entry, binary join, consistency, and an independence relation for non-overlapping predicates.
$T_0$ says logic is the zero/positive split of recognition work: the consistent Boolean floor state has cost $0$, inconsistent states have positive cost, and independent joins add costs. $T_2$ says discreteness is that same floor split into two distinct Boolean states, with zero cost selecting only consistency. $T_3$ is the ledger bookkeeping of that work: empty consistent entry balanced, empty join left-neutral (and cost-neutral), and additivity on independent joins. The reciprocal scalar $J$ ledger is an analytic refinement later in the chain.
The $T_{-1}\to T_0$ bridge supplies the Boolean absolute-floor witness, normalized two-point floor, configuration interface, and unit-normalized recognition-work cost used by these fields.
proof idea
No proof body: this is a Prop-valued structure defining the bridge interface. Inhabitants are built by the companion theorem t0_t2_to_t3_bridge_holds, which fills fields by projection: empty-join neutrality from the floor config on the $T_{-1}\to T_0$ bridge, additivity from $T_0$'s independent-join law, the two-state split from $T_2$'s state dichotomy, and the $T_3$ ledger record assembled from those pieces. The structure itself only names the obligations.
why it matters
In the forcing ladder, $T_3$ (ledger) sits after logic and discreteness and before recognition observables, unique $J$, $\varphi$, the eight-tick octave, and $D=3$. This bridge is the explicit edge that $T_0$ plus $T_2$ force the ledger layer via cost symmetry bookkeeping on the Boolean floor, matching the module's claim that every level is forced rather than merely compatible.
It is consumed by CompleteForcingChain in this module and by CompleteForcingChainT8 / the parallel bridge in TMinus1ToT8Bridge, which thread the full $T_{-1}$–$T_8$ aggregate. The doc-comment stresses that $T_2$'s dichotomy lets empty-join neutrality be stated without raw case-splitting inside the chain. Note the honesty caveat on the longer $T_8$ aggregate: later $T_5$ uniqueness of $J$ does not substantively depend on the floor bridges beyond surface re-export; this certificate's job is the $T_3$ step, not analytic $J$-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.