vp_360_five
plain-language theorem explainer
The exponent of prime 5 in the factorization of 360 equals 1. Modelers building Recognition Science constants cite this fact to anchor repeated arithmetic in bridge lemmas without re-deriving factorizations. The proof is a one-line native_decide tactic that evaluates the factorization function on the concrete pair.
Claim. The exponent of 5 in the prime factorization of 360 is 1, i.e., $v_5(360)=1$.
background
The RSConstants module assembles small decidable arithmetic facts about integers that recur in the repo, including 8, 45, 360, 840 and the prime markers 11, 17, 37, 103, 137. These facts serve as stable anchors that keep later bridge lemmas readable by avoiding repeated arithmetic proofs. The function vp p n returns the exponent of prime p in the factorization of n, implemented directly as n.factorization p.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute the factorization of 360 and extract the coefficient of 5.
why it matters
This theorem supplies one of the concrete arithmetic anchors collected in RSConstants. It belongs to the family of prime-exponent facts that support the broader set of decidable constants used across the Recognition Science framework, including the eight-tick octave and phi-ladder constructions. No downstream uses are recorded, but the fact prevents re-proving the same arithmetic in multiple bridge lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.