balanced_floor_recognition
plain-language theorem explainer
From a balanced empty Boolean ledger (recognition cost of false equals zero), one obtains the minimal recognition package: the balance equation plus a nonempty Bool-to-Bool recognizer. Cited by the T2–T3→T4 bridge and by the absolute-floor recognition extraction. Proof is a structure inhabitant whose recognizer is the self-pair (false, false), threaded through an if-by-hypothesis so the balance assumption is formally consumed.
Claim. If the Boolean-floor recognition cost of the empty state vanishes, $C(\mathsf{false})=0$, then there is a balanced-floor recognition package consisting of that balance equation together with a nonempty witness $\mathsf{Recognize}(\mathsf{Bool},\mathsf{Bool})$, realized by the self-recognition pair $(\mathsf{false},\mathsf{false})$.
background
The Unified Forcing Chain module aims to force every level T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). T4 is Recognition: a ledger plus observables yields a recognition event. The absolute floor supplies a two-point Boolean configuration space before analytic cost is introduced.
The Boolean recognition-work cost is the CostFunction on Bool with $C(\mathsf{false})=0$ and $C(\mathsf{true})=1$. Balance of the empty ledger is exactly $C(\mathsf{false})=0$. The structure BalancedFloorRecognition packages that balance hypothesis with a field recognition : Nonempty (Recognize Bool Bool): a nonempty pair of Boolean states standing as the pre-analytic recognition event.
Upstream, LedgerForcing treats a ledger as balanced when its event list balances; the empty Boolean case is the floor instance used here. The bridge modules (TMinus1ToT1, TMinus1ToT8) share the same cost and the same packaging pattern.
proof idea
Term-mode structure construction, not a multi-step tactic proof. The source_balance field is definitionally the input hypothesis hbalanced. The recognition field is built by an if _ : C false = 0 then ... else ... projection whose both branches inhabit Nonempty (Recognize Bool Bool) by the pair ⟨⟨false, false⟩⟩ (empty state recognizing itself). The conditional exists only so the recognizer construction formally depends on the balance hypothesis; the inhabitant is identical on both branches. No external lemmas are applied beyond the structure and the cost definition.
why it matters
This is the T4 seed on the absolute floor: recognition as the empty consistent state recognizing itself once the ledger is balanced. Downstream, recognition_from_balanced_floor_ledger projects out the nonempty recognizer, and balanced_floor_recognition_source_balance records that the package carries its balance source definitionally.
The parent bridge t2_t3_to_t4_bridge_holds uses this certificate: T2 supplies a distinction (false ≠ true) and T3 supplies the empty balanced ledger; this theorem turns that balance into the recognition witness field of the T2–T3→T4 bridge. Parallel copies live in TMinus1ToT8Bridge. In the forcing chain landmarks, this closes the step from T3 (ledger from cost symmetry $J(x)=J(1/x)$) into T4 (recognition), before T5 forces unique $J$ and T6 forces $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.