canonical_first_closure_law_iff_isClosed
plain-language theorem explainer
Existence of a canonical first-closure law on a geometric scale sequence is equivalent to the sequence being closed. Anyone packaging hierarchy minimality or the φ scale sequence into a first-closure witness cites this bridge. The proof is a two-direction term argument: uniqueness of the first nontrivial index one way, and the fixed witness index 2 the other.
Claim. For any geometric scale sequence $S$ (ratio $r>0$, $r\neq 1$), there exists a natural number $n$ such that $S$ obeys the canonical first-closure law at $n$ if and only if $S$ is closed. Here the canonical first-closure law at $n$ means: $n$ is the first nontrivial closure index, and the seed scales of $S$ close at that index.
background
The ambient module is the Unified Forcing Chain: T-1 through T8 forced from the Recognition Composition Law plus normalization and calibration. Geometric scale sequences (from PhiForcingDerived) are the discrete self-similar ladders that carry the φ-forcing story (T6): a positive ratio not equal to one, with successive scales $r^n$.
A canonical first-closure law packages two facts: the index is the first nontrivial closure index, and scale closure holds at that index (seed scales identify under the sequence action). The predicate isClosed on a geometric scale sequence is the existing closedness flag for those seed scales; the doc-comment states the equivalence bluntly: a canonical first-closure law is exactly that predicate.
Upstream, the first nontrivial closure index is pinned at 2 in this development, so closedness is a concrete finite check rather than an open search over $\mathbb{N}$.
proof idea
Bidirectional constructor on the biconditional.
Forward: from an existential witness $n$ with a canonical first-closure law, uniqueness of the first nontrivial closure index rewrites that $n$ to the canonical index; unfolding scale-closure-at then yields the closedness predicate on $S$.
Backward: assume $S$ is closed. Supply the concrete witness $n=2$ via the lemma that the first nontrivial closure index is two, then unfold scale-closure-at and transport closedness into the required closure-at-first field.
No induction or analytic estimates; pure propositional packaging around the unique first index.
why it matters
This lemma is the conversion hinge between the geometric closedness flag and the structured first-closure law used by hierarchy and φ-scale arguments. Downstream, minimal hierarchies obtain a first-closure law by applying the reverse direction to their minimal-closure hypothesis; the canonical φ scale sequence does the same from its closedness theorem. The canonicality package then builds on the same bridge to assert uniqueness of the first index and the full first-closure law package.
In the forcing chain this sits under T6 (φ forced as the self-similar fixed point) and the discrete geometric ladder that feeds T7's eight-tick octave. It does not itself force φ or dimension; it makes closedness interchangeable with the law-shaped object later steps quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.