ValidStep
plain-language theorem explainer
ValidStep declares a real displacement delta to be valid precisely when it equals an integer multiple of the natural logarithm of the golden ratio. Researchers closing the acknowledged GCIC gap on discrete gauge invariance cite this predicate when establishing dynamical equivalence of log-ratios under the phi-lattice. The definition is a direct existential quantifier over the integers with no further hypotheses or lemmas.
Claim. A real number $δ$ is a valid step if there exists an integer $n$ such that $δ = n ln φ$, where $φ$ denotes the golden ratio.
background
The module derives the discrete gauge identification $r ~ r + n ln φ$ as a consequence of the forcing chain rather than an imposed input. T6 (phi-step) requires each tick to alter the log-ratio by an integer multiple of $ln φ$ from self-similarity $φ² = φ + 1$. T7 (8-tick neutrality) requires the sum of eight consecutive changes to vanish. The local setting is the Bloch analogy: the phi-lattice supplies the periodic potential while the eight-tick period supplies the crystal cell, yielding a compact phase without hand-imposed periodicity. Upstream, the Kronecker delta appears in Ndim connections but is not invoked here; the core prior results are the phi-forcing and discreteness lemmas imported from the foundation modules.
proof idea
The definition is introduced directly by the existential statement that delta equals some integer times the logarithm of phi. No lemmas are applied and no tactics are used; the body is the primitive predicate on which the subsequent lemma that every integer multiple is valid rests.
why it matters
This predicate supplies the base notion for the 8-tick compactification result that closes Gap A in the GCIC Response paper. It is used by the lemma establishing that $n ln φ$ is always a valid step for any integer $n$. The construction realizes the T6-T7 forcing chain inside the discrete gauge, mirroring Bloch theory and confirming that the compact phase follows from the existing Recognition Science landmarks rather than additional assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.