canonical_support_cardinality_cost
plain-language theorem explainer
For any atom type with decidable equality, the support-event cost on the canonical support carrier is the unique support-cardinality cost. Anyone citing the T5–T6 self-similarity bridge or support-cost uniqueness on the forcing chain needs this certificate. The proof is a two-field structure pack of the existence and uniqueness lemmas already proved for support events.
Claim. For every type $A$ of atoms with decidable equality, the support-event cost on the canonical support carrier $\mathrm{SupportEvent}(A)$ is a support-cardinality cost (via the support map and support cost), and it is the unique such cost among cost functions on that carrier.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Support events are the canonical carrier for distinction-based costs: each event carries a finite support of atoms, and the support map records that support.
Support-cardinality cost means the recognition cost of an event equals (up to the fixed calibration) the cardinality of its support. The structure SupportCardinalityCostCanonicality packages two facts on that carrier: the built-in support-event cost is a support-cardinality cost, and any cost function that is support-cardinality cost agrees with it.
Upstream, several cost notions appear (J-cost on recognition events, multiplicative-recognizer derived cost, rung-coarsen multiset cost). Here the relevant one is the support-event cost already shown to be support-cardinality and unique among such costs.
proof idea
Term-mode structure construction. The canonical_cost field is filled by supportEvent_support_cardinality_cost Atom, which already proves that the support-event cost (with its support map) is a support-cardinality cost. The unique field is filled by supportEvent_support_cardinality_cost_unique Atom, which proves uniqueness among cost functions on the support-event carrier. No further rewriting or case analysis occurs.
why it matters
This certificate is the packaged form of support-cardinality uniqueness used on the path into the T5–T6 bridge. Downstream, t5_to_t6_bridge_holds records that the T5-to-T6 self-similarity bridge is theorem-backed once T5 uniqueness is available; support-cost canonicality is part of the discrete ledger/cost infrastructure that makes self-similarity and the forced fixed point $\varphi$ (T6) speak the same cost language as T5's unique $J$.
In the forcing chain, T5 pins $J(x)=(x+x^{-1})/2-1$ and T6 forces $\varphi$ as the self-similar scale. A unique, support-cardinality cost on the canonical carrier keeps the discrete ledger side aligned with that uniqueness, so hierarchy and closed-scale arguments do not introduce a competing cost. The declaration itself is a thin certificate, not a new analytic step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.