canonical_level_seed_independent
plain-language theorem explainer
In the canonical level-tagged support carrier, the seed events for levels 0 and 1 are independent as configurations: their supports are disjoint singletons, so no extra independence hypothesis is needed. Anyone building the T5-to-T6 self-similarity bridge or a seed-only recognition-work model cites this. The proof is a one-line application of the general seed-support independence lemma to the canonical support model.
Claim. In the configuration space of support events on $\mathbb{N}$, the canonical level-$0$ and level-$1$ seed events (singleton supports $\{0\}$ and $\{1\}$) are independent: they share no atoms under the support map.
background
The Unified Forcing Chain module aims to force every step T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). The T5-to-T6 leg needs a discrete multilevel hierarchy whose seed levels post recognition work additively; that additivity rests on configuration independence of the seeds.
A configuration space supplies an empty config, a join, consistency, and an independence relation (no shared predicates). Here events are support events on $\mathbb{N}$: the canonical level-tagged event at index $k$ is the singleton support ${k}$, so distinct levels are disjoint by construction.
Upstream, seed_independent_of_support_model states that any seed pair packaged as a SeedEventSupportModel (support-disjoint seeds) yields ConfigSpace.Independent. The companion theorem canonical_level_seed_support_model installs levels 0 and 1 in that model via the support-event seed constructor.
proof idea
One-line term proof: apply seed_independent_of_support_model to canonical_level_seed_support_model. The latter already certifies that levelSupportEvent 0 and levelSupportEvent 1 form a seed support model (disjoint singleton supports under SupportEvent.supportMap). The general lemma then discharges ConfigSpace.Independent with no further hypotheses.
why it matters
This lemma closes the independence obligation for the canonical seed carrier used throughout the T5-to-T6 bridge. Downstream, canonical_seed_recognition_work_model_of_support_events builds the seed-only recognition-work model "route used by the forcing bridge: only seed disjointness is required." That model feeds T5_To_T6_SelfSimilarity_Bridge and the theorem t5_to_t6_bridge_holds, which certify that unique $J$ plus a realized closed hierarchy forces the self-similar scale $\varphi$ (forcing-chain landmark T6).
Without seed independence, recognition-work additivity across levels would need an extra hypothesis; the canonical singleton tagging removes that gap. The result is local plumbing inside Foundation.UnifiedForcingChain, but it is load-bearing for the complete inevitability claim that T6 is forced rather than merely compatible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.