CanonicalTwoPointFloorNormalization
plain-language theorem explainer
Packages the explicit normalization of the absolute Boolean floor into a two-point recognition floor: empty/marked orientation, unit cost on the single inconsistency, and a recognition-work certificate. Anyone citing the T-1→T0 bridge needs this bundle so bare distinguishability is not smuggled into Boolean names or a hidden cost scale. As a structure it is a Prop certificate, not a proved theorem.
Claim. Given an absolute-floor witness on $\mathrm{Bool}$, a canonical two-point floor normalization is a bundle of four facts: (i) the witness orients as the empty/marked Boolean configuration interface; (ii) recognition cost is unit-normalized with $C(\mathrm{false})=0$ and $C(\mathrm{true})=1$; (iii) that cost admits a recognition-work constraint certificate (dichotomy and independent additivity); (iv) $(\mathrm{Bool},\mathrm{true},C)$ is a normalized two-point recognition floor under the identity equivalence.
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). T-1 is the absolute floor: a meta-language that can distinguish propositions together with a non-singleton universe of discourse. An AbsoluteFloorWitness on a type $K$ records bare distinguishability and a nontrivial specification; it does not yet name Boolean values or fix a cost scale.
The T-1→T0 step needs more. A cost function on a configuration space obeys dichotomy (cost zero iff consistent) and independent additivity over joins that share no predicates. The recognition-work constraint certificate packages such a cost with empty-cost zero and a calibrated positive cost on a chosen inconsistency. Sibling structures convert the Boolean absolute-floor witness into an empty/marked ledger interface and pin $C(\mathrm{true})=1$. The abstract normalized two-point floor is the same data up to equivalence with $\mathrm{Bool}$: one empty point, one marked point, unit cost, exhaustive dichotomy.
proof idea
No proof body: this is a structure (Prop bundle), not a theorem. Inhabitants are assembled fieldwise. The downstream constructor canonical_two_point_floor_normalization fills the four fields by applying bool_floor_config_from_witness, bool_recognition_cost_from_floor, the Boolean recognition-work constraint from the T-1→T0 interface, and the corresponding normalized two-point floor instance (identity equivalence on $\mathrm{Bool}$). Each field is itself a named certificate already proved or packaged elsewhere in the module.
why it matters
This is the explicit normalization edge that older aggregates left implicit. Bare T-1 distinguishability does not contain the labels false/true, Boolean join, or unit cost; without this certificate those choices hide inside definitions. Downstream, TMinus1_To_T0_Bridge requires a Boolean absolute-floor witness plus this normalized floor, then routes through the cost/consistency interface into the Logic-from-Cost T0 payload ("consistency is cheap"). That bridge is the non-vacuous missing edge of the complete inevitability chain: T-1 absolute floor → T0 logic forced by cost minimization. It sits at the base of the forcing chain 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.