primeLedgerCert
plain-language theorem explainer
The prime ledger certificate packages the equivalence between prime ledger atoms and standard primes, the exclusion of the unit as an atom, and the positivity of prime ledger states. Researchers constructing the Euler product decomposition or the logic-aware RH data bundle cite this certificate as the arithmetic foundation. It is realized as a structure definition that directly supplies the three required fields from their respective supporting theorems.
Claim. The prime ledger certificate asserts that a natural number $p$ is a prime ledger atom if and only if it is prime, that 1 is not a prime ledger atom, and that every prime $p$ induces a positive integer ledger state.
background
This module establishes the classical arithmetic ledger that underpins the Recognition Science bridge to the Riemann hypothesis. Primes function as the irreducible elements in the multiplicative positive-integer ledger. The PrimeLedgerCert structure collects three properties: the biconditional between PrimeLedgerAtom and Nat.Prime, the negation for 1, and the positivity map for primes.
proof idea
The definition constructs the PrimeLedgerCert record by assigning each field to the corresponding upstream theorem: atom_iff_prime to primeLedgerAtom_iff_prime, one_not_atom to one_not_primeLedgerAtom, and prime_positive to prime_is_positive_ledger_state. No additional reasoning is required beyond these direct references.
why it matters
This certificate supplies the arithmetic base for the prime ledger in the Recognition Science framework, feeding directly into the Euler ledger partition certificate and the boundary transport constructions for the physical thesis data. It closes the classical number-theoretic foundation before the Euler product and zeta function enter, consistent with the ledger grounding step prior to the RCL-weighted analysis. The downstream logicData_of_boundaryTransport and rsPhysicalThesisData_of_boundaryTransport both invoke it to recover the prime ledger without extra assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.