t0_t2_to_t3_bridge_holds
plain-language theorem explainer
Given the T-1→T0 bridge, forced logic (T0), and forced discreteness (T2), the T0/T2→T3 bridge certificate is inhabited: empty-join neutrality, independent-join additivity, and the pre-analytic ledger payload all follow. Anyone assembling the complete T-1–T8 forcing chain cites this edge before claiming the ledger layer. The proof wires floor join laws and T0 additivity, then case-splits on the Boolean dichotomy for empty-join identities.
Claim. If the absolute-floor to logic bridge is available, logic is forced (consistent floor states have zero recognition-work cost; independent joins are additive), and discreteness is forced (every floor state is one of the two Boolean values), then the T0/T2→T3 bridge holds: joining with the empty/consistent state is the identity, independent joins add costs, and the pre-analytic ledger structure (empty balance, empty-join neutrality, additive independent joins) is forced.
background
The Unified Forcing Chain module aims to show every step T-1 through T8 is forced from the cost foundation (Recognition Composition Law plus normalization and calibration), not merely compatible. T3 is the ledger layer: before analytic $J$ appears, the ledger is the recognition-work bookkeeping on Boolean floor configurations, with empty-join neutrality and additive independent joins.
T0 packages logic as the zero/positive split of recognition work: consistency is cheap ($C(\mathsf{false})=0$), contradiction is expensive. T2 packages discreteness as the Boolean floor split: every state is $\mathsf{false}$ or $\mathsf{true}$, and zero cost selects only the consistent state. The T-1→T0 bridge supplies the concrete Boolean floor configuration and its empty-join law from the absolute-floor witness.
The bridge certificate T0/T2→T3 records exactly the interface the chain needs: floor empty-join from the Boolean config, T0 additivity, the T2 dichotomy as a reusable split, and a filled T3 ledger payload. Downstream t3_holds extracts that payload unconditionally once the prior bridges are closed.
proof idea
Structure construction, not a deep calculation. Empty-join is copied from the T-1→T0 bridge floor config (empty_join_left). Independent-join additivity is copied from T0 (additive_indep). The floor split field is T2's state_dichotomy.
The nested T3 payload is assembled fieldwise: empty balance from T0's consistency_cheap; independent-join additivity again from T0. For empty-join left and empty-join cost neutrality, introduce an arbitrary Boolean configuration $\Gamma$, case-split on T2's dichotomy ($\Gamma=\mathsf{false}$ or $\Gamma=\mathsf{true}$), and in each branch rewrite or simpa with the floor empty-join identity. No new arithmetic: the dichotomy removes ad-hoc case analysis from later chain steps.
why it matters
This is the certified edge from forced logic and forced discreteness into the ledger layer of the complete inevitability chain. Parent consumers include t3_holds ("T3 holds on the pre-analytic recognition-work ledger"), which is literally (t0_t2_to_t3_bridge_holds ...).t3, and t4_holds, which threads the same bridge before recognition is forced. Both complete_forcing_chain and the T-8-length chain assembly depend on this step.
In the primer forcing ladder, T3 is the ledger forced by cost symmetry structure (later analytic $J(x)=J(1/x)$ sits on this discrete bookkeeping). Without a non-vacuous T0/T2→T3 bridge, the chain would jump from discreteness to recognition with a gap. Closing this edge keeps the stronger claim: every level is forced from the cost foundation, not assumed. It does not yet pin unique $J$ (T5), $\varphi$ (T6), the eight-tick octave (T7), or $D=3$ (T8); those sit further down the same chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.