forcedQuotientConfigSpace
plain-language theorem explainer
Given any type carrying a distinction witness, the forced observable quotient inherits a full configuration-space structure by transporting the Boolean one across the quotient–Bool equivalence. Researchers closing the T−1→T0 floor from a concrete distinction cite this instance as the ambient algebra of configurations. Fields are defined by push/pull along the equivalence; monoid and consistency laws reduce to finite Bool case analysis.
Claim. Let $K$ be any type with a distinction witness $h:\exists x,y\in K,\,x\neq y$, and let $Q_h$ be the forced observable quotient of $K$ under $h$. Transporting the Boolean configuration space along the canonical equivalence $Q_h\simeq\mathrm{Bool}$ equips $Q_h$ with empty configuration, binary join, a consistency predicate, and an independence relation satisfying the configuration-space axioms (commutative monoid laws for join with empty identity, symmetry of independence, and the join–consistency compatibility rules).
background
This module opens the closure path from a supplied distinction witness to the early forcing spine (Phase 1 of T−1→T8). From $h:\exists x,y:K,,x\neq y$, the upstream construction builds the forced observable quotient $Q_h=\mathrm{Quotient}(\text{forcedObservableSetoid},h)$ and proves it equivalent to $\mathrm{Bool}$. The point is to thread that witness rather than reuse a global Boolean chain.
A configuration space (from CostFromDistinction) is an abstract algebra of configurations: an empty configuration, a binary join, a consistency predicate, and an independence relation. The laws require join to be a commutative monoid with empty as identity, independence to be symmetric with empty independent of everything, and join of independent consistent pieces to stay consistent (with the usual inconsistency-propagation rules).
The forced quotient–Bool coordinate equivalence supplies the transport map used here. All structure on $Q_h$ is the Boolean structure pulled back along that equivalence.
proof idea
Define the four fields by transport: empty is the preimage of $\mathrm{false}$; join is Boolean OR conjugated by the equivalence; consistency means the Bool coordinate is $\mathrm{false}$; independence means at least one side has Bool coordinate $\mathrm{false}$.
Each law is proved by reducing along the equivalence. Empty-consistency and empty-independence are immediate simplifications. Independence symmetry is a one-line Or swap. Commutativity, associativity, and empty-join of join use injectivity of the equivalence plus exhaustive case splits on the two (or three) Bool coordinates, then simp. The two join–consistency compatibility lemmas rewrite the joined coordinate as an OR and discharge by the same Bool cases (including an exfalso branch when a side is forced true).
why it matters
This instance is the algebraic floor on which the module builds a T0 recognition-work surface generated by the distinction itself, rather than by unthreaded global Bool facts. Downstream siblings (recognition-cost transport, the recognition-work constraint, and the T0-from-distinction theorems) sit on this ConfigSpace instance.
In the Recognition forcing chain, T0 is the recognition-work / cost surface that later forces J-uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8). Phase 1 of the T−1→T8 closure needs that surface to live on the quotient forced by a concrete distinction witness; this declaration supplies exactly that carrier. Without it, later T1–T4 routing would still lean on a global Boolean configuration space disconnected from the witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.