superprime_onehundredfiftyseven
plain-language theorem explainer
The declaration asserts that 157 and 37 are both prime, marking 157 as the superprime tied to 37 in the RS prime sequence. Number theorists building arithmetic ladders or phi-scaled mass formulas would reference this concrete anchor. The proof is a direct computational check via native_decide on the primality predicates.
Claim. $157$ and $37$ are both prime numbers, with $157$ the superprime associated to $37$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for the standard Nat.Prime predicate. The local setting is the NumberTheory.Primes section, where such facts support later Dirichlet inversion and squarefree checks.
proof idea
The proof is a one-line term proof that applies native_decide to evaluate Prime 157 and Prime 37 directly in the kernel.
why it matters
This anchors the superprime sequence used in RS mass formulas and the phi-ladder. It supplies concrete values for the prime rung in the eight-tick octave and D=3 spatial structure. No downstream theorems yet reference it, leaving its placement in the forcing chain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.