superprime_onehundredseventynine
plain-language theorem explainer
The declaration confirms that both 179 and 41 are prime numbers, labeling 179 as a superprime in the local sequence. Number theorists working with arithmetic functions or prime ladders in the Recognition Science framework would cite this for concrete verification steps. The proof is a one-line term wrapper that invokes native_decide for direct computational settlement.
Claim. $179$ and $41$ are both prime.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. Local notation defines Prime as the standard natural number primality predicate from the Basic import. Upstream results supply foundational structures such as collision-free classes from OptionAEmpiricalProgram, algebraic tautologies from SimplicialLedger, and the mock theta construction from the Ramanujan bridge.
proof idea
The proof is a term-mode wrapper consisting of a single native_decide tactic that evaluates the conjunction of the two primality statements by direct computation.
why it matters
This supplies a concrete prime verification inside the arithmetic functions section. It has no listed downstream applications and stands as an isolated check. The result supports sequence construction in the framework but does not engage the forcing chain, RCL, or constants such as phi or alpha inverse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.