supportEvent_support_cardinality_cost
plain-language theorem explainer
On the canonical support-bearing event carrier, event cost equals the cardinality of the event's finite support. Cost-from-distinction and ledger-forcing arguments cite this to certify that the default support-event cost is a support-cardinality cost. The proof is pure definitional reflexivity after introducing an arbitrary event.
Claim. Fix a type of atoms with decidable equality. Equip support events (each event is a finite set of atoms) with the canonical cost and the support projection. Then for every event $e$, the cost satisfies $C(e)=|\mathrm{supp}(e)|$: the cost is support-cardinality cost.
background
The Unified Forcing Chain module derives T-1 through T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Early in that chain, cost is read off distinction structure rather than postulated as an independent primitive.
A support event is the concrete carrier whose data is a finite set of atoms. Join is union and the empty configuration is the empty set, so independence is literally disjointness of supports rather than an extra predicate. A cost function on a configuration space is called support-cardinality cost when the cost of every event equals the cardinality of its finite support.
The structure SupportCardinalityCost packages exactly that equality as a Prop field. The present theorem instantiates it on the support-event model with the model's own support map and canonical cost.
proof idea
Term-mode structure instance with a one-step tactic field. After intro e, the goal is definitional equality between the canonical support-event cost of $e$ and the cardinality of $e$'s support; rfl closes it. No external lemmas are required: the cost and support map are defined so that the identity holds by construction.
why it matters
This is the positive half of the canonical support-cardinality cost certificate. Downstream, canonical_support_cardinality_cost packages it with the matching uniqueness theorem so that any support-cardinality cost on support events agrees pointwise with the canonical cost.
In the forcing chain, that certificate anchors cost-from-distinction bookkeeping: when events are finite supports, recognition cost is counting atoms in the support. That discrete counting model feeds later ledger and recognition steps (T3–T4) where cost symmetry and observables are forced, and it keeps the absolute-floor / T0 cost foundation aligned with a concrete Finset carrier rather than an abstract ConfigSpace alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.