PrimeLedgerAtom
A structure definition that declares a natural number p to be a prime ledger atom precisely when it is a classical prime and satisfies the multiplicative irreducibility condition that every factorization p = a * b forces a = 1 or b = 1. Researchers bridging classical number theory to the Recognition Science arithmetic ledger cite this when preparing the Euler product for J-cost weighting. The declaration is a direct structure definition with no proof obligations or lemmas.
claimA natural number $p$ is a prime ledger atom when $p$ is prime and, for all natural numbers $a,b$, the equality $p = a b$ implies $a=1$ or $b=1$.
background
The module grounds the arithmetic ledger that precedes the RH bridge in Recognition Science. Positive integers function as states of the multiplicative ledger, and the structure isolates those states that are irreducible under multiplication. This classical setup is required before the primes are weighted by J-cost into the Euler ledger. The upstream multiplicative theorem from CostAlgebra supplies the automorphism that preserves the product operation used in the irreducibility clause.
proof idea
The declaration is a structure definition that directly records the two fields: ordinary primality from Mathlib and the universal quantification expressing ledger irreducibility. No tactics, reductions, or upstream lemmas are invoked; the definition itself supplies the predicate.
why it matters in Recognition Science
PrimeLedgerAtom supplies the base predicate for the equivalence theorems primeLedgerAtom_iff_prime and prime_is_ledger_atom inside the same module, and for the recovered-logic versions PrimeLedgerAtomLogic and PrimeLedgerLogicCert downstream. It identifies the irreducible postings of the multiplicative ledger before J-cost weighting begins, consistent with the Recognition Composition Law and the transition from arithmetic to spectral emergence. The definition closes the classical arithmetic interface required by the eight-tick octave and D=3 spatial forcing chain.
scope and limits
- Does not assign J-cost values or phi-ladder rungs to the atoms.
- Does not extend the predicate to LogicNat or recovered integers.
- Does not assert infinitude or density of such atoms.
- Does not incorporate gauge or spectral content from upstream structures.
- Does not address the Euler product or zeta-function weighting.
formal statement (Lean)
19structure PrimeLedgerAtom (p : ℕ) : Prop where
20 prime : Nat.Prime p
21 irreduciblePosting : ∀ a b : ℕ, p = a * b → a = 1 ∨ b = 1
22
23/-- Positive integers are the states of the multiplicative integer ledger. -/