T2_T3_To_T4_Bridge
plain-language theorem explainer
Packages the T2+T3 to T4 step of the unified forcing chain: discreteness plus a balanced empty ledger force recognition on the Boolean floor. Anyone assembling the complete forcing chain cites this certificate. It is a Prop-structure of named fields, not a proved theorem; the companion inhabitant theorem fills the fields from T2 and T3.
Claim. Given discreteness is forced (Boolean floor states exhaustive and distinct; zero cost selects only consistency) and the ledger is forced (empty consistent entry has cost zero; empty join neutral), one obtains a bridge certificate: the normalized two-point recognition floor on $\mathrm{Bool}$; a non-trivial Boolean distinction; balanced empty ledger $C(\mathsf{false})=0$; a balanced-floor recognition certificate; balance implies a nonempty witness $\mathrm{Recognize}(\mathrm{Bool},\mathrm{Bool})$; that implication equals the named balanced-ledger theorem; hence recognition is forced (T4).
background
The Unified Forcing Chain module argues that T-1 through T8 are inevitabilities from the cost foundation (Recognition Composition Law plus normalization and calibration), not merely compatible layers. At the pre-analytic floor, configurations are Boolean: false is the empty/consistent entry and true the marked inconsistent entry, with recognition-work cost C on that carrier.
T2 (discreteness forced) asserts state dichotomy, distinctness of the two floor states, and that zero cost selects only consistency. T3 (ledger forced) asserts that the empty consistent entry is zero-cost and that empty joins are neutral on states and costs. A normalized two-point recognition floor packages exhaustiveness, a marked point distinct from empty, unit-normalized cost, and an equivalence showing Bool is only the canonical representative.
T4 (recognition forced) needs both a non-trivial discrete distinction and a recognition witness on the floor carrier. Balanced-floor recognition reads the minimal Boolean recognizer off the balance equation C(false)=0, rather than inserting recognition as a free sibling of the ledger.
proof idea
No proof body: this is a structure definition (a Prop bundling fields). The mathematical content is the interface itself. Downstream, the inhabitant theorem fills every field: normalized floor from the Boolean two-point floor lemma; distinction as the pair false, true via T2 state distinctness; balanced ledger from T3 empty-balanced; the balanced-floor recognition certificate from the constructor on that balance equation; and T4 assembled from those pieces. Treat this declaration as the named certificate type, not as a derivation step.
why it matters
In the forcing chain diagram, T4 is Recognition from ledger plus observables. Earlier presentations hid the two ingredients; this bridge makes them explicit: T2 supplies the non-trivial floor distinction, T3 the balanced empty ledger from which the floor recognition witness is read. The witness remains the minimal Boolean recognizer, now tied to the balanced ledger rather than a free sibling.
Downstream parents are the complete forcing chain records in this module and in the T-1-to-T8 bridge, plus the inhabitant theorems that build this structure. Those complete-chain records thread T-1 through T8; this structure is the T2/T3 to T4 edge type they require. It sits before T5 (unique J), T6 (phi), T7 (eight-tick), and T8 (D=3). Note the honesty audit on the T8 complete chain: T5 uniqueness is proved from cost-uniqueness lemmas and does not consume the T-1..T4 floor beyond re-export; this bridge still matters for the floor narrative and for any claim that recognition is forced before the analytic J layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.