has_prime_factor
plain-language theorem explainer
Every natural number greater than 1 has at least one prime factor. In the Recognition Science ledger this asserts that no multiplicative transaction can avoid irreducible entries. The result is cited when building the balance sheet property that leads to unique factorization. The proof is a one-line wrapper applying the standard existence lemma for prime divisors after the inequality is discharged by arithmetic simplification.
Claim. For every natural number $n > 1$ there exists a prime $p$ such that $p$ divides $n$.
background
The module treats natural numbers as transactions on a discrete multiplicative ledger. Primes function as the irreducible entries that cannot be decomposed further. The d'Alembert identity (RCL) then relates the J-cost of a composite transaction to the costs of its prime factors. Upstream definitions supply the cost function on recognition events and the multiplicative recognizer that induces J-cost on positive ratios.
proof idea
The proof is a one-line wrapper that applies Nat.exists_prime_and_dvd to the hypothesis 1 < n. The inequality is discharged by the omega tactic inside the application.
why it matters
The declaration supplies the existence half of the ledger's balance sheet and feeds the module's development of primes as irreducible transactions. It supports the structural parallel between J-cost symmetry and the zeta functional equation while leaving open the question whether the Euler product imposes d'Alembert-type constraints on the completed zeta function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.