t2_t3_to_t4_bridge_holds
plain-language theorem explainer
Given forced discreteness (T2) and a forced ledger (T3) on the Boolean recognition floor, the T2/T3→T4 bridge certificate is inhabited, so recognition (T4) follows. Anyone assembling the complete T−1…T8 inevitability chain cites this step. The proof is a term-mode structure fill: Boolean two-point floor, empty balanced ledger, recognition witness, and the T4 corollary of T2+T3.
Claim. Assume discreteness is forced: the pre-analytic floor is Boolean, the two states are distinct, and zero cost selects only the consistent state. Assume the ledger is forced: the empty consistent entry has cost zero and empty joins are neutral. Then the T2/T3$\to$T4 bridge holds: the normalized two-point recognition floor is available, T2 supplies a nontrivial distinction, T3 supplies the balanced empty ledger, floor recognition is certified from that balance, and recognition itself is forced as a corollary.
background
The module Unified Forcing Chain proves that every level T−1 through T8 is forced from the cost foundation (Recognition Composition Law plus normalization and calibration), not merely compatible with it. At this stage the analytic $J$-cost has not yet appeared; the floor is the Boolean configuration space with recognition cost that marks consistency (false) as zero-cost and inconsistency (true) as positive-cost.
T2 (discreteness forced) packages the dichotomy: every floor state is one of the two Booleans, the states are distinct, and zero cost selects only consistency. T3 (ledger forced) packages additive bookkeeping at that floor: the empty consistent entry has cost zero, and empty joins are identity and cost-neutral. The reciprocal scalar ledger is an analytic refinement later.
T4 needs both ingredients that earlier presentations left implicit. Upstream, bool_normalized_two_point_floor identifies the concrete Boolean floor as the canonical normalized two-point recognition floor; balanced_floor_recognition turns empty-balance into a recognition witness; recognition_from_balanced_floor_ledger packages that witness as nonempty recognition data.
proof idea
Term-mode construction of the bridge structure. The normalized floor field is the canonical Boolean two-point floor theorem. Distinction is the pair (false, true) with T2's states_distinct. Balanced ledger is T3's empty_balanced (cost of false is zero). The balanced-floor recognition certificate is balanced_floor_recognition applied to that empty balance; recognition-from-balanced-ledger is the corresponding upstream implication. Equality of the recognition packaging is rfl. The T4 field is the corollary that recognition is forced from T2 and T3 together.
why it matters
This is the explicit T2+T3$\to$T4 link in the complete inevitability chain. Downstream, t4_holds builds T2 and T3 from earlier bridges and applies this certificate to obtain T4 (recognition forced on the pre-analytic floor). The same step is threaded into complete_forcing_chain and the T−1…T8 bridge's complete_forcing_chain_t8.
In the module's forcing ladder, T4 is "Recognition ← Ledger + observables": without a nontrivial floor distinction (T2) and a balanced empty ledger state (T3), the recognition witness would be a free sibling rather than a forced readout. Closing this bridge keeps the chain gap-free before T5 (unique $J$), T6 ($\varphi$ as self-similar fixed point), T7 (eight-tick octave), and T8 ($D=3$). No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.