prime_seven
plain-language theorem explainer
Seven is prime. Researchers constructing RS constant factorizations cite this when anchoring wheel arithmetic for gaps and masses. The proof is a one-line decision that verifies the primality predicate holds for 7.
Claim. The integer $7$ is prime.
background
This module gathers small decidable arithmetic facts on integers that recur in Recognition Science calculations, such as the primes 5, 7, 11, 17, 37, 103, 137 and relations including eight equals two cubed and forty-five equals three squared times five. The local setting treats these facts as stable anchors that keep later bridge lemmas readable and avoid repeated arithmetic proofs. The definition of primality is taken from the Basic module in the same directory.
proof idea
The proof applies the decide tactic directly to the primality statement, reducing it to a finite exhaustive check of possible divisors.
why it matters
This theorem supplies a basic arithmetic anchor inside the NumberTheory.Primes section. It supports wheel-factorization derivations that feed into gap and mass calculations, consistent with the eight-tick octave and phi-ladder structures in the Recognition framework. No downstream uses appear in the current dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.