canonical_posting_operation_forces_closure
plain-language theorem explainer
Any multilevel hierarchy equipped with a canonical posting operation must satisfy the seed closure equation: the size of level 2 equals the sum of levels 0 and 1. Hierarchy and ledger-forcing arguments cite this to convert a local posting certificate into the primitive additive relation among the first three levels. The proof is a three-line rewrite: instantiate additivity at (0,1), substitute the seed landing post(0,1)=2, and symmetrize.
Claim. Let $M$ be a nontrivial multilevel composition (a positive real-valued level-size map with at least three levels). Let $\mathrm{post}:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ be a binary index map, and suppose a canonical posting operation exists: $\mathrm{post}(0,1)=2$ and $M.levels(\mathrm{post}(i,j))=M.levels(i)+M.levels(j)$ for all $i,j$. Then $M.levels(0)+M.levels(1)=M.levels(2)$.
background
The ambient module is the Unified Forcing Chain: it aims to derive the full T0–T8 ladder as inevitabilities from the Recognition Composition Law plus normalization and calibration. Local hierarchy data appear as a NontrivialMultilevelComposition: a map $k\mapsto M.levels(k)\in\mathbb{R}$ that is strictly positive on every index and, in particular, positive on the seed triple $0,1,2$.
A CanonicalPostingOperation is a Prop-valued certificate on such an $M$ relative to an external binary map $\mathrm{post}$. Its two fields say that posting the adjacent seeds lands at the next level ($\mathrm{post}(0,1)=2$) and that posting is additive on level sizes ($M.levels(\mathrm{post}(i,j))=M.levels(i)+M.levels(j)$). The structure is deliberately not a data carrier: $\mathrm{post}$ is a parameter so the certificate remains propositional.
This sits next to ledger-posting adjacency (unit debit/credit posts on accounts) and multilevel ratio-forcing (no free scale parameters force uniform adjacent ratios). The present lemma isolates the purely algebraic seed-closure consequence of the posting certificate, before ratio or self-similarity hypotheses enter.
proof idea
Three tactic steps, no external lemmas. Instantiate the certificate's additivity field at the seed pair $(0,1)$ to obtain $M.levels(\mathrm{post},0,1)=M.levels,0+M.levels,1$. Rewrite the left-hand index with the certificate's seed-landing field $\mathrm{post},0,1=2$. Symmetrize the resulting equality to match the goal $M.levels,0+M.levels,1=M.levels,2$.
why it matters
In the forcing chain this is the bridge from a local posting certificate to the primitive three-level additive relation that hierarchy arguments treat as the first closure step. Downstream, canonical_posting_closure_of_operation builds the full canonical posting closure from an explicit operation rather than from a raw equality; it consumes this theorem (together with no-free-scale and ratio-greater-than-one hypotheses) to package the seed sum into the closure object used later in the chain.
The module's stronger claim is that every rung T-1 through T8 is forced from cost. Seed-level additivity is the discrete bookkeeping step that lets multilevel composition talk about local second-order hierarchy without free parameters: levels 0 and 1 close at 2 by posting, after which uniform ratios and self-similarity (toward T6 $\varphi$ and the eight-tick octave) can be imposed. The declaration itself is fully proved; it does not touch open scaffolding, but it is the algebraic hinge those later packaging theorems turn on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.