forcedQuotientBoolEquiv_join
plain-language theorem explainer
Under the forced quotient-to-Bool equivalence induced by a distinction witness, join of configurations maps to Boolean OR. Anyone transporting ConfigSpace structure or recognition-work cost from Bool onto the distinction quotient cites this. The proof rewrites join via the equivalence inverse and closes by simp on the equivalence definition.
Claim. Let $K$ be any type with 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:Q_h\simeq\mathrm{Bool}$ be the forced coordinate equivalence. For any $\Gamma_1,\Gamma_2\in Q_h$, $$\Phi(\Gamma_1\mathbin{\vee}\Gamma_2)=\Phi(\Gamma_1)\lor\Phi(\Gamma_2),$$ where $\vee$ is configuration join and $\lor$ is Boolean disjunction.
background
The module closes Phase 1 of the T−1→T8 spine: start from a raw distinction witness $h:\exists x,y\in K,,x\neq y$, form the forced observable quotient $Q_h=\mathrm{Quotient}(\mathrm{forcedObservableSetoid},h)$, and prove $Q_h\simeq\mathrm{Bool}$. The point is to thread every later T0–T4 fact through this witness-generated quotient rather than through unthreaded global Bool identities.
A configuration space (from CostFromDistinction) is an abstract monoid of configurations with empty element, binary join, consistency, and independence. On Bool the natural join is disjunction. The forced quotient-to-Bool coordinate equivalence $\Phi$ is the noncomputable equivalence forcedQuotientBoolEquiv, built from the T−1 forcing construction. This lemma is the join-homomorphism half of transporting that ConfigSpace structure across $\Phi$.
proof idea
Tactic proof, two steps. First change rewrites the left-hand side by inserting the equivalence inverse: join on $Q_h$ is defined so that
$$\Gamma_1\mathbin{\vee}\Gamma_2=\Phi^{-1}(\Phi(\Gamma_1)\lor\Phi(\Gamma_2)),$$
hence the claim becomes $\Phi(\Phi^{-1}(b_1\lor b_2))=b_1\lor b_2$. Then simp [forcedQuotientBoolEquiv] discharges the round-trip identity of the equivalence. No external lemmas beyond the definition of $\Phi$ are needed.
why it matters
This is a structural simp fact in the transported ConfigSpace on the distinction quotient. Downstream, forcedQuotientRecognitionCost defines recognition-work cost on $Q_h$ by pulling back the Bool T−1→T0 cost along $\Phi$; join-homomorphism is required for that cost to respect configuration composition. The Phase-2 bridge ledger_floor_t0_bridge likewise consumes the transported floor for every distinction witness and positive weight.
In the forcing chain this sits at the T0 surface: once join and empty are transported, the recognition-work constraint on the quotient is available, and T1–T4 can be routed through the witness rather than global Bool. It is scaffolding for the full T−1→T8 closure path announced in the module doc, not a physics identity by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.