one103_is_prime
plain-language theorem explainer
The integer 1103 is established as prime. Researchers examining Ramanujan's 1/π series in Recognition Science cite the result to confirm that 1103 does not factor into RS topological integers such as 11. The verification proceeds by a single native decision tactic that checks the primality predicate directly on the constant.
Claim. $1103$ is a prime natural number.
background
The module treats Ramanujan's rapidly convergent series for 1/π, whose denominators contain the integers 396 = 2² × 3² × 11 and 9801 = 99². These incorporate the RS topological integer 11, identified as the number of passive field edges of Q₃. The constant 1103 appears in the numerator term (1103 + 26390n) and originates in the class-number theory of the quadratic field Q(√−163), the largest Heegner discriminant. The upstream alias Prime (n : ℕ) := Nat.Prime n supplies the predicate used in the signature.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the primality goal for 1103.
why it matters
The theorem supplies the primality fact required by the downstream RamanujanPiCert structure, which assembles the full set of RS connections for the π-series (passive_11, divisibility of 396 by 11, and square divisibility of 9801). It implements the explicit statement in the module documentation that 1103 does not decompose into products of RS integers, preserving its separate origin in Heegner theory while the 8-tick octave forces π itself. No open scaffolding remains for this constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.