canonical_posting_closure_of_closure
plain-language theorem explainer
Given a nontrivial multilevel composition with uniform adjacent ratios greater than one, the raw equality levels₀ + levels₁ = levels₂ is enough to build the full canonical posting-closure certificate. Hierarchy and self-similarity arguments cite this to obtain additive recurrence without assuming an external composition axiom. The proof packages the given equality and derives additivity via the hierarchy ladder and posting-extensivity.
Claim. Let $M$ be a multilevel composition with positive levels $L:\mathbb{N}\to\mathbb{R}$ and at least three levels. Suppose adjacent ratios are scale-free: $L(j+1)/L(j)=L(k+1)/L(k)$ for all $j,k$, and $L(1)/L(0)>1$. If the primitive closure $L(0)+L(1)=L(2)$ holds, then $M$ carries a canonical posting-closure certificate: that equality as posting closure, plus the derived additive recurrence used by the hierarchy theorem.
background
The Unified Forcing Chain module aims to force T0–T8 from the cost foundation (Recognition Composition Law with normalization and calibration). The T5→T6 step needs self-similarity on a discrete ledger hierarchy; that hierarchy is a positive level sequence, not yet a composition law.
A NontrivialMultilevelComposition supplies only positive levels with at least three rungs. Uniform adjacent ratios (no free scale) plus ratio $>1$ produce a UniformScaleLadder via hierarchy_forced. What is still missing is a posting/composition operation relating levels.
CanonicalPostingClosure is the first theorem-facing certificate for that missing operation: primitive order $L(0)+L(1)=L(2)$, together with the additive recurrence the hierarchy theorems consume. Upstream, closure_forces_additive states that geometric-scale closure under additive composition forces the same equality in additive form, replacing an external HasAdditiveComposition axiom by the physical demand that composing level-0 and level-1 events yields a level-2 event.
proof idea
Term-mode structure construction. The posting_closure field is the hypothesis $L(0)+L(1)=L(2)$ unchanged.
For additive_closure, apply PostingExtensivity.closure_forces_additive to $L$, positivity of levels, and the ratio, ratio-greater-than-one, and uniform-scaling fields of hierarchy_forced M no_free_scale ratio_gt_one, plus the same closure equality. That lemma returns the additive form used downstream.
The remaining field additive_eq_posting_extensivity is definitional (rfl).
why it matters
In the complete inevitability chain, T6 (φ forced by self-similarity in the discrete ledger) needs a closed scale hierarchy with genuine additive posting, not an assumed composition axiom. This theorem is the base constructor: raw primitive closure becomes a full CanonicalPostingClosure.
It feeds canonical_posting_closure_of_operation and canonical_posting_closure_of_seed_operation, which rebuild the same certificate from an explicit local or seed posting map rather than a bare equality. Those certificates support t5_to_t6_bridge_holds, which asserts the T5-to-T6 self-similarity bridge is theorem-backed (unique $J$ plus internal hierarchy forcing φ).
Framework landmarks: T5 $J$-uniqueness and T6 φ as the self-similar fixed point. The construction is the RS-internal stand-in for additive composition on the scale ladder that later pins φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.