one_not_primeLedgerAtom
plain-language theorem explainer
The theorem shows that 1 fails the prime ledger atom property in the multiplicative positive-integer ledger. Researchers grounding the arithmetic side of the Recognition Science Riemann hypothesis bridge cite it to exclude the unit from the set of irreducible postings. The proof is a term-mode wrapper that assumes the atom hypothesis for 1 and applies the classical non-primality of 1 to its embedded prime component.
Claim. The natural number 1 does not satisfy the prime ledger atom property, i.e., it is not the case that 1 is a natural prime whose every factorization into positive integers forces one factor to be 1.
background
The module supplies the classical foundation for the multiplicative ledger in which positive integers act as states and primes function as irreducible postings. A prime ledger atom on a natural number p requires both that p is prime in the naturals and that p = a b implies a = 1 or b = 1 for any positive integers a and b. This setup precedes any Recognition Science weighting of primes into the Euler ledger; the module doc states that the RS contributions begin only after this identification is complete.
proof idea
The term proof introduces a hypothesis h asserting that 1 is a prime ledger atom, then applies the upstream lemma that 1 is not a natural prime directly to the prime field of h.
why it matters
The result supplies the exclusion-of-one clause inside the prime ledger certificate definition, which bundles the atom-prime equivalence, the exclusion of 1, and the positivity of primes. It completes the classical alignment of ledger atoms with standard primes before the Euler product or any Recognition Science forcing chain is invoked. The module doc emphasizes that this classical layer is required before the RH bridge work begins.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.