liftToQuotient_spec
plain-language theorem explainer
The declaration shows that any map f from configurations to an arbitrary type X, constant on pairs related by the indistinguishability relation from recognition map r, recovers its original values when composed with the quotient projection. Researchers building functions out of the recognition quotient in geometry or information models would cite this to verify commutativity of the diagram. The proof is immediate reflexivity matching the definition of the lift operation.
Claim. Let $C$ be the configuration space with recognition map $r: C → E$. For any $f: C → X$ such that $f(c_1)=f(c_2)$ whenever $c_1$ and $c_2$ are indistinguishable under $r$, the induced map on the quotient satisfies $f([c]_r)=f(c)$ for all $c ∈ C$.
background
The module builds the recognition quotient $C_R = C / ∼$ by collapsing configurations that produce identical outputs under the recognition map $r$. Indistinguishability is the equivalence $c_1 ∼ c_2$ iff $r(c_1)=r(c_2)$, drawn from the imported Indistinguishable relation. liftToQuotient constructs the unique map out of the quotient that commutes with the canonical projection when the input function respects the relation.
proof idea
The proof is a term-mode reflexivity that directly matches the defining equation of liftToQuotient. No additional lemmas are invoked; the equality holds by construction of the quotient projection recognitionQuotientMk.
why it matters
This result supplies the universal property of the recognition quotient, ensuring invariant functions factor through the quotient. It supports sibling constructions such as quotientEventMap and quotientNeighborhoods within the same module. In the broader framework it aligns with the forcing chain by furnishing a geometric identification that preserves J-cost and phi-ladder structures imported from PhiForcingDerived and SpectralEmergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.