ScaleClosureAtWith
plain-language theorem explainer
Closure of a geometric scale sequence at index n under an arbitrary binary scale operation is the statement that composing the zeroth and first scales equals the n-th scale. Anyone comparing work-extensive composition laws to additive ledger composition cites this predicate. The body is a one-line propositional definition, not a proved claim.
Claim. Fix a binary operation $\mathrm{op}:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$, a geometric scale sequence $S$ (positive ratio $r\neq 1$), and $n\in\mathbb{N}$. Scale-closure at $n$ under $\mathrm{op}$ holds precisely when $\mathrm{op}(S_0,S_1)=S_n$, where $S_k$ is the $k$-th term of $S$.
background
The ambient module is the Unified Forcing Chain: T-1 through T8 are derived as inevitabilities from the Recognition Composition Law plus normalization and calibration. Scale structure enters near T6 ($\varphi$ forced by self-similarity in the discrete ledger) and the geometric ladders used downstream for mass and cosmology.
A geometric scale sequence is a structure carrying a ratio $r>0$ with $r\neq 1$, together with the $n$-th scale term built from that ratio. Additive ledger composition is the binary map $(a,b)\mapsto a+b$; it is the default way two ledger scales combine. The present definition abstracts that combination to an arbitrary binary operation on $\mathbb{R}$, so one can state closure without fixing the law of composition.
Related scale objects in the import graph include the pure $\varphi$-power ladder $k\mapsto\varphi^k$ used in large-scale structure, and stage chains in the primitive recognition calculus; those supply concrete sequences once a ratio is chosen.
proof idea
Definitional, not a proof. The predicate is the equality $\mathrm{op}(S.\mathrm{scale},0,,S.\mathrm{scale},1)=S.\mathrm{scale},n$. No lemmas are applied; the body is a single propositional equation used as a reusable interface for later equivalences.
why it matters
This predicate is the left-hand side of the equivalence scaleClosureAtWith_iff_ledgerCompose: under a work-extensive scale composition hypothesis, closure for an arbitrary operation is the same as ordinary scale-closure under additive ledger composition. That comparison lets the forcing chain treat work-extensive laws and ledger addition as interchangeable when asking whether two base scales generate a later rung.
In the T0–T8 story this sits with T6 ($\varphi$ forced as the self-similar fixed point) and the geometric scale ladders that feed mass formulas and cosmology. It does not itself force $\varphi$ or the eight-tick octave; it only packages the closure question so the chain can swap composition laws without rewriting every statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.