BalancedFloorRecognition
plain-language theorem explainer
A Prop-structure packaging a balanced empty Boolean ledger (recognition cost of false is zero) with a nonempty Boolean self-recognition witness. Cited by anyone using the T2/T3→T4 bridge or the floor-to-recognition step of the unified forcing chain. As a structure definition it only records the two fields; the companion constructor fills them with the pair of empty points recognizing each other.
Claim. Given that the Boolean recognition cost of the empty configuration vanishes, $C(\mathsf{false})=0$, the structure asserts both that source-balance equation and that there exists a recognition map $\mathrm{Recognize}(\mathsf{Bool},\mathsf{Bool})$: a nonempty witness of Boolean self-recognition on the balanced empty floor.
background
The Unified Forcing Chain module aims to derive every level T-1 through T8 as forced from the cost foundation (Recognition Composition Law plus normalization and calibration). T-1 is the absolute floor: a meta-language Prop distinction in a non-singleton universe. T0 forces logic from cost minimization (consistency is cheap). T2 forces discreteness; T3 forces a ledger from cost symmetry $J(x)=J(1/x)$.
Boolean recognition cost is the discrete cost functional on the two-point floor $\mathsf{Bool}$. Balance of the empty configuration means $C(\mathsf{false})=0$: the empty consistent state carries no recognition work. A ledger is balanced when its event list is balanced; every constructed ledger is balanced by design.
T4 (Recognition) needs both a non-trivial floor distinction (from T2) and a balanced empty ledger state (from T3) from which a minimal recognition witness can be read. This structure is the certificate type for that packaging step: source balance plus a nonempty $\mathrm{Recognize},\mathsf{Bool},\mathsf{Bool}$.
proof idea
Definitional structure, not a proved theorem: two fields and no proof body. source_balance re-records the hypothesis $C(\mathsf{false})=0$. recognition is a Nonempty wrapper around a Boolean self-recognizer.
The companion constructor theorem balanced_floor_recognition builds an instance by setting source_balance to the given hypothesis and supplying the witness $\langle\mathsf{false},\mathsf{false}\rangle$: the balanced empty point recognizing itself on both sides. The recognizer field depends on the balance hypothesis only through that source-balance record.
why it matters
In the forcing chain, T4 (Recognition) is the step "ledger + observables." Earlier drafts inserted a free Boolean recognizer as a sibling assumption. This structure ties the witness explicitly to the balanced empty ledger from T3, so recognition is read off the floor rather than postulated.
Downstream, T2_T3_To_T4_Bridge requires a balanced_floor_recognition_cert field of this type (alongside a T2-sourced distinction and the T3 balance equation). The same pattern appears in the TMinus1ToT8Bridge module. The module doc frames the whole chain as complete inevitability from RCL + normalization + calibration; this certificate closes the T2/T3→T4 seam that feeds T5 (unique $J$), T6 ($\varphi$), T7 (eight-tick), and T8 ($D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.