vp_360_seven
plain-language theorem explainer
The declaration establishes that the 7-adic valuation of 360 is zero, confirming 7 does not divide 360. Authors constructing the prime spectrum for the wheel modulus 840 cite this fact to fix the exact set {2, 3, 5, 7}. The proof is a one-line native_decide tactic that evaluates the decidable equality in constant time.
Claim. The 7-adic valuation of the integer 360 vanishes: $v_7(360) = 0$.
background
This module assembles small decidable arithmetic facts about integers that recur throughout the Recognition Science development, including factorizations of 8, 45, 360 and 840 together with selected primes 11, 17, 37, 103 and 137. These anchors keep later bridge lemmas free of repeated arithmetic. The local setting is the collection of prime facts needed for the wheel modulus whose cyclic carrier size is given by modulus(k) = k + 2.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the equality vp 7 360 = 0 directly, relying on the decidability of integer valuation supplied by the Factorization import.
why it matters
This fact completes the prime spectrum of 840 by showing that 7 appears in the wheel modulus factorization but not in 360 itself. It supports the modular realizations whose modulus definition appears in ModularLogicRealization. Within the Recognition framework it supplies a stable arithmetic constant for the eight-tick octave and the D = 3 spatial dimensions used in phi-ladder calculations. No open questions remain; the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.