PrimeLedgerAtom
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.