PrimeLedgerLogicCert
plain-language theorem explainer
The PrimeLedgerLogicCert structure packages four axioms certifying that prime ledger atoms on LogicNat match classical primes under the toNat recovery map, with positivity and transport conditions. Number theorists bridging the Recognition logic foundation to analytic number theory cite it to justify moving primality statements into the Euler product and zeta machinery. The declaration is a pure structure definition that bundles the transport and positivity conditions with no proof obligations.
Claim. A structure $C$ with four fields: (1) for all $p$ in LogicNat, PrimeLedgerAtomLogic$(p)$ holds if and only if toNat$(p)$ is a classical prime; (2) PrimeLedgerAtomLogic does not hold for fromNat$(1)$; (3) every classical prime recovered from a LogicNat element satisfies IntegerLedgerStateLogic; (4) PrimeLedgerAtomLogic$(p)$ is equivalent to the classical PrimeLedgerAtom applied to toNat$(p)$. Here PrimeLedgerAtomLogic$(p)$ is defined as PrimeLedgerAtom(toNat$(p))$ and IntegerLedgerStateLogic$(n)$ asserts $0 < n$.
background
LogicNat is the inductive type of natural numbers forced by the Law of Logic, with constructors identity (representing the zero-cost element) and step (one iteration of the generator). The maps toNat and fromNat supply the equivalence between this logic-native representation and classical Nat. PrimeLedgerAtomLogic$(p)$ is defined by applying the classical PrimeLedgerAtom to toNat$(p)$, while IntegerLedgerStateLogic$(n)$ asserts positivity via $0 < n$ on the recovered integer.
proof idea
The declaration is a structure definition that directly enumerates its four fields: the iff between logic and classical primality, the exclusion of 1, the positivity implication, and the transport equivalence to the classical PrimeLedgerAtom. No tactics or lemmas are applied inside the declaration itself; the fields are populated downstream by explicit proofs such as primeLedgerAtomLogic_iff_prime and one_not_primeLedgerAtomLogic.
why it matters
This certificate enables the recovered prime ledger to support the Euler product for the zeta function, as required by recovered_prime_ledger_supports_euler_product. It appears as the primeLedgerLogic field in RSPhysicalThesisDataLogic, supplying the recovered-prime component for the RH decomposition data. The structure closes the transport between logic-native arithmetic (from the Law of Logic) and the classical prime ledger, allowing the Recognition framework to interface with analytic number theory without altering the Mathlib zeta machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.