superprime_onehundredninetyone
plain-language theorem explainer
The declaration asserts that both 191 and 43 are prime numbers. Number theorists building prime lists inside the Recognition Science arithmetic scaffolding would cite this instance for verification of specific values. The proof is a one-line wrapper that invokes native_decide to evaluate the primality predicates directly.
Claim. The natural numbers 191 and 43 are both prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for Nat.Prime supplied by the Basic submodule. Upstream results include the is structures from OptionAEmpiricalProgram, SimplicialLedger, MechanismDesignFromSigma, and MockThetaPhantom, each marking collision-free or tautological properties, plus the Prime alias itself.
proof idea
The proof is a term-mode one-line wrapper that applies native_decide to discharge the conjunction of primality statements for 191 and 43.
why it matters
The result supplies a concrete prime fact inside the NumberTheory.Primes layer that supports later arithmetic-function statements such as those involving μ. It sits downstream of the Prime alias and aligns with the framework's use of explicit number-theoretic checks in the forcing chain. No downstream uses are recorded and no open scaffolding questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.