BalancedFloorRecognition
plain-language theorem explainer
Packages the T4 floor-recognition certificate: given that the Boolean cost of false is zero (balanced empty ledger), record that balance equation and a nonempty Boolean recognizer. Cited by the T2/T3→T4 bridge and the public forcing spine when discharging the recognition-witness step. Pure structure definition; no proof body.
Claim. A proposition depending on a hypothesis $h$ that the Boolean recognition cost of $\mathsf{false}$ is zero. It asserts two fields: the same balance equation $C(\mathsf{false})=0$, and that there exists a minimal recognizer pair $\mathsf{Recognize}(\mathsf{Bool},\mathsf{Bool})$ (a recognizer value paired with a recognized value).
background
This module is the public T-1 through T8 forcing spine. T-1 is the absolute distinguishability floor; T0 the Boolean recognition-work split; T1 the cost-form Meta-Principle; T2 two-state discreteness; T3 additive ledger bookkeeping; T4 the recognition witness on that discrete floor. The structure sits at the T4 interface.
The Boolean recognition cost is the concrete floor cost $C(a)=0$ if $a=\mathsf{false}$ and $1$ otherwise (nonnegative, with the usual dichotomy). Balance of the empty ledger is exactly $C(\mathsf{false})=0$. Upstream, $\mathsf{Recognize},A,B$ is the minimal recognizer→recognized pairing: a value of type $A$ paired with a value of type $B$. The Meta-Principle forbids Nothing recognizing itself; here both sides are Boolean, so the empty consistent state can recognize itself.
The UnifiedForcingChain twin states the same idea: "A balanced empty Boolean ledger supplies the minimal recognition witness."
proof idea
No proof: this is a structure (Prop-valued record). Fields are the balance hypothesis restated as source_balance and a Nonempty witness that a Boolean–Boolean recognizer exists. Instantiation is deferred to the companion theorem balanced_floor_recognition, which fills the fields by source_balance := hbalanced and recognition := ⟨⟨false, false⟩⟩ (empty point recognizing itself).
why it matters
T4 in the public spine needs an explicit recognition witness tied to the balanced ledger rather than inserted as a free sibling. Downstream, balanced_floor_recognition constructs the certificate, and T2_T3_To_T4_Bridge packages it: T2 supplies a nontrivial floor distinction, T3 the balanced empty ledger, and this structure is the recognition-witness field of that bridge. The UnifiedForcingChain twin records the same bridge role: the witness is "explicitly tied to the balanced ledger." That closes the T2/T3→T4 step on the way to T5 (J-uniqueness), T6 ($\varphi$), T7 (eight-tick), and T8 ($D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.