prime_sixhundredninetyone
plain-language theorem explainer
The declaration establishes that 691 is a prime number. Number theorists working with arithmetic functions such as the Möbius function in the Recognition Science setting would cite it for small-prime checks during calculations. The proof is a direct computational verification.
Claim. $691$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local setting keeps statements basic before layering Dirichlet algebra. Upstream results include the active edge count A from IntegrationGap, defined as 1 and satisfying the φ-power balance identity at D = 3: φ^(A − gap) · φ^gap = φ, equivalently φ^(−44) · φ^45 = φ; a parallel A from Masses.Anchor; and the Prime predicate from the Basic sibling module.
proof idea
The proof is a one-line wrapper that applies native_decide to confirm primality by direct computation.
why it matters
This supplies a basic verified fact inside the primes section of the arithmetic functions module. It has no listed downstream uses. It touches the number-theory scaffolding without direct reference to the forcing chain T0-T8, the Recognition Composition Law, or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.