SupportCardinalityCostCanonicality
plain-language theorem explainer
Packages two properties: the canonical support-event cost equals support cardinality, and any cost with that form agrees pointwise with it. Cited when fixing the discrete cost model before self-similarity and φ forcing. As a Prop structure it is pure interface; the inhabited certificate is built elsewhere.
Claim. For a type of atoms with decidable equality, a support-cardinality cost canonicality certificate asserts: (i) the canonical cost on support-events equals the cardinality of the event's finite support; (ii) any cost function $\kappa$ on support-events that likewise equals support cardinality agrees with the canonical cost on every event.
background
In the Unified Forcing Chain, T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. Early steps need a discrete event model whose cost is not an arbitrary functional but is pinned to combinatorial data.
A SupportEvent is a finite set of atoms; join is union and the empty configuration is the empty set. Independence is disjointness of supports, not an extra predicate. A cost is support-cardinality cost when $C(e)$ equals the cardinality of that support.
The present structure records that the built-in support cost on this carrier is of that form and is unique among all such costs. That uniqueness is the discrete anchor later bridges use when moving from unique $J$ (T5) toward self-similar scale ratio $\varphi$ (T6).
proof idea
No proof body: this is a Prop-valued structure (definitional interface). Fields are the two propositions canonical_cost and unique. A companion Subsingleton instance shows any two certificates are propositionally equal by rfl. Inhabitation is deferred to canonical_support_cardinality_cost, which fills the fields from supportEvent_support_cardinality_cost and its uniqueness lemma.
why it matters
Gives a named certificate type for “support cost is cardinality and is unique,” so later chain steps can demand that discrete cost model without re-proving it. Downstream, canonical_support_cardinality_cost inhabits the structure for every atom type. The T5→T6 self-similarity bridge sits in the same module and routes unique $J$ plus hierarchy data toward $\varphi$; a fixed support-cardinality cost is part of the discrete ledger setting that makes self-similarity well-posed. In the primer chain this sits under the cost foundation feeding T5 (unique $J$) and T6 ($\varphi$ as self-similar fixed point), not as a standalone physics law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.