canonical_seed_posting_forces_closure
plain-language theorem explainer
A canonical seed-posting certificate on a nontrivial multilevel hierarchy forces the primitive closure identity: the size of level 2 equals the sum of levels 0 and 1. Hierarchy and T5→T6 bridge arguments cite it to discharge the local additive posting law without the full all-pairs operator. The proof is a two-rewrite: flip the certificate's size equation, then identify the post index with 2 via uniqueness.
Claim. Let $M$ be a nontrivial multilevel composition (positive level sizes $M.\mathrm{levels}:\mathbb{N}\to\mathbb{R}$ with at least three levels). If a canonical seed-posting operation exists for some index $\mathrm{post}_{01}\in\mathbb{N}$ (certifying that $\mathrm{post}_{01}$ is the canonical second-order seed index, that it equals $2$, and that the posted level has additive size), then $M.\mathrm{levels}(0)+M.\mathrm{levels}(1)=M.\mathrm{levels}(2)$.
background
The module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). Inside that chain, the T5→T6 bridge needs only a local hierarchy fact: posting the seed pair of levels closes at level 2 with additive size.
A NontrivialMultilevelComposition is a map of level sizes that is strictly positive at every index and, in particular, at 0, 1, and 2. The structure CanonicalSeedPostingOperation isolates exactly the local datum the bridge uses: a seed-post index certificate, the equality of that index with 2, and the additive size law $M.\mathrm{levels}(\mathrm{post}_{01})=M.\mathrm{levels}(0)+M.\mathrm{levels}(1)$. The full all-pairs posting operator is deliberately stronger than this certificate.
Upstream, canonical_seed_post_index_unique states that any seed-posting index certificate forces the index to equal 2. That uniqueness is the only external lemma the present argument needs beyond the certificate fields themselves.
proof idea
Two rewrites, no case splits. Start from the goal $M.\mathrm{levels}(0)+M.\mathrm{levels}(1)=M.\mathrm{levels}(2)$. Rewrite with the reverse of the certificate field seed_level_posting, replacing the left-hand sum by $M.\mathrm{levels}(\mathrm{post}{01})$. The goal is then $M.\mathrm{levels}(\mathrm{post}{01})=M.\mathrm{levels}(2)$. Apply canonical_seed_post_index_unique to the certificate's seed_index field to obtain $\mathrm{post}_{01}=2$, and the equality collapses.
why it matters
This lemma is the thin interface between a seed-posting certificate and the primitive posting closure identity used by the hierarchy recurrence. Downstream, canonical_posting_closure_of_seed_operation builds the full canonical posting closure from exactly this seed operation (under uniform adjacent ratios and ratio greater than one). In the forcing chain, that closure is the local additive step the T5→T6 bridge needs: unique $J$ plus self-similar discrete ledger forces $\varphi$ as the fixed point, and the hierarchy sizes must close additively at the second-order seed. The certificate design keeps the bridge from depending on a global all-pairs posting operator, so later scaffolding can strengthen the operator without reopening this identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.