canonical_first_closure_law_canonicality
plain-language theorem explainer
For any geometric scale sequence, the first nontrivial closure index is uniquely 2, and the first-closure law is equivalent to the existing closedness predicate. Anyone citing the T5–T6 self-similarity bridge or φ-forcing from closed scales needs this package. The proof assembles three prior lemmas into the structure fields.
Claim. Let $S$ be a geometric scale sequence (ratio $r>0$, $r\neq 1$). Then the first-closure law canonicality package holds for $S$: the first nontrivial closure index exists and equals $2$; any first nontrivial closure index equals $2$; and $S$ satisfies the canonical first-closure law at some index if and only if $S$ is closed.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T5 pins the unique cost $J$; T6 forces the golden ratio $\varphi$ as the self-similar fixed point of a discrete ledger.
A geometric scale sequence is a positive ratio $r\neq 1$ with scales built by successive powers of that ratio. Closure of such a sequence is the discrete self-similarity condition that feeds $\varphi$-forcing: the first nontrivial place where the sequence can close is the structural seed of the T5-to-T6 bridge.
The structure packaged here records three facts together: existence of first nontrivial closure at index 2, uniqueness of that index, and equivalence between the first-closure law and the older isClosed predicate on the sequence.
proof idea
Term-mode structure construction with three field fillers. Existence of the first nontrivial index at 2 is supplied by firstNontrivialClosureIndex_two. Uniqueness is a one-line intro-and-apply of firstNontrivialClosureIndex_unique. Equivalence of the first-closure law with closedness is the prior lemma canonical_first_closure_law_iff_isClosed applied to $S$. No new arithmetic is done here; the package only bundles those three results.
why it matters
This package is a direct dependency of t5_to_t6_bridge_holds, which states that the T5-to-T6 self-similarity bridge is theorem-backed once $J$-uniqueness is available. That bridge is the formal link from T5 (unique $J$ from d'Alembert, normalization, calibration) to T6 ($\varphi$ forced by self-similarity in the discrete ledger).
In the forcing chain, closed geometric scales with canonical first index 2 are the concrete objects that realize the self-similar fixed point. Without uniqueness of the first nontrivial closure index and without the equivalence to the existing closedness predicate, the realized-closed-scale arm of the T5–T6 bridge would not be well-defined. The declaration therefore sits at the foundation of $\varphi$-forcing rather than at a peripheral lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.