prime_is_ledger_atom
plain-language theorem explainer
Natural numbers that are prime satisfy the PrimeLedgerAtom structure in the multiplicative ledger. Researchers bridging classical number theory to the Recognition Science RH framework cite this result to establish the base case for ledger atoms. The tactic proof supplies the primality field directly and derives the irreducibility condition from the divisor characterization of primes.
Claim. If $p$ is a prime natural number, then $p$ is a prime ledger atom: it carries the primality witness and satisfies that for all natural numbers $a,b$, if $p=a b$ then $a=1$ or $b=1$.
background
The module grounds the arithmetic ledger used by the RH bridge. Positive integers are states of the multiplicative integer ledger. The structure PrimeLedgerAtom requires a Nat.Prime witness together with the irreduciblePosting property that any factorization forces a unit factor. This sits before the Euler ledger construction. The upstream Prime abbrev is the transparent alias for Nat.Prime.
proof idea
Tactic-mode structure construction. It introduces the factorization $p=a b$, derives the divisibility $a|p$, applies the prime divisor lemma to split into cases $a=1$ or $a=p$, and resolves the second case by left-cancellation to obtain $b=1$.
why it matters
This theorem supplies the forward direction of the equivalence between ordinary primality and the ledger-atom property. It is invoked by the sibling iff theorem that equates the two notions. In the Recognition framework it grounds the arithmetic ledger before primes are weighted into the Euler product. No open questions are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.