int_mul_log_phi_valid_step
plain-language theorem explainer
The lemma shows that for any integer n the quantity n ln φ qualifies as a valid single-step displacement. Researchers closing the GCIC discrete gauge gap or building 8-tick trajectories cite it as the basic generator of the φ-lattice. The proof is a direct term-mode construction that witnesses the existential quantifier by supplying n and reflexivity.
Claim. For every integer $n$, the displacement $n$ ln φ satisfies the valid-step predicate: there exists an integer $k$ such that $n$ ln φ equals $k$ ln φ.
background
The declaration sits inside the module that formalizes Mechanism A of the GCIC Response paper. That module derives the discrete gauge identification r ~ r + n ln φ from two forcing-chain results: T6 (each tick changes the log-ratio by an integer multiple of ln φ) and T7 (the sum of eight consecutive changes is zero). ValidStep is the predicate that a real displacement equals some integer multiple of ln φ. Upstream constants supply the tick as the fundamental time quantum and A as the active edge count per tick, which anchor the integration gap and mass formulas used in the surrounding development.
proof idea
The proof is a one-line term-mode wrapper. It constructs the witness for the existential quantifier inside the valid-step predicate by taking the supplied integer n and applying reflexivity to the equality.
why it matters
The lemma supplies the elementary generator for valid steps that the module documentation uses to reach the 8-tick compactification theorem. It thereby converts the acknowledged explicit input of the GCIC paper into a derived consequence of T6 and T7, supporting the Bloch-analogy argument that the φ-lattice plus eight-tick periodicity forces a compact phase in ℝ/ℤ. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.