supportEvent_support_cardinality_cost_unique
plain-language theorem explainer
Any cost on support-bearing events that equals the cardinality of finite support agrees pointwise with the canonical support-cardinality cost. Foundation workers cite this when packaging uniqueness of the support-event cost model. The proof rewrites by the support-cardinality hypothesis and closes by definitional equality.
Claim. Let $\mathrm{Atom}$ be a type with decidable equality, and let $\kappa$ be a cost function on support events over $\mathrm{Atom}$. If $\kappa$ is a support-cardinality cost relative to the support map (i.e. $\kappa(e)=|\mathrm{support}(e)|$ for every event $e$), then for every support event $e$, $\kappa(e)$ equals the canonical support cost of $e$.
background
In the Unified Forcing Chain, T0–T8 are forced from the cost foundation (Recognition Composition Law plus normalization and calibration). Early in that chain one needs a concrete event carrier on which independence is not an extra predicate but disjointness of finite supports.
A SupportEvent is exactly that carrier: an event is a finite set of atoms, join is union, and the empty support is the empty configuration. A cost function on a configuration space satisfies dichotomy (zero cost iff consistency) and independent additivity over joins of configurations that share no predicates.
SupportCardinalityCost is the property that event cost equals the cardinality of its finite support. The canonical cost on support events is defined that way; this theorem says every cost satisfying the same property agrees with it pointwise.
proof idea
Term/tactic hybrid, three steps. Introduce an arbitrary support event $e$. Rewrite the goal using the support-cardinality hypothesis cost_eq_card, which replaces $\kappa.C,e$ by the cardinality of the support of $e$. The remaining equality is definitional with the canonical support cost, so rfl finishes.
why it matters
This uniqueness lemma is one half of the canonical support-cardinality cost certificate. Downstream, canonical_support_cardinality_cost packages the existence of the canonical support cost together with this uniqueness into a single SupportCardinalityCostCanonicality record.
In the forcing chain that matters because the absolute-floor and T0 logic-from-cost story need a rigid, unique cost model on the support-event carrier: independence is support-disjointness, and cost is support size. Without pointwise uniqueness, later steps that treat the support cost as the forced recognition-work measure would only hold up to an unspecified alternative. The result sits in Foundation, feeding the complete inevitability chain rather than a late physics constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.