mod4_onehundredthree_prime
plain-language theorem explainer
103 is established as prime with residue 3 modulo 4. Number theorists applying Recognition Science to arithmetic properties of primes would cite this fact for its congruence class. The verification proceeds by direct computational decision via native_decide.
Claim. The integer $103$ is prime and satisfies $103 ≡ 3 mod 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local theoretical setting keeps statements minimal before deeper Dirichlet algebra is added. This theorem isolates the concrete property of 103 being prime with residue 3 modulo 4, noted as RS-relevant.
proof idea
The proof is a one-line wrapper that invokes native_decide to computationally verify both primality of 103 and the residue class modulo 4.
why it matters
This supplies a basic arithmetic fact relevant to Recognition Science applications involving primes congruent to 3 mod 4. It supports potential downstream number-theoretic constructions in the monolith, though no immediate parent theorems are listed. The result aligns with the arithmetic functions footholds but stands without explicit ties to T0-T8 forcing or J-cost structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.