supportCost
plain-language theorem explainer
Canonical recognition-work cost on support events equals the cardinality of the finite support, cast to a real. Anyone building the seed recognition-work model or proving support-cardinality cost canonicality cites this. The definition packages three short Finset arguments: nonnegativity of card, zero card iff empty support, and card of a disjoint union.
Claim. On the carrier of support events (each event is a finite set of atoms), the map $C(a) = |\mathrm{supp}(a)| \in \mathbb{R}$ is a cost function: $C \ge 0$; $C(a) = 0$ if and only if $\mathrm{supp}(a) = \emptyset$; and if two events have disjoint supports then $C(a \vee b) = C(a) + C(b)$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Early in that chain one needs a concrete configuration space on which recognition work is measured.
A configuration space supplies an empty configuration, a join, consistency, and an independence relation. A cost function on such a space is a real-valued map that is nonnegative, zero exactly on consistent configurations (dichotomy), and additive under independent join.
SupportEvent is the concrete carrier: an event is just a finite set of atoms; join is union; independence is disjointness of supports. That makes independence structural rather than an extra predicate, which is why this carrier is the canonical model for seed recognition-work posting.
proof idea
The cost map is defined by $C(a) = |\mathrm{supp}(a)|$ as a real. Nonnegativity is Nat.zero_le on the card, cast to $\mathbb{R}$. Dichotomy: if the real card is zero then the natural card is zero, hence the Finset is empty (Finset.card_eq_zero); conversely the empty support has card zero. Additivity: under the independence hypothesis (disjoint supports), Finset.card_union_of_disjoint gives $|A \cup B| = |A| + |B|$, cast to reals.
why it matters
This is the scalar cost that the forcing bridge actually uses. Downstream, it feeds the canonical seed-only recognition-work model (only seed disjointness required), the aggregate scalar-work projection by finite-support cardinality, and the theorems that the SupportEvent cost is support-cardinality cost and is unique/canonical after quotient. Those surfaces sit under SupportCardinalityCostCanonicality and SupportEventAggregateProjection.
In the T−1/T0 layer of the chain, recognition work must be a genuine cost function before logic and discreteness can be forced from cost minimization. Packaging cardinality as that cost closes the concrete model side of the cost foundation without introducing an ad hoc functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.