CanonicalPostingOperation
plain-language theorem explainer
A Prop-valued certificate that a binary map on hierarchy indices is a local posting operation: it sends the seed pair (0,1) to level 2, and the size of a posted level equals the sum of the two input sizes. Hierarchy and self-similarity arguments cite it in place of the bare equality levels(0)+levels(1)=levels(2). As a structure of hypotheses there is no proof body; downstream lemmas unpack the two fields.
Claim. Fix a nontrivial multilevel composition $M$ (with level-size function $\mathrm{levels}:\mathbb{N}\to\mathbb{R}$) and a binary index map $\mathrm{post}:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$. The pair $(M,\mathrm{post})$ is a canonical posting operation when $\mathrm{post}(0,1)=2$ and, for all $i,j$, $\mathrm{levels}(\mathrm{post}(i,j))=\mathrm{levels}(i)+\mathrm{levels}(j)$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The T5→T6 step forces φ as the self-similar scale ratio of a discrete ledger hierarchy; that step needs an additive “posting” law on level sizes, not only a closed observable cost.
NontrivialMultilevelComposition packages a hierarchy with a level-size map and nontriviality hypotheses (multiple levels, positive sizes). A posting operation is the explicit dynamical stand-in for the seed closure equation $\mathrm{levels}(0)+\mathrm{levels}(1)=\mathrm{levels}(2)$: the map $\mathrm{post}$ names which index receives the sum of two levels, and the two fields pin the seed case and global additivity.
Keeping $\mathrm{post}$ as a parameter (not a structure field) makes the certificate a pure Prop, so later bridges can quantify over operations without smuggling a preferred map into the type.
proof idea
Definitional structure: no proof obligations beyond the two fields. Instantiating it means exhibiting post_zero_one and level_posting. Downstream, canonical_posting_operation_forces_closure is the one-line unpacking: apply level_posting at $(0,1)$ and rewrite with post_zero_one to obtain $\mathrm{levels},0+\mathrm{levels},1=\mathrm{levels},2$. Related projections build the seed-posting certificate and the full posting-closure package from the same data.
why it matters
This is the operation-level interface that feeds the T5→T6 self-similarity bridge. Downstream, canonical_posting_operation_forces_closure recovers the primitive level-0/1 closure equation; canonical_seed_posting_of_operation projects to the seed certificate; canonical_posting_closure_of_operation builds the full closure under constant scale ratio and ratio $>1$. The bridge structure T5_To_T6_SelfSimilarity_Bridge records that bare closed-observable data do not force hierarchy fields such as additive posting, so this certificate is the explicit missing piece rather than a hidden assumption.
In the forcing chain, T5 pins the unique J-cost $J(x)=(x+x^{-1})/2-1$; T6 forces φ as the self-similar fixed point of the discrete ledger. Additive posting is the hierarchy dynamics that makes the scale ratio well-defined and forces it to φ. Without an operation-shaped witness, the chain would rest on a raw numeric equality with no dynamical content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.