superprime_eightythree
plain-language theorem explainer
The statement confirms that both 83 and 23 are prime natural numbers. Researchers applying arithmetic functions such as the Möbius function in the Recognition Science number theory layer would cite it to anchor explicit small-prime instances. The proof reduces to a single native decision procedure that resolves the primality predicates for these concrete values.
Claim. Let Prime$(n)$ denote that the natural number $n$ is prime. Then Prime$(83) land Prime$(23)$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, starting with the Möbius function. Prime is the repo-local alias for the standard Nat.Prime predicate on natural numbers. This places the result in the NumberTheory.Primes section, where small verified primes support later Möbius inversions and squarefree checks once the basic interfaces stabilize.
proof idea
The proof is a one-line term that invokes native_decide to discharge the conjunction of the two primality checks.
why it matters
The declaration supplies concrete prime instances required for arithmetic function evaluations in this file. It supports the number theory primitives that feed into Recognition Science constructions such as the phi-ladder and the T0-T8 forcing chain, although the current dependency graph lists no direct downstream uses. It fills a basic verification role without engaging open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.