lcm_eight_fortyfive_vp_characterization
plain-language theorem explainer
The theorem asserts that for any natural number p the p-adic valuation of 360 equals the maximum of the valuations of 8 and of 45. Number theorists working with prime exponents among Recognition Science constants would cite it to simplify repeated factorization steps. The proof is a short tactic sequence that first confirms nonzeroness then rewrites via the lcm identity and applies the general lcm valuation lemma.
Claim. For every natural number $p$, the exponent of $p$ in the prime factorization of 360 equals the maximum of the exponents of $p$ in 8 and in 45.
background
The module collects small decidable arithmetic facts about integers that recur in the reality repo, such as 8, 45, 360 and 840, serving as stable anchors that keep later bridge lemmas readable. The function vp p n extracts the exponent of p in the prime factorization of n. The upstream result vp_lcm states that for nonzero a and b the exponent of p in lcm(a,b) equals the maximum of the exponents in a and in b. The companion equality lcm 8 45 = 360 supplies the concrete identification used here.
proof idea
The tactic proof first obtains nonzeroness of 360, 8 and 45 via decide. It rewrites the left-hand side by the already-proved equality lcm 8 45 = 360, then concludes by exact application of the vp_lcm theorem on those three nonzero arguments.
why it matters
The declaration supplies a stable arithmetic identity inside the RSConstants module that supports prime-factor calculations involving 360. It sits alongside sibling facts such as eight_eq_two_pow_three and fortyfive_eq_three_sq_mul_five, reinforcing the eight-tick octave structure (period 2^3) and the factorization of 45. No downstream uses are recorded, leaving it as a leaf lemma whose value lies in preventing repeated arithmetic re-proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.