PrimeLedgerCert
plain-language theorem explainer
PrimeLedgerCert records the exact match between PrimeLedgerAtom and ordinary primality in natural numbers, excludes 1 from the ledger atoms, and confirms that primes are positive integers. Number theorists assembling the Recognition Science bridge to the Riemann hypothesis cite this certificate when they need the classical arithmetic foundation before forming the Euler product. The declaration is a plain structure whose three fields are later instantiated by sibling lemmas in the same module.
Claim. A certificate consisting of three assertions: (i) for every natural number $p$, PrimeLedgerAtom$(p)$ holds if and only if $p$ is prime; (ii) 1 is not a PrimeLedgerAtom; (iii) every prime $p$ satisfies IntegerLedgerState, i.e., $p > 0$.
background
The Prime Ledger Atoms module grounds the arithmetic ledger used by the RH bridge. Primes are exactly the irreducible postings of the multiplicative positive-integer ledger; the RS work starts after this point, when the prime postings are weighted into the Euler ledger. PrimeLedgerAtom is the structure requiring both that $p$ is prime and that $p = a b$ forces $a=1$ or $b=1$. IntegerLedgerState is the predicate $0 < n$ on positive integers.
proof idea
The declaration is a structure definition that simply names the three required fields. No tactics or reductions occur inside the structure itself; the fields are supplied by the separate lemmas primeLedgerAtom_iff_prime, one_not_primeLedgerAtom and prime_is_positive_ledger_state when the instance primeLedgerCert is constructed.
why it matters
PrimeLedgerCert is required by EulerLedgerPartitionCert to equate the finite prime-ledger partitions with the Euler product for Re(s) > 1, and by both RSPhysicalThesisDataLogic and RSPhysicalThesisData to retain a classical prime ledger alongside the analytic zeta stack. It supplies the arithmetic base before the Recognition Composition Law or the T0-T8 forcing chain is invoked to derive physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.