canonical_two_point_floor_normalization
plain-language theorem explainer
Given any absolute-floor witness on Bool, there is a canonical normalization that orients the two-point distinction as empty/marked and assigns unit recognition work to the single marked inconsistency. Anyone citing the T-1→T0 edge of the unified forcing chain needs this certificate. The proof is a four-field term record assembling existing Boolean floor config, cost, work-constraint, and normalized-floor witnesses.
Claim. For every absolute-floor witness $F$ on $\mathrm{Bool}$ (meta-language distinguishability plus a nontrivial specification of $\mathrm{Bool}$), there exists a canonical two-point floor normalization of $F$: an oriented Boolean configuration, a unit-normalized Boolean recognition cost, a recognition-work constraint certificate for that cost, and the abstract normalized two-point floor represented by $\mathrm{Bool}$.
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 two propositions and a non-singleton universe of discourse. An AbsoluteFloorWitness on a type $K$ packages exactly those two facts.
Bare T-1 distinguishability does not name false/true, Boolean join, or a unit cost scale. The structure CanonicalTwoPointFloorNormalization is the explicit normalization step: orient the Boolean floor as empty/marked and assign unit recognition work to the one marked inconsistency. Sibling constructors supply the oriented config from the witness, the unit-normalized Boolean recognition cost, the work-constraint certificate (dichotomy and independent additivity), and the abstract normalized two-point floor on Bool.
This sits just above Absolute Floor Closure and just below the Logic-from-Cost T0 payload: once the Boolean floor carries a concrete recognition-work cost, consistency-is-cheap can force classical logic.
proof idea
Term-mode record construction, not a tactic script. The four fields of CanonicalTwoPointFloorNormalization are filled by four already-proved sibling witnesses:
configfrombool_floor_config_from_witness floor(oriented empty/marked Boolean interface).costfrombool_recognition_cost_from_floor floor(unit-normalized Boolean recognition cost).recognition_workfrom the existingbool_recognition_work_constraint(nonempty recognition-work constraint cert on Bool).normalized_two_pointfrombool_normalized_two_point_floor(abstract normalized two-point floor).
No new algebra is done here; the theorem is the packaging that turns those four pieces into the single certificate the T-1→T0 bridge consumes.
why it matters
This is the non-vacuous edge that was missing from older aggregate closures. Downstream, tminus1_to_t0_bridge and tminus1_to_t0_bridge_holds cite it as the normalized_floor field: the absolute floor supplies the Boolean distinction; that distinction carries a concrete recognition-work cost satisfying dichotomy and independent additivity; and the LogicFromCost T0 payload is then reached through this cost/consistency interface.
In the forcing chain this is the T-1 → T0 step: absolute floor (meta-language Prop distinction + non-singleton universe) to logic forced by cost minimization ("consistency is cheap"). Without the unit-cost orientation, T-1 is only bare distinguishability and cannot feed the analytic cost refinement or the rest of T0–T8. It does not itself force φ, the eight-tick octave, or D=3; those arrive later (T5–T8) once unique J and the discrete ledger are in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.