T0_T2_To_T3_Bridge
plain-language theorem explainer
The T0/T2→T3 bridge certificate packages what forces additive ledger bookkeeping on the Boolean recognition floor: empty-join neutrality, cost additivity on independent joins, the two-state split, and the resulting T3 ledger record. Anyone wiring the public T−1..T8 forcing spine cites it when attaching T3 to the complete chain. It is a pure Prop interface; the companion inhabitance theorem fills every field from prior T0 and T2 data.
Claim. Given a bridge from the absolute distinguishability floor to T0, a certificate that logic is the zero/positive split of recognition work, and a certificate that the floor is two-state discrete, the bridge asserts four facts on the Boolean floor: joining the empty configuration leaves any state $\Gamma$ unchanged; recognition cost is additive under independent joins; every state is $\mathsf{false}$ or $\mathsf{true}$; and the additive ledger layer (T3) holds.
background
This module is the public T−1 through T8 forcing spine. T0 is the Boolean recognition-work split (zero cost on the consistent empty state, positive cost on inconsistency). T2 is two-state discreteness of that floor. T3 is additive ledger bookkeeping: empty cost zero, empty join as identity, cost-neutral empty joins, and additivity on independent joins.
A configuration space supplies an empty configuration, a binary join, consistency, and an independence relation (no shared predicates), with join a commutative monoid. The concrete Boolean cost is $C(\mathsf{false})=0$ and $C(\mathsf{true})=1$. The T−1→T0 bridge already hands the absolute Boolean floor, its config laws, and that cost. T0 records recognition-work constraints and additivity over independent joins; T2 records the dichotomy, distinctness of the two states, and the zero/positive cost selectors.
proof idea
No proof body: this is a Prop structure, not a theorem. It declares four fields that a later inhabitance proof must supply: empty-join left-identity on Bool, T0-style cost additivity under Independent, the T2 state dichotomy, and a full T3 ledger certificate.
The companion theorem constructs an instance by projection: empty-join from the T−1→T0 floor config, additivity from T0's independent-join law, and the floor split from T2's state dichotomy, then assembles T3 from those pieces. No new arithmetic is done at the structure itself.
why it matters
T3 is the additive ledger step on the public forcing spine (MODULE_DOC: T3 = additive ledger bookkeeping). Downstream, CompleteForcingChain and CompleteForcingChainT8 both thread this bridge so the chain can step from the discrete Boolean floor to ledger neutrality without ad-hoc case splits.
The UnifiedForcingChain copy states the design intent directly: T0 supplies recognition-work additivity over independent joins, while T2 supplies the Boolean floor split used to prove empty-join neutrality. That is exactly the T0/T2→T3 arrow in the T0–T8 forcing chain, before T4 (recognition witness), T5 (J-uniqueness), T6 ($\varphi$), T7 (eight-tick), and T8 ($D=3$).
The honesty note on CompleteForcingChainT8 concerns the later T4→T5 arrow, not this bridge: T3 still depends substantively on the floor data packaged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.