SeedEventsEquivalentToCanonical
plain-language theorem explainer
A hierarchy's two seed events are canonically equivalent when their finite supports are exactly the singleton level tags {0} and {1}. Anyone building the T5→T6 self-similarity bridge or a seed-support model cites this predicate. It is a pure Prop structure: two equalities, no proof body.
Claim. Fix a configuration space of events with a support map $\mathrm{support}:\mathrm{Event}\to\mathrm{Finset}\,\mathbb{N}$ and two distinguished seeds $s_0,s_1$. The seeds are canonically equivalent when $\mathrm{support}(s_0)=\{0\}$ and $\mathrm{support}(s_1)=\{1\}$, matching the level-tagged support events at levels $0$ and $1$.
background
The Unified Forcing Chain module aims to force T0–T8 from the cost foundation (Recognition Composition Law, normalization, calibration). Mid-chain, discrete ledger structure and hierarchy dynamics need a concrete model of independent seed events before self-similarity can pin $\varphi$ (T6).
A configuration space supplies empty config, join, consistency, and independence. The canonical carrier is the support-event model: an event is a finite set of atoms, join is union, and independence is literally disjointness of supports. Level-tagged support events package a single natural-number level as a singleton support.
This declaration packages the matching condition that two named seeds realize exactly those canonical singletons ${0}$ and ${1}$. Downstream lemmas then read off disjointness and the seed-support model without extra predicates.
proof idea
No proof: the declaration is a structure-as-Prop. It records two field equalities, seed0_support and seed1_support, each identifying the given support of a seed with the support map of the corresponding level-tagged support event. Inhabitants are pairs of equalities; consumers pattern-match on those fields.
why it matters
Canonical seed equivalence is the clean interface between abstract hierarchy seeds and the support-event model used for independence. Immediate consumers are seed_support_disjoint_of_canonical_equiv (disjointness of ${0}$ and ${1}$) and seed_support_model_of_canonical_equiv (ConfigSpace independence via a compatibility map from disjoint supports).
Those facts feed the T5→T6 self-similarity bridge certificate: a closed observable framework plus a realized hierarchy forces the scale ratio to be $\varphi$. The bridge explicitly needs hierarchy data beyond bare T5 J-uniqueness; canonical seeds supply the discrete two-level seed layer that self-similarity acts on. In the forcing chain this sits between T5 (unique $J(x)=\cosh(\log x)-1$) and T6 ($\varphi$ as the self-similar fixed point).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.