firstNontrivialClosureIndex_unique
plain-language theorem explainer
Any natural number that is the least index strictly above the seed level 1 must equal 2. Closure-law and geometric-scale arguments in the unified forcing chain cite this uniqueness pin. The proof is a two-sided inequality: leastness gives n ≤ 2, and above-seed gives 2 ≤ n, then antisymmetry.
Claim. If $n \in \mathbb{N}$ is a first nontrivial closure index (that is, $1 < n$ and $n$ is least among all naturals strictly larger than $1$), then $n = 2$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Inside that chain, geometric scale sequences and first-closure laws need a canonical discrete index for the first nontrivial closed level above a seed.
A first nontrivial closure index is a natural $n$ with two properties: it sits strictly above the seed index $1$, and it is least among all such indices. The seed is fixed at $1$; the next candidate is therefore forced by order on $\mathbb{N}$ alone, before any $\varphi$-ladder or ledger composition enters.
Downstream packages treat this unique index as the first-closure slot in a geometric scale sequence, equating a canonical first-closure law with the existing closedness predicate on that sequence.
proof idea
From leastness applied at $m = 2$ (which satisfies $1 < 2$ by norm_num), obtain $n \le 2$. From the above-seed hypothesis $1 < n$, obtain $2 \le n$ via Nat.succ_le_of_lt. Finish with Nat.le_antisymm on the two inequalities. No cost functional, ledger, or $\varphi$ identity is used; the argument is pure order on naturals.
why it matters
This uniqueness pin feeds canonical_first_closure_law_canonicality (the canonical first-closure law package on a geometric scale sequence) and canonical_first_closure_law_iff_isClosed (equating existence of a canonical first-closure law with the sequence being closed). In the forcing chain it stabilizes the discrete first step above the seed before T6–T8 material ($\varphi$, eight-tick octave, $D = 3$) is attached to scale geometry. Without a unique first nontrivial index, canonicality of the first-closure law would be ambiguous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.