ForcedQuotient
plain-language theorem explainer
Given a type with a distinction witness (two unequal elements), the forced observable quotient is the two-class partition induced by the forced Boolean projection of that witness. Foundation proofs cite it as the carrier for the T−1 floor generated by the witness itself, not by a global Bool. The declaration is a one-line abbreviation of the quotient by the forced observable setoid.
Claim. For any type $K$ and witness $h:\exists x,y\in K,\,x\neq y$, the forced observable quotient of $h$ is the quotient set $K/\sim_h$, where $x\sim_h y$ if and only if the forced Boolean projection of $h$ takes the same value at $x$ and at $y$.
background
The module closes the early forcing spine from a supplied distinction witness rather than from an unthreaded global Boolean chain. A distinction witness on a type $K$ is simply a proof that two elements of $K$ are unequal. From that witness, the upstream construction forcedObservableSetoid builds the equivalence relation that identifies points exactly when the forced Boolean projection agrees on them.
The present abbreviation names the corresponding quotient set. Upstream, that setoid is already proved to be an equivalence; the Boolean projection itself is forced by the existence of a marked pair of unequal elements. The local goal is Phase 1 of the T−1→T8 closure: equip this quotient with a transported configuration space and recognition-work cost so that later T0–T4 facts live on the witness-generated floor.
proof idea
One-line abbreviation: the carrier is exactly the Lean quotient of $K$ by the forced observable setoid of the distinction witness. No further proof obligations; all setoid laws are discharged upstream in the construction of that setoid.
why it matters
This carrier is the floor on which the module transports Boolean configuration space and recognition-work cost. Downstream, the forced quotient–Bool equivalence, the transported ConfigSpace instance, the recognition-cost function, and the recognition-work constraint are all typed over it. The completed early spine structure packages those facts as “the supplied distinction forces the T−1 floor and T0–T3 on its own observable quotient.”
In the Recognition forcing chain this is the concrete T−1 object generated by distinction alone, before T5 J-uniqueness, T6 φ, T7 eight-tick, and T8 D=3. It keeps the closure path honest: later steps must route through the witness quotient rather than smuggle in global Bool facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.