prime_sixhundredfiftythree
plain-language theorem explainer
653 is established as a prime integer. Number theorists using arithmetic functions for Möbius inversion or square-free checks in the Recognition Science setting would cite this fact when verifying small primes on the phi-ladder. The proof is a one-line wrapper that invokes native_decide to settle the claim by direct kernel computation.
Claim. $653$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ. Prime is the transparent alias for Nat.Prime. Upstream results include the Prime abbrev from Basic together with several 'is' structures from OptionAEmpiricalProgram, SimplicialLedger, GameTheory, and RamanujanBridge that enforce collision-free or tautological properties in the surrounding framework.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic, delegating the primality test for the concrete integer 653 to Lean's native computation engine.
why it matters
This declaration supplies a verified small prime required for arithmetic-function evaluations in the NumberTheory.Primes section. It supports Möbius calculations referenced in the module documentation without adding hypotheses. No direct connection to the T0-T8 forcing chain or phi-ladder appears here, yet the result populates the prime footholds needed for later inversion steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.