superprime_eleven
plain-language theorem explainer
The declaration asserts that both 11 and 5 are prime natural numbers. Researchers constructing the phi-ladder mass assignments in Recognition Science would cite this to anchor the rung-5 and rung-11 cases. The proof is a one-line term that invokes native_decide to evaluate the primality predicates directly.
Claim. $11$ and $5$ are both prime natural numbers, where primality is the standard predicate on the naturals.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This theorem appears in the primes section yet addresses only primality rather than inversion formulas. The local setting keeps statements minimal until Dirichlet algebra layers stabilize. Upstream, Prime is defined as the transparent alias for Nat.Prime, while the listed foundation modules supply collision-free and algebraic-tautology structures that native_decide relies upon for evaluation.
proof idea
The proof is a term-mode one-liner that applies native_decide to discharge both primality checks by compile-time evaluation.
why it matters
It supplies a verified base case for superprimes relevant to the Recognition Science mass formula on the phi-ladder. The result aligns with the T5 J-uniqueness step and the eight-tick octave structure, though no downstream theorems yet consume it. This leaves open its precise integration into the full forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.