scaleClosureAtWith_iff_ledgerCompose
plain-language theorem explainer
Under work-extensive scale composition (op equals addition on work values), closure of a geometric scale sequence at index n via op is equivalent to closure via ledger composition. Cite when swapping an abstract compose operator for the ledger's additive compose in φ-scale arguments. Proof is a two-sided unfold-and-rewrite on the work-extensivity identity.
Claim. Let $op:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ be work-extensive, i.e. $op(a,b)=a+b$ for all real $a,b$. For any geometric scale sequence $S$ (ratio $r>0$, $r\neq 1$) and any $n\in\mathbb{N}$, one has $op(S_0,S_1)=S_n$ if and only if $\mathrm{ledgerCompose}(S_0,S_1)=S_n$.
background
The module UnifiedForcingChain derives the full T0–T8 inevitability ladder from the Recognition Composition Law plus normalization and calibration. Near the φ-forcing segment (T6), one studies geometric scale sequences: structures carrying a positive ratio $r\neq 1$ and a scale map $n\mapsto S_n$ along that ratio.
Scale closure at a proposed index $n$ asks whether composing the two seed scales recovers the $n$-th scale. The ledger-native form uses ledgerCompose on those seeds. The parameterized form ScaleClosureAtWith replaces that fixed compose by an arbitrary binary operation $op$ on reals, so one can state closure relative to a chosen composition law.
WorkExtensiveScaleComposition is the theorem-facing package for the physical requirement that composition be extensive in the scale-as-work observable: $op(a,b)=a+b$. It exists precisely so proofs need not silently hard-code addition as ledger compose.
proof idea
Bidirectional constructor on the biconditional. Forward: assume ScaleClosureAtWith op S n, unfold both closure predicates, rewrite the hypothesis with h.work_extensive (so $op$ becomes $+$), and the goal is exactly ScaleClosureAt. Reverse: same unfolds in the opposite order, rewrite with h.work_extensive again, and close. No arithmetic beyond the extensivity identity is used.
why it matters
In the Complete Inevitability Chain, T6 forces φ as the self-similar fixed point of the discrete ledger. Scale-closure predicates are the local language for that self-similarity: composing seed scales must land on a later rung of the geometric sequence. This lemma licenses replacing an abstract work-composition operator by ledger compose (or the reverse) whenever extensivity holds, so later φ-forcing arguments can stay operator-agnostic until the additive law is imposed.
No downstream consumers are recorded yet; the result is infrastructure for the scale-closure layer rather than a cited parent theorem. It sits beside the work-extensive recognition-work model and the geometric-scale apparatus imported from PhiForcingDerived, tightening the bridge between cost/work observables and ledger arithmetic without touching T5 J-uniqueness or the eight-tick/D=3 steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.