forcedQuotientBoolEquiv_emp
plain-language theorem explainer
Under the forced quotient-to-Bool equivalence built from a distinction witness, the empty configuration is sent to false. Anyone transporting Boolean configuration-space structure onto the distinction quotient cites this as the unit case. The proof is a two-line simp: rewrite emp as the inverse image of false, then unfold the equivalence.
Claim. Let $K$ be any type admitting a distinction witness $h:\exists x,y\in K.\, x\neq y$. Write $Q_h$ for the forced observable quotient of $h$, and let $\Phi_h:Q_h\simeq\mathrm{Bool}$ be the forced coordinate equivalence. Then $\Phi_h(\mathrm{emp})=\mathsf{false}$, where $\mathrm{emp}$ is the empty configuration of the transported configuration space on $Q_h$.
background
This module opens Phase 1 of the T−1→T8 closure: given a distinction witness $h:\exists x,y:K.,x\neq y$, one builds the forced observable quotient $Q_h=\mathrm{Quotient}(\mathrm{forcedObservableSetoid},h)$ and proves it equivalent to $\mathrm{Bool}$. The point is to thread the witness through the early forcing spine rather than quoting unthreaded global Boolean facts.
A configuration space (CostFromDistinction) carries an empty configuration $\mathrm{emp}$, a binary join, consistency, and independence, with join a commutative monoid and $\mathrm{emp}$ the identity. The forced quotient-to-Bool map $\Phi_h$ is the noncomputable equivalence forcedQuotientBoolEquiv, aliasing the already-constructed forcedQuotientEquivBool. Transporting the Boolean configuration space across $\Phi_h$ yields a T0 recognition-work surface generated by the distinction itself.
This lemma pins the unit of that transport: $\mathrm{emp}$ on $Q_h$ must land on $\mathsf{false}$.
proof idea
Two-line tactic proof. First change rewrites the goal as $\Phi_h(\Phi_h^{-1}(\mathsf{false}))=\mathsf{false}$, using that $\mathrm{emp}$ is definitionally the inverse image of false under the equivalence. Then simp [forcedQuotientBoolEquiv] unfolds the equivalence and discharges the round-trip identity. No external lemmas beyond the definition of the equivalence are needed.
why it matters
Phase 1 of Distinction→T4 requires a full ConfigSpace instance on the forced quotient, not merely a bare equivalence to Bool. The empty-configuration law is the monoid-unit half of that instance; its sibling forcedQuotientBoolEquiv_join handles the binary join. Together they let recognition-work cost and the T0 surface be transported across $\Phi_h$, so later steps (T0_FromDistinction, distinction_forces_T0, and the T1 bridge) sit on a quotient generated by the supplied distinction rather than on a global Bool.
In the forcing chain this is scaffolding under T0: once the transported floor is in place, T1–T4 route through it. No downstream theorems currently depend on this simp lemma by name, but it is the unit clause any such transport proof must invoke.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.