ScaleClosureAt
plain-language theorem explainer
Seed-scale closure for a geometric scale sequence at a proposed index: the ledger sum of the zeroth and first scales equals the scale at that index. Downstream first-closure laws and the T5-to-T6 self-similarity bridge cite this predicate as the bare closure atom. It is a pure definitional Prop (equality under additive ledger composition), with no proof obligations.
Claim. Let $S$ be a geometric scale sequence (positive ratio $r \neq 1$) and let $n \in \mathbb{N}$. The seed scales of $S$ close at index $n$ when the ledger composition of the zeroth and first scales equals the $n$-th scale, i.e. $S_0 + S_1 = S_n$.
background
The Unified Forcing Chain module derives T0 through T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The T5-to-T6 step needs a precise notion of when discrete scales close under composition, so that self-similarity can force the golden ratio $\varphi$.
A geometric scale sequence carries a fixed ratio $r > 0$ with $r \neq 1$ and an indexed family of real scales. Ledger composition is ordinary addition of two scale values: composing $a$ and $b$ yields $a+b$. That additive law is the canonical model of work-extensive scale composition used throughout the forcing chain.
This definition packages the elementary equality "seed scales sum to the $n$-th scale" as a named proposition, so later structures can talk about first nontrivial closure indices without repeating the arithmetic.
proof idea
Definitional abbreviation only. The body is the single equality ledgerCompose (S.scale 0) (S.scale 1) = S.scale n, which unfolds to $S_0 + S_1 = S_n$. No tactics, no lemmas, no hypotheses beyond the type of $S$.
why it matters
This is the bare closure atom for the self-similarity layer of the forcing chain. CanonicalFirstClosureLaw wraps it with the requirement that $n$ is the first nontrivial closure index; the equivalence theorems then identify that package with the existing isClosed predicate on geometric sequences.
Work-extensive and nonnegative-work composition models are shown equivalent to this ledger form (scaleClosureAtWith_iff_ledgerCompose, scaleClosureAtWithNonnegative_iff_ledgerCompose, canonical_nonnegative_work_closure_iff_ledger), so every composition story collapses to the same Prop.
The T5-to-T6 bridge certificate routes through closed hierarchy dynamics that force the scale ratio to be $\varphi$ (primer landmark T6). Without a named seed-closure predicate, that bridge could not state "the seeds close" independently of a particular composition operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.