IndisputableMonolith.Foundation.TMinus1ForcedFromDistinction
From a distinction witness one extracts a marked pair and forces the T-1 Boolean floor: an observable setoid, a nontrivial quotient, and a canonical equivalence with Bool. Recognition auditors cite this when closing the path from raw distinction to the early forcing spine. The argument wires a mark-based Boolean projection to an observable-floor witness so the two-valued quotient is forced rather than assumed.
claimGiven a distinction witness on a carrier, extract a marked pair $(a,b)$ with $a \neq b$, induce an observable setoid and floor, form the nontrivial quotient, and obtain a canonical equivalence between that quotient and $\mathrm{Bool}$.
background
The T-1 Boolean floor is the earliest layer of the Recognition forcing spine. Before J-cost uniqueness, $\varphi$, the eight-tick octave, or $D=3$, one needs a genuine two-valued distinction that is observationally meaningful, not merely a raw type-theoretic inequality.
ObservableFloorWitness records Anil Thapa's T-1 audit: gauge-related or observationally equivalent representatives can be unequal as terms while physically indistinguishable. An observable floor is therefore a pair of notions that separates term inequality from physical distinguishability. BooleanProjectionFromMark adds that the Boolean floor is canonical only after a distinguishing mark has been chosen; a non-singleton carrier supplies at least one two-point shadow, but a larger carrier does not choose that shadow uniquely.
This module starts from a supplied distinction witness, extracts the marked pair it carries, and forces the projection, setoid, floor, and quotient equivalence to Bool.
proof idea
Definition-and-construction module, not a single theorem. It first extracts the marked pair from the distinction witness, then builds the forced Boolean projection (base and alternate forms) via the mark. From that projection it defines the forced observable setoid and floor, proves the quotient is nontrivial, constructs the quotient-to-Bool map and a Boolean representative with a left-inverse law, and packages the canonical equivalence between the forced quotient and Bool.
why it matters in Recognition Science
Feeds DistinctionToT4, which "starts the real closure path from a supplied distinction witness to the early forcing spine" and insists on not returning a global Bool chain while ignoring the witness. Without this module, T-1 would either smuggle in raw type inequality or assume Bool rather than force it from distinction. It closes the observable-floor gap identified in the T-1 audit and supplies the Boolean base that later spine steps (toward T4 and the T0–T8 chain) can cite when a witness is in hand.
scope and limits
- Does not derive the distinction witness; the witness is an input hypothesis.
- Does not force uniqueness of the mark on carriers larger than two points.
- Does not reach J-cost uniqueness, $\varphi$, eight-tick structure, or $D=3$.
- Does not identify the observable setoid with a physical gauge beyond the supplied floor witness.
- Does not close the full path to T4; that lives in the downstream module.
used by (1)
depends on (2)
declarations in this module (19)
-
def
markedPairOfDistinction -
def
forcedBoolProjection -
theorem
forcedBoolProjection_base -
theorem
forcedBoolProjection_alt -
def
forcedObservableSetoid -
theorem
forcedObservableFloor -
theorem
forcedQuotientNontrivial -
def
forcedQuotientToBool -
def
forcedBoolRepresentative -
theorem
forcedQuotientToBool_representative -
theorem
forcedBoolRepresentative_left_inv -
def
forcedQuotientEquivBool -
structure
ForcedBooleanCoordinates -
def
canonicalForcedBooleanCoordinates -
def
forcedBooleanCoordinateChange -
theorem
forcedBooleanCoordinates_unique_up_to_bool_aut -
theorem
rawFloor_forced_from_distinction -
theorem
booleanObservableFloor_forced_from_distinction -
theorem
bool_distinction