coprime_eight_fortyfive_vp
plain-language theorem explainer
The theorem shows that the p-adic valuation of gcd(8,45) vanishes for every natural number p. Number theorists maintaining the RS constants file would cite it to confirm that 8 and 45 share no prime factors. The proof is a one-line wrapper that rewrites the gcd to its known value of 1 and applies simplification.
Claim. For every natural number $p$, the $p$-adic valuation $v_p$ of the greatest common divisor of 8 and 45 equals zero.
background
The RSConstants module collects small decidable arithmetic facts about integers that recur in the reality repo, including 8, 45, 360, and 840. These facts act as stable anchors that keep later bridge lemmas readable without repeated arithmetic proofs. The function vp p n extracts the exponent of prime p in the factorization of n. The upstream lemma gcd_eight_fortyfive_eq_one states that Nat.gcd 8 45 = 1 and is proved by native_decide.
proof idea
The proof is a one-line wrapper that rewrites using gcd_eight_fortyfive_eq_one to replace the gcd with 1, then applies simp to obtain the zero valuation.
why it matters
This declaration supplies a basic coprimeness fact that supports the collection of decidable anchors in the Recognition Science framework. It keeps arithmetic transparent for lemmas involving the eight-tick octave and phi-ladder. No downstream uses are recorded and no open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.