seed_support_disjoint_of_canonical_equiv
plain-language theorem explainer
If two seed events are canonically equivalent (level-0 support is {0}, level-1 support is {1}), their finite supports are disjoint. Anyone building the seed-support model or the T5→T6 self-similarity bridge cites this. The proof rewrites both supports to the canonical level-tagged maps and applies the known disjointness of those maps.
Claim. Let $E$ be a configuration space with a support map $\mathrm{supp}: E \to \mathrm{Finset}\,\mathbb{N}$. If seed events $s_0,s_1\in E$ are canonically equivalent (so $\mathrm{supp}(s_0)=\{0\}$ and $\mathrm{supp}(s_1)=\{1\}$ via the level-tagged support events), then $\mathrm{supp}(s_0)$ and $\mathrm{supp}(s_1)$ are disjoint.
background
The module Unified Forcing Chain derives the full T-1 through T8 ladder from the cost foundation (Recognition Composition Law, normalization, calibration). Mid-chain, seed events must sit on a discrete hierarchy whose supports behave like independent configuration atoms.
A configuration space supplies empty config, join, consistency, and an independence relation (no shared predicates). Support here is a map from events to finite sets of natural numbers (level tags). Canonical seed-event equivalence means the two seeds are exactly the level-tagged support events: seed 0 carries support ${0}$ and seed 1 carries ${1}$.
Upstream, levelSupportEvent_seed_disjoint already records that those two canonical level supports are disjoint. The present result lifts that fact from the canonical representatives to any pair of seeds that match them.
proof idea
One-line algebraic transfer. Rewrite support seed0 and support seed1 by the two fields of the canonical-equivalence hypothesis, replacing them with the supports of levelSupportEvent 0 and levelSupportEvent 1. Then apply levelSupportEvent_seed_disjoint, which states those two Finsets are disjoint. No case split or induction.
why it matters
Disjoint seed supports are the bridge from canonical equivalence to a genuine seed-support model: the immediate parent seed_support_model_of_canonical_equiv packages this disjointness with a compatibility map into ConfigSpace.Independent. That model feeds the T5→T6 self-similarity bridge (t5_to_t6_bridge_holds), where unique $J$ (T5: $J(x)=(x+x^{-1})/2-1$) forces $\varphi$ as the discrete self-similar fixed point (T6).
Without support disjointness, the two seeds would share level tags and could not act as independent generators of the hierarchy. In the forcing chain this is a small but load-bearing step between ledger/recognition structure and the $\varphi$-forcing half of the ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.