BoolRecognitionCostFromFloor
plain-language theorem explainer
Packages the unit-normalization axioms for Boolean recognition-work cost on the absolute floor: empty/consistent state costs 0, the marked inconsistent state costs 1, and positive cost is exactly inconsistency. Anyone citing the T-1→T0 bridge or canonical two-point floor normalization needs this certificate. It is a pure Prop structure (definitional interface), not a proved theorem.
Claim. Given an absolute-floor witness on $\mathrm{Bool}$, the Boolean recognition-work cost $C$ is unit-normalized when: $C(\mathsf{false})=0$, $C(\mathsf{true})=1$, every inconsistent Boolean configuration has $C(\Gamma)=1$, and $0<C(\Gamma)$ if and only if $\Gamma$ is inconsistent (equivalently $C(\Gamma)=0$ iff $\Gamma$ is consistent).
background
The Unified Forcing Chain module aims to force T0–T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). The chain begins at T-1: an absolute floor, meaning a meta-language that can distinguish propositions and a non-singleton universe of discourse. An AbsoluteFloorWitness on a type $K$ records bare distinguishability and a nontrivial specification.
On $\mathrm{Bool}$, configurations form a two-point space with empty/consistent state $\mathsf{false}$ and marked inconsistent state $\mathsf{true}$. A configuration space supplies empty config, join, and an IsConsistent predicate. Recognition-work cost is the scalar assigned to each configuration; the Boolean instance is the minimal dichotomy cost used to reach T0 (logic from cost minimization: consistency is cheap).
Earlier bridges hid the scale choice $C(\mathsf{true})=1$ inside the definition of the Boolean cost. This structure externalizes that normalization so the T-1→T0 edge can cite an explicit certificate rather than a baked-in constant.
proof idea
No proof body: this is a structure (Prop bundle), not a theorem. It declares five fields that any inhabitant must supply: zero cost on empty, unit cost on the marked state, unit cost on every inconsistent Boolean, and the two iff characterizations linking positivity/zero to inconsistency/consistency. Downstream theorems such as bool_recognition_cost_from_floor discharge the fields mostly by rfl against the concrete Boolean cost definition, plus a short case split for the inconsistent-unit clause.
why it matters
This is the explicit scale-fixing step between bare T-1 distinguishability and T0 logic-from-cost. Downstream, CanonicalTwoPointFloorNormalization pairs it with the oriented Boolean configuration interface; TMinus1_To_T0_Bridge then packages floor witness, normalized floor, and recognition-work constraint into the non-vacuous T-1→T0 edge of the complete inevitability chain.
Without unit normalization on the marked inconsistency, cost minimization cannot force the logic dichotomy (consistency cheap, inconsistency unit-priced). The module claim is that T0 emerges from cost rather than being assumed; this structure is the named interface that makes that emergence checkable. It sits at the base of the forcing ladder that later yields unique $J$, $\varphi$, the eight-tick octave, and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.