CanonicalFirstClosureLaw
plain-language theorem explainer
Packages scale closure of a geometric sequence at the least index strictly above the seed. Anyone citing first-closure uniqueness, minimal hierarchies, or the canonical φ scale sequence uses this predicate. It is a two-field Prop structure (first nontrivial index plus ledger composition equality), propositionally unique by subsingleton.
Claim. For a geometric scale sequence $S$ with ratio $r>0$, $r\neq 1$, and $n\in\mathbb{N}$, a canonical first-closure law at $n$ asserts: (i) $n$ is the least natural with $n>1$; (ii) ledger composition of the seed scales equals the $n$-th scale, $\mathrm{compose}(S_0,S_1)=S_n$.
background
The module UnifiedForcingChain derives the full T−1 through T8 chain from the Recognition Composition Law plus normalization and calibration: logic, MP, discreteness, ledger, unique $J$, $\varphi$, the eight-tick octave, and $D=3$ are treated as forced, not assumed.
A geometric scale sequence is a positive ratio $r\neq 1$ with scales $S_n$. Scale closure at index $n$ means the ledger composition of the two seed scales recovers $S_n$. The first nontrivial closure index is the least $n$ with $n>1$ (hence uniquely $2$ once existence is fixed).
This structure simply conjoins those two Props for fixed $S$ and $n$, giving a named interface for “closes at the first nontrivial rung” used throughout the $\varphi$-forcing and hierarchy-minimality layer.
proof idea
Definitional packaging, not a derived theorem. The structure has two fields: FirstNontrivialClosureIndex n (above seed and least such) and ScaleClosureAt S n (ledgerCompose of scales 0 and 1 equals scale $n$). The accompanying Subsingleton instance is immediate: any two inhabitants are equal by rfl because both fields are Props.
why it matters
Gives the clean interface that later results identify with the older isClosed predicate: existence of some $n$ with this law is equivalent to $S$ being closed. Downstream, every minimal hierarchy supplies such a law for its scales, and the canonical $\varphi$ scale sequence is shown to carry one. The companion canonicality package pins the first nontrivial index uniquely at $2$ and equates old closure with closure at that index.
In the forcing chain this sits under T6 ($\varphi$ forced by self-similarity on the discrete ledger): first nontrivial scale closure is the minimal self-similar return that selects the geometric $\varphi$ hierarchy rather than an arbitrary ratio. It does not itself derive $\varphi$ or T7–T8; it standardizes the closure side-condition those steps consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.