FirstClosureLawCanonicality
plain-language theorem explainer
Packages three facts about geometric scale sequences: the first nontrivial closure index is uniquely 2, and the legacy closedness predicate is exactly closure at that index. Cited by the T5-to-T6 self-similarity bridge when forcing φ from discrete ledger hierarchy. The structure is a pure Prop bundle; uniqueness of certificates is by subsingleton (proof-irrelevant).
Claim. For a geometric scale sequence $S$ (ratio $r>0$, $r\neq 1$), the first-closure canonicality package asserts: (i) $2$ is a first nontrivial closure index (least $n$ with $1<n$); (ii) every first nontrivial closure index equals $2$; (iii) there exists $n$ such that $S$ closes at the first nontrivial index $n$ if and only if $S$ is closed in the existing sense.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The T5→T6 step forces the golden ratio φ as the self-similar fixed point of a discrete ledger hierarchy.
A GeometricScaleSequence is a positive scale ratio $r\neq 1$ with successive scales $r^n$. Closure of such a sequence is the algebraic condition that seed scales recombine at a finite index. FirstNontrivialClosureIndex n means $n$ is the least natural strictly above the seed index $1$. CanonicalFirstClosureLaw S n pairs that least-index fact with scale closure of $S$ at $n$.
This structure does not prove those facts; it names the Prop that packages them so later bridges can demand a single certificate rather than three loose hypotheses.
proof idea
Definitional: a structure of three Prop fields, no proof body. The companion Subsingleton instance is immediate by proof irrelevance (rfl on equality of Props). The actual content is discharged downstream by canonical_first_closure_law_canonicality, which fills first_index from firstNontrivialClosureIndex_two and proves uniqueness and the isClosed equivalence by direct case analysis on the least-above-seed characterization.
why it matters
Sits on the T5→T6 bridge path inside the complete inevitability chain. Downstream, canonical_first_closure_law_canonicality builds the inhabited package, and T5_To_T6_SelfSimilarity_Bridge consumes the closed-hierarchy data that this package equates with the legacy isClosed flag. Without a unique first nontrivial index fixed at 2, self-similarity would not pin a single scale ratio; with it, the discrete ledger forces φ (primer T6). The package also records that no extra closure notion is smuggled past the existing predicate, matching the bridge's explicit obstruction note that bare closed-observable fields alone do not force hierarchy fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.