prime_sixhundredfortythree
plain-language theorem explainer
643 is established as a prime number. Number theorists applying arithmetic functions such as the Möbius function within the Recognition Science framework would reference this fact for calculations involving 643. The proof is a direct term-mode invocation of native_decide that evaluates the primality predicate.
Claim. $643$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the local transparent alias for Nat.Prime. Upstream results include foundational 'is' predicates from option, simplicial ledger, game theory, and Ramanujan bridge modules that record collision-free or algebraic properties.
proof idea
The proof is a one-line term that applies native_decide to discharge the primality goal for 643.
why it matters
This supplies a verified prime fact inside the arithmetic functions module to support Möbius and related definitions. It contributes concrete number-theoretic building blocks without direct ties to the T0-T8 forcing chain or RCL. No parent theorems appear in the used_by edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.