T2_T3_To_T4_Bridge
plain-language theorem explainer
Bridge certificate from two-state discreteness (T2) and additive ledger balance (T3) to a recognition witness on the Boolean floor (T4). Anyone assembling the public T-1..T8 forcing spine cites this Prop bundle. It is a structure definition whose fields package distinction, zero-cost empty ledger, a balanced-floor recognition certificate, and the T4 record; the companion inhabitance theorem fills the fields from T2/T3 hypotheses.
Claim. Given a proof that the Boolean floor is two-state discrete and a proof that the Boolean ledger is additive with balanced empty state, the bridge asserts: there exist distinct Booleans $a \neq b$; the empty ledger has recognition cost $C(\mathrm{false})=0$; that balance yields a balanced-floor recognition certificate; $C(\mathrm{false})=0$ implies a nonempty recognition witness on $\mathrm{Bool}$; and recognition on the discrete floor is forced (T4).
background
The module is the public T-1 through T8 forcing spine: absolute distinguishability floor, Boolean recognition-work split, cost-form Meta-Principle, two-state discreteness, additive ledger bookkeeping, then recognition witness, J-uniqueness, phi, eight-tick cadence, and D = 3. It stops before private operator and measurement layers.
The Boolean recognition-work cost is the concrete floor cost with C(false) = 0 and C(true) = 1. T2 packages state dichotomy, distinctness of false and true, and the selection rules that zero cost picks consistency while positive cost picks the marked state. T3 packages empty balance C(false) = 0, left-unit join, cost neutrality of joining empty, and independent-join additivity.
BalancedFloorRecognition is the intermediate certificate: given C(false) = 0, it records source balance and a nonempty Recognize Bool Bool. T4 is the forced recognition record: floor distinction, nonempty recognition, a recognition structure with universe Bool, and the zero-cost implication to a recognition witness.
proof idea
No proof body: this is a Prop-valued structure definition. Fields are the mathematical obligations of the T2/T3 to T4 arrow: distinction extracted from T2, balance extracted from T3, a BalancedFloorRecognition certificate on that balance, the zero-cost implies recognition implication, and the assembled T4 record.
Inhabitance is supplied by the sibling theorem that fills distinction from T2 states_distinct, balance from T3 empty_balanced, the balanced-floor cert via the balanced_floor_recognition constructor, and builds the remaining fields from those.
why it matters
Closes the T2/T3 to T4 step on the public forcing spine. Downstream, CompleteForcingChainT8 and the unified CompleteForcingChain consume this bridge so the chain can list T4 after discreteness and ledger without smuggling a free recognition witness. The UnifiedForcingChain twin states the intent directly: T4 needs both ingredients that were previously hidden; T2 supplies a nontrivial floor distinction, and T3 supplies the balanced empty ledger from which the floor recognition witness is read.
In the primer landmarks this is the pre-T5 segment: recognition on the discrete balanced floor, before J-uniqueness (T5), phi (T6), eight-tick (T7), and D = 3 (T8). The honesty note on CompleteForcingChainT8 records that T5 uniqueness does not consume this floor bridge beyond re-export; the bridge still matters for an honest T4 placement in the spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.