supportCardinalityCost_of_quotient_cost
plain-language theorem explainer
If a cost on events equals the canonical support-event cost after quotienting each event by its finite support map, then that cost is exactly support cardinality. Anyone wiring cost-from-distinction into the T5–T6 self-similarity bridge cites this. The proof is a two-step rewrite: apply the agreement hypothesis, then reduce to the definition of support cost.
Claim. Let $\mathrm{Event}$ carry a configuration-space structure and let $\kappa$ be a cost function on it. Fix a support map $\mathrm{support}:\mathrm{Event}\to\mathrm{Finset}\,\mathrm{Atom}$. If for every event $e$ one has $\kappa(e)=C_{\mathrm{supp}}(q(e))$, where $q$ is the support-quotient embedding into support-bearing events and $C_{\mathrm{supp}}$ is the canonical support cost, then $\kappa(e)=|\mathrm{support}(e)|$ for all $e$.
background
The ambient module is the Unified Forcing Chain: T−1 through T8 are forced from the Recognition Composition Law plus normalization and calibration. Locally one works in the cost-from-distinction layer. A configuration space supplies empty config, join, consistency, and independence. A cost function $C$ is nonnegative, zero exactly on consistent configs (dichotomy), and additive on independent joins.
Support events are the concrete model: each carrier is a finite set of atoms, join is union, and independence is disjointness of supports. The associated support cost is cardinality of that finite set. Support-cardinality cost is the proposition that an arbitrary cost $\kappa$ on a general event type agrees with cardinality of a chosen support map.
The support quotient sends a general event to the support event whose support is $\mathrm{support}(e)$. The hypothesis here is that $\kappa$ already matches the canonical support cost after that quotient.
proof idea
Tactic proof of the single field cost_eq_card. Introduce an arbitrary event $e$. Rewrite $\kappa.C,e$ by the given pointwise agreement with support cost on the quotiented event. The remaining equality is definitional: support cost of the support-quotient event is exactly the cardinality of $\mathrm{support}(e)$, discharged by rfl. No external lemmas are needed beyond that definitional reduction.
why it matters
This is a small but load-bearing certificate in the forcing chain. Downstream, supportCardinalityCost_of_supportQuotient lifts cost preservation through a quotient map to support-cardinality cost on the extracted support. That package feeds the T5-to-T6 bridge (t5_to_t6_bridge_holds), which turns unique $J$ (T5: $J(x)=(x+x^{-1})/2-1$) into self-similarity forcing $\varphi$ (T6).
In the framework, support cardinality is the discrete counting cost that makes ledger independence literal disjointness. Without identifying general costs with that counting form after quotient, the discrete self-similar hierarchy that pins $\varphi$ does not attach cleanly to the cost foundation. The declaration closes that identification under the natural agreement hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.