ledger_atom_is_prime
plain-language theorem explainer
A natural number p qualifies as a prime ledger atom only if it is an ordinary prime. Number theorists grounding the multiplicative ledger for the Recognition Science RH bridge cite this to confirm that ledger atoms coincide with standard primes before weighting them into the Euler product. The proof is a one-line term extraction of the embedded Nat.Prime witness from the structure hypothesis.
Claim. If a natural number $p$ is a prime ledger atom (a prime integer equipped with the multiplicative irreducibility property), then $p$ is a prime natural number.
background
This module grounds the arithmetic ledger used by the RH bridge. Positive integers are the states of the multiplicative integer ledger, and primes are exactly its irreducible postings. The local setting is deliberately classical: the Recognition Science extensions begin only after these prime postings are weighted into the Euler ledger.
proof idea
The proof is a term-mode field projection. The hypothesis h has type PrimeLedgerAtom p, whose structure definition includes a field prime : Nat.Prime p; the term h.prime returns that witness directly.
why it matters
This supplies the forward direction of the equivalence primeLedgerAtom_iff_prime, which states PrimeLedgerAtom p ↔ Nat.Prime p. It anchors the base arithmetic for the Recognition Science framework before the J-function, phi-ladder, and eight-tick octave enter. The module doc-comment notes that RS work starts after this classical grounding step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.