semiprime_ninetyfive
plain-language theorem explainer
95 factors as 5 times 19 and therefore satisfies the semiprime condition that the total number of prime factors counted with multiplicity equals two. Number theorists inside the Recognition Science development would cite the result when confirming small composites against the bigOmega predicate. The proof reduces to a single native decision procedure that evaluates the definition directly.
Claim. $95 = 5 × 19$ satisfies the semiprime condition, i.e., the sum of exponents in its prime factorization equals exactly two.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. A number n is semiprime precisely when bigOmega n equals 2, where bigOmega counts the total number of prime factors with multiplicity; the isSemiprime predicate encodes this Boolean test directly. Upstream structural definitions from nucleosynthesis tiers, ledger factorization, phi-forcing, spectral emergence, and physics complexity supply the Recognition Science setting in which these arithmetic checks occur.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the isSemiprime predicate on 95.
why it matters
The result supplies a concrete instance of the semiprime predicate used in the arithmetic functions library. It supports constructions that rely on prime factorizations within the Recognition framework, although no immediate parent theorem appears among the used-by edges. It aligns with the development of number-theoretic footholds for Möbius inversion and related tools.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.