pith. machine review for the scientific record. sign in
abbrev definition def or abbrev high

Prime

show as:
view Lean formalization →

This supplies a transparent local alias for the standard primality predicate on natural numbers. Modules constructing Gap-45 barriers and Euler-Mascheroni bounds cite it to keep a uniform namespace without repeated Mathlib imports. The implementation is a single-line abbreviation that directly delegates to Mathlib's Nat.Prime, inheriting all its decidability and proof infrastructure.

claimFor a natural number $n$, the predicate $P(n)$ holds if and only if $n$ satisfies the standard definition of primality in elementary number theory.

background

The module NumberTheory.Primes.Basic supplies basic prime-number footholds for the Recognition Science repository. Its design goals are to reuse Mathlib’s Nat.Prime, remain axiom-free and sorry-free, and grow upward into analytic number theory only after the algebraic layer stabilizes.

proof idea

The declaration is a one-line abbreviation that re-exports Mathlib’s Nat.Prime predicate under the local name Prime. No lemmas or tactics are applied; transparency ensures every property of Nat.Prime transfers directly.

why it matters in Recognition Science

This alias feeds BarrierCert, beat_is_prime, gapDiff_prime, shimmer_cert and ShimmerCert in the Gap45 modules, plus gamma_numerical_bounds. It underpins the eight-tick octave constructions by guaranteeing that the beat frequency 37 remains irreducible inside the 360-tick window.

scope and limits

Lean usage

theorem beat_is_prime : Prime 37 := by native_decide

formal statement (Lean)

  36abbrev Prime (n : ℕ) : Prop := Nat.Prime n

proof body

Definition body.

  37

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more