mod6_fortythree_prime
plain-language theorem explainer
43 is established as prime and congruent to 1 modulo 6. Number theorists verifying specific primes for arithmetic-progression conditions or Möbius-function calculations might reference this fact. The proof is a one-line wrapper that invokes native_decide to confirm the conjunction directly.
Claim. $43$ is a prime number and $43 ≡ 1 mod 6$.
background
The declaration appears in the module supplying lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ. The local setting keeps statements minimal until basic interfaces stabilize for later Dirichlet algebra. It depends only on the upstream definition of Prime as the transparent alias for Nat.Prime.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the conjunction of primality and the modular condition.
why it matters
This supplies a concrete prime instance inside the arithmetic-functions module. No downstream theorems are recorded yet, so it functions as a basic verification step rather than a parent result. In the Recognition Science setting it supplies a modular fact that could support later checks involving primes on the phi-ladder, though the connection remains undeveloped.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.