SeedClosureEquiv
plain-language theorem explainer
Defines the forcing-relevant equivalence between a multilevel hierarchy and a seed-closed replacement: non-seed levels match, and the seed slot is the canonical sum of the base two levels. Hierarchy and φ-forcing arguments cite it as the exact quotient used on the universal forcing spine. As a structure of propositions there is no proof body; instances are built by supplying the four field witnesses.
Claim. For nontrivial multilevel compositions $M,N$ (positive level maps $\mathbb{N}\to\mathbb{R}$ with at least three positive levels), $M$ and $N$ are seed-closure equivalent when: (i) $N$ is a seed-closed replacement of $M$ (all levels except the canonical seed index agree, and $N$'s seed level equals $N$'s level $0$ plus level $1$); (ii) $N$'s levels $0$ and $1$ equal $M$'s; (iii) $N$'s seed level equals $M$'s level $0$ plus $M$'s level $1$ (canonical additive closure).
background
The module UnifiedForcingChain aims to force the full T-1 through T8 chain from the Recognition Composition Law plus normalization and calibration. Mid-chain, hierarchies of positive real levels encode discrete self-similar scale structure; T6 is the claim that the unique admissible adjacent ratio is $\varphi$.
A NontrivialMultilevelComposition is a map $\mathrm{levels}:\mathbb{N}\to\mathbb{R}$ with every level positive and the first three strictly positive. Seed closure concerns a distinguished index (the canonical seed post): a replacement may rewrite only that slot, setting it to the sum of levels $0$ and $1$ (the seed size law), while freezing every other level.
SeedClosedReplacement packages that freeze-plus-seed-size condition. The present structure tightens it to a forcing quotient: base levels $0$ and $1$ are identified with the original hierarchy, and the seed slot is the additive closure computed from the original base, not merely from the replacement's own base. Downstream lemmas treat this as the exact equivalence used when swapping a hierarchy for its seed-closed form without changing forced ratios.
proof idea
Definitional structure, not a proved theorem. An instance is a four-field Prop record: a SeedClosedReplacement witness, equality of level $0$, equality of level $1$, and equality of the seed level with $M.levels,0+M.levels,1$. No tactics or upstream lemmas discharge anything here; constructors such as seedClosedMultilevelComposition_equiv later fill the fields by simp on the canonical seed-closed construction and by the companion replacement theorem.
why it matters
This is the bridge relation on the universal forcing spine between raw multilevel hierarchies and their seed-closed forms. Parent results include seedClosedMultilevelComposition_equiv (the canonical construction is equivalent to the original), seedClosureEquiv_levels_unique (any equivalent $N$ has the canonical seed-closed level sequence), and seedClosureEquiv_preserves_base_ratio (the ratio $levels,1/levels,0$ is invariant).
Most directly for T6, seedClosureEquiv_forces_phi_iff states that seed-closure equivalence preserves the proposition that the forced hierarchy ratio is $\varphi$: replacing a hierarchy by a seed-closed equivalent does not change whether the hierarchy forces $\varphi$. seedClosureEquiv_hierarchy_forced_ratio_eq likewise identifies ratio fields of forced ladders once uniformity and growth witnesses are supplied. Without this quotient, seed-size normalization would be an ad hoc rewrite rather than a forcing-invariant step in the complete inevitability chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.