FirstNontrivialClosureIndex
plain-language theorem explainer
A natural number n is a first nontrivial closure index when it is the least integer strictly larger than the seed index 1. Anyone packaging scale-closure laws on geometric phi-sequences cites this predicate. It is a pure Prop structure with two fields (strictly above seed, and least such), so there is no proof body.
Claim. A natural number $n$ is a first nontrivial closure index if $n > 1$ and $n \le m$ for every natural number $m > 1$. Equivalently, $n$ is the least natural number strictly above the seed index $1$.
background
The Unified Forcing Chain module aims to show that T0 through T8 are forced from the cost foundation (Recognition Composition Law, normalization, calibration), starting from an absolute floor. Within that chain, geometric scale sequences on the phi-ladder admit a notion of scale closure at an index: seed scales close after a discrete number of steps.
The seed index is taken to be 1. Anything that counts as a nontrivial closure must sit strictly above that seed. The present structure packages exactly that least-above-seed condition as a Prop on $n$, so later statements can say "closure at the first nontrivial index" without hard-coding the numeral 2 into every hypothesis.
Downstream packages such as CanonicalFirstClosureLaw and FirstClosureLawCanonicality then attach actual scale-closure data to this index predicate and prove that the only such index is 2.
proof idea
No proof: this is a Prop-valued structure (definition). The two fields are the strict inequality $1 < n$ and the leastness universal $\forall m,, 1 < m \to n \le m$. Inhabitants are constructed later by firstNontrivialClosureIndex_two (norm_num plus omega) and uniqueness is discharged by firstNontrivialClosureIndex_unique via antisymmetry of $\le$.
why it matters
This predicate is the index half of the first-closure law package. CanonicalFirstClosureLaw requires index_is_first : FirstNontrivialClosureIndex n together with scale closure of a GeometricScaleSequence at that $n$. FirstClosureLawCanonicality packages existence at 2, uniqueness of any such index, and the identification of the older isClosed predicate with closure at that canonical index.
In the forcing chain this sits near the discrete self-similarity step that forces $\varphi$ (T6) and the subsequent eight-tick / $D=3$ layer (T7-T8): scale closure must begin at a definite first nontrivial rung above the seed. Pinning that rung by a named Prop keeps the canonicality theorems free of magic constants in their hypotheses while still forcing $n=2$ as a theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.