SupportCardinalityCost
plain-language theorem explainer
A cost on events is support-cardinality cost when each event's cost equals the size of its finite atomic support. Workers on the T0–T8 forcing chain cite this predicate when reducing recognition cost to counting independent atoms. It is a Prop-structure definition with a single field (no proof body); later uniqueness and quotient-extraction lemmas inhabit or discharge it.
Claim. Fix a configuration space of events, a cost function $\kappa$ on those events, and a support map $s$ sending each event to a finite set of atoms. Then $\kappa$ is support-cardinality cost relative to $s$ when $\kappa(e)=|s(e)|$ for every event $e$.
background
The ambient module is the Unified Forcing Chain: T-1 through T8 are derived as inevitabilities from the cost foundation (Recognition Composition Law, normalization, calibration), rather than assumed as compatible axioms.
A configuration space supplies an empty configuration, a binary join, consistency, and an independence relation. A cost function assigns a real cost to each configuration. The canonical concrete carrier is the support-bearing event: each event is a finite set of atoms, join is union, and independence is disjointness of supports. On that carrier the natural cost is the cardinality of the support set.
Upstream, configuration spaces and cost functions come from CostFromDistinction; the support-event model packages independence as a structural fact rather than an extra predicate. Cosmology-side event and rung-cost notions supply related counting language but are not required to state this predicate.
proof idea
Definitional structure, not a proved theorem. It packages one propositional field: for every event, the cost equals the cardinality of the assigned finite support. No tactics, no lemmas applied. Downstream theorems construct instances by rfl on the canonical support-event cost, or by transporting equality through a support quotient that preserves cost.
why it matters
This predicate is the interface between abstract recognition cost and discrete atom-counting. It is inhabited immediately for the canonical support-event cost, and uniqueness says any support-cardinality cost on that carrier agrees pointwise with the canonical one. Quotient theorems lift the property: if a source cost agrees with support-event cost after support quotient, or if cost is preserved through a quotient map into support-events, then the extracted support map yields support-cardinality cost. Full support-extraction compatibility structures use it to replace a primitive support map by theorem-backed extraction.
In the forcing chain this sits under the cost foundation that drives T0 (logic from cost minimization) and the discreteness/ledger steps (T2–T4): cost that is literally support cardinality makes independence and join-cost additive in the finite-set sense, aligning with the discrete ledger before J-uniqueness (T5) and φ-forcing (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.