supportQuotient_unique_of_preserves_support
plain-language theorem explainer
Any map from events to support-bearing carriers that recovers a given finite-support observation equals the canonical support-forgetting quotient pointwise. Uniqueness is the certificate used when the forcing chain installs a single support quotient. The proof cases on the image structure and rewrites with the preservation hypothesis.
Claim. Let $E$ be a type of events and $A$ a type of atoms with decidable equality. Fix a support observation $\mathrm{supp}: E \to \mathrm{Finset}\,A$ and a map $q: E \to \mathrm{SupportEvent}(A)$ such that $\mathrm{supportMap}(q(e))=\mathrm{supp}(e)$ for every $e\in E$. Then $q(e)$ equals the canonical support quotient of $e$ for all $e$.
background
In the Unified Forcing Chain, events are often reduced to the atoms they touch. A support event is the concrete carrier whose only data is a finite set of atoms; independence is then ordinary disjointness of those sets, not an extra predicate.
The support map simply reads that finite set. A support-preserving quotient is any map $q$ from raw events into support events such that composing with the support map recovers a prescribed observation $\mathrm{supp}$. The canonical choice sends each event $e$ to the support event whose set is exactly $\mathrm{supp}(e)$.
This sits in the cost-foundation module that forces T0–T8 from the Recognition Composition Law, normalization, and calibration. Support forgetting is the discrete reduction step that makes ledger and recognition structure live on finite atom sets.
proof idea
Tactic proof, short. Introduce an arbitrary event $e$ and case on the structure of $q(e)$, writing it as a support event with underlying set $s$. The preservation field of the hypothesis, rewritten with the support-map definition, forces $s=\mathrm{supp}(e)$. A final simplification against the definition of the canonical support quotient closes the equality $q(e)=\mathrm{canonical}(e)$.
why it matters
Uniqueness turns the support-forgetting construction into a canonical object rather than one choice among many. Downstream, the theorem canonical_support_quotient_map packages the canonical map as a full support-quotient certificate, using this uniqueness together with the fact that the canonical map itself preserves support.
In the forcing chain this matters for T2–T4 style discreteness and ledger steps: once events are identified with finite supports, cost, independence, and recognition work become Finset combinatorics. The result is pure foundation scaffolding inside the complete inevitability chain (absolute floor through T8), not a numerical constant claim, but it locks the discrete carrier the later φ and eight-tick arguments sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.