primes_are_irreducible
plain-language theorem explainer
Natural numbers act as transactions on the RS multiplicative ledger, with primes as its irreducible elements that resist decomposition into smaller factors. Ledger formalizers and number theorists in the RS setting cite this to secure atomicity before invoking unique factorization. The tactic proof applies the divisibility property of primes to the product equation, performs case split on the divisor, and cancels to force one factor to unity.
Claim. Let $p$ be a prime natural number. Then for all natural numbers $a,b$, if $a b = p$ then $a=1$ or $b=1$.
background
Recognition Science treats reality as a discrete multiplicative ledger in which every natural number counts as a transaction. Primes are defined via the standard predicate as the irreducible transactions that cannot factor nontrivially, matching the module statement that primes are the atomic ledger entries whose existence forces the fundamental theorem of arithmetic to serve as the ledger balance sheet. The local setting also records the proved d'Alembert zero-line theorem, the definitional J-to-zeta model, and the open hypothesis that ledger conservation predicts the Riemann Hypothesis via Euler-product constraints.
proof idea
The tactic proof introduces the factors a and b under the product hypothesis. It invokes the standard lemma that a prime dividing a product must divide one factor, here instantiated with the product equal to p itself. Case analysis on the resulting disjunction yields either a equals 1 or a equals p; the second case substitutes into the product equation, obtains a b equals a times 1, and cancels the positive a to conclude b equals 1.
why it matters
The declaration supplies the irreducibility step required for the module's ledger interpretation of the fundamental theorem of arithmetic. It thereby underpins the structural parallel between J-cost symmetry and the zeta functional equation, and it closes the basic number-theoretic prerequisite for the open question whether the Euler product imposes d'Alembert-type constraints on the completed zeta function. No downstream uses are recorded, so the result functions as a foundational ledger axiom rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.