repunit_three_composite
plain-language theorem explainer
111 factors as 3 times 37 and is therefore composite. Number theorists verifying small repunit cases in Recognition Science arithmetic contexts would cite this result. The proof is a direct computational check via native_decide.
Claim. $¬ Prime(111) ∧ 111 = 3 × 37$, where Prime is the standard predicate for natural-number primality.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local setting keeps statements minimal to support later Dirichlet algebra. Prime is the repository alias for Nat.Prime.
proof idea
One-line term proof that invokes native_decide to confirm the factorization and non-primality.
why it matters
It records the explicit factorization of the third repunit, flagged as RS-relevant through the factor 37. The result sits in the primes arithmetic functions section with no downstream uses recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.