vp_fortyfive_five
plain-language theorem explainer
The 5-adic valuation of 45 equals 1. Modelers working with Recognition Science constants cite this when confirming the prime factors in the LCM of 8 and 45 that yields 360. The proof is a one-line native_decide tactic that evaluates the valuation directly from integer factorization.
Claim. $v_5(45) = 1$
background
This module gathers small decidable arithmetic facts about integers that recur across the Recognition Science codebase, such as the numbers 8, 45, 360, and 840 together with prime markers 11, 17, 37, 103, and 137. These facts function as stable anchors that keep later bridge lemmas readable by avoiding repeated arithmetic proofs. The local setting is the collection of prime factorization and valuation utilities imported from Mathlib along with the sibling Basic and Factorization files.
proof idea
One-line wrapper that applies the native_decide tactic to the equality vp 5 45 = 1.
why it matters
This theorem supplies a basic arithmetic anchor for the prime spectrum of 360, which appears in LCM calculations central to the RS constants. It supports the factorization lemmas in the same module, including threehundredsixty_factorization and wheel840_factorization. In the framework it contributes to the stable numerical foundations required for the phi-ladder and J-cost structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.