canonical_posting_closure_of_operation
plain-language theorem explainer
From a local posting operation on a multilevel hierarchy (seed levels 0 and 1 post to level 2, sizes add), one obtains the full canonical posting-closure certificate. Hierarchy and T5–T6 bridge arguments cite this to upgrade a local additive seed into the global additive recurrence under uniform scale ratios. The proof composes two lemmas: the operation forces the primitive equality, then that equality is packaged as CanonicalPostingClosure.
Claim. Let $M$ be a nontrivial multilevel composition (positive level sizes, at least three levels). Assume adjacent ratios are constant (no free scale) and $M.\mathrm{levels}(1)/M.\mathrm{levels}(0)>1$. If a posting map $\mathrm{post}:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ satisfies $\mathrm{post}(0,1)=2$ and $M.\mathrm{levels}(\mathrm{post}(i,j))=M.\mathrm{levels}(i)+M.\mathrm{levels}(j)$ for all $i,j$, then $M$ admits canonical posting closure: $M.\mathrm{levels}(0)+M.\mathrm{levels}(1)=M.\mathrm{levels}(2)$ and the derived additive recurrence on levels.
background
The module UnifiedForcingChain aims to force the full T0–T8 chain from the cost foundation (Recognition Composition Law, normalization, calibration). T6 is the self-similarity step that pins $\varphi$ in a discrete ledger hierarchy.
A NontrivialMultilevelComposition supplies only a positive real sequence of level sizes with at least three levels; it does not encode how levels compose. A CanonicalPostingOperation is a Prop-valued certificate for a supplied map post: posting the seed pair $(0,1)$ lands at level $2$, and posted level size equals the sum of the two constituent sizes.
CanonicalPostingClosure is the theorem-facing object that fills the missing operation: primitive order $M.\mathrm{levels},0+M.\mathrm{levels},1=M.\mathrm{levels},2$, plus the additive recurrence the hierarchy theorems consume. The hypotheses no_free_scale (uniform adjacent ratios) and ratio_gt_one are the scale-rigidity side conditions used throughout HierarchyForcing.
proof idea
Term-mode one-liner. First apply canonical_posting_operation_forces_closure to $M$ and the operation certificate: the local axioms post 0 1 = 2 and additivity of sizes immediately give the primitive equality $M.\mathrm{levels},0+M.\mathrm{levels},1=M.\mathrm{levels},2$. Then feed that equality into canonical_posting_closure_of_closure, which packages the primitive posting equality (under the standing no-free-scale and ratio-gt-one hypotheses) into a full CanonicalPostingClosure record, including the derived additive recurrence field.
why it matters
This is the preferred entry point into posting closure: start from an explicit local operation rather than a raw equality. Downstream it is consumed by t5_to_t6_bridge_holds, whose doc-comment states that the T5-to-T6 self-similarity bridge is theorem-backed. That bridge is the forcing step from unique $J$ (T5: $J(x)=(x+x^{-1})/2-1$) to $\varphi$ as the self-similar fixed point (T6) inside a discrete multilevel ledger.
In the module's complete inevitability chain, T6 is forced by self-similarity in the discrete ledger; canonical posting closure supplies the additive composition law that makes self-similar scale recurrence well-defined. Without upgrading a seed posting operation to global closure, the hierarchy cannot force a unique growth ratio, and the $\varphi$-pinning argument does not fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.