CanonicalSeedPostingOperation
plain-language theorem explainer
Certificate that a multilevel hierarchy posts the seed pair (levels 0 and 1) at the canonical index 2 with additive size. Isolates the exact local datum the T5→T6 self-similarity bridge needs, weaker than full all-pairs posting. Downstream closure and φ-forcing constructors cite it. Pure structure of three Prop fields; no proof body.
Claim. For a nontrivial multilevel composition $M$ (positive level sizes $M_k$ with at least three levels) and an index $n\in\mathbb{N}$, the seed-posting certificate asserts: $n$ equals the canonical seed-post index (hence $n=2$), and the level sizes satisfy $M_n = M_0 + M_1$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T5 pins the unique cost $J(x)=(x+x^{-1})/2-1$; T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger hierarchy.
A nontrivial multilevel composition $M$ is a map $\mathbb{N}\to\mathbb{R}$ of positive level sizes with at least three levels occupied. The hierarchy recurrence that feeds self-similarity only needs the primitive seed pair: level 0 posted with level 1 closes at level 2, and the posted size is the sum of the two seed sizes.
CanonicalSeedPostIndex is the companion certificate that a proposed index equals the theorem-backed canonical seed-post index (namely 2). The full all-pairs posting operation is stronger than the bridge requires; this structure isolates that exact local datum.
proof idea
Definitional structure, not a proved theorem. It packages three fields: (i) a CanonicalSeedPostIndex witness that the proposed index is the canonical seed-post index; (ii) the explicit equality of that index with 2; (iii) the additive size law $M_{\mathrm{post}}=M_0+M_1$ at the posted level. Inhabitants are built by the sibling constructors that project a full posting operation, a seed-size law, or a direct level-two size hypothesis onto these three fields.
why it matters
This is the minimal certificate the T5→T6 self-similarity bridge consumes. Downstream, canonical_seed_posting_forces_closure rewrites the additive law at index 2; canonical_posting_closure_of_seed_operation and canonical_posting_closure_of_uniform_growth_seed lift it to full posting closure under uniform scale and growth orientation; canonical_uniform_growth_seed_forces_phi and T5_To_T6_SelfSimilarity_Bridge carry the chain from unique $J$ to forced $\varphi$.
By stripping the all-pairs posting operation down to the seed pair, the bridge avoids over-hypothesizing while still feeding the discrete self-similarity that pins $\varphi$ (primer landmark T6). It sits inside the complete inevitability chain from the cost foundation through T5 uniqueness to the eight-tick and $D=3$ steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.