vp_840_seven
plain-language theorem explainer
The declaration states that the exponent of prime 7 in the factorization of 840 is exactly 1. Number theorists maintaining Recognition Science constant tables cite it to fix the prime content of 840 for later bridge lemmas. The proof reduces to a single native_decide call that evaluates the factorization directly.
Claim. $v_7(840)=1$, where $v_p(n)$ is the exponent of prime $p$ in the factorization of the natural number $n$.
background
The module assembles small decidable arithmetic facts about integers that recur in the reality repo, including 8, 45, 360, 840 and prime markers such as 11, 17, 37, 103, 137. These facts serve as stable anchors that keep later bridge lemmas readable without repeated arithmetic proofs. The function vp extracts the exponent of a given prime in the factorization of its second argument, implemented directly as the Mathlib factorization map.
proof idea
The proof is a one-line term that applies native_decide to compute the prime factorization of 840 and read off the exponent of 7.
why it matters
The result supplies one of the concrete prime facts required by the 840-wheel factorization and related lcm statements inside the RS constants module. It supports the prime markers that appear in the alpha band and the eight-tick octave constructions. No open questions remain; the arithmetic stub is closed by direct computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.