semiprime_fourteen
plain-language theorem explainer
Fourteen factors as 2 times 7 and therefore satisfies the semiprime condition that the total number of prime factors counted with multiplicity equals 2. Researchers constructing arithmetic tables for the phi-ladder and mass formulas in Recognition Science would cite this verification when classifying small integers. The proof is a one-line term that applies native_decide to evaluate the boolean definition directly on the constant 14.
Claim. The natural number 14 satisfies $14=2×7$ and therefore obeys $Ω(14)=2$, where $Ω(n)$ counts the prime factors of $n$ with multiplicity.
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, with bigOmega defined via the sum of exponents in the prime factorization. This concrete check sits among sibling results that establish basic properties of bigOmega and the Möbius function for squarefree inputs.
proof idea
The proof is a term-mode one-liner that invokes native_decide on the definition isSemiprime 14, which unfolds to bigOmega 14 = 2 and evaluates the factorization of the numeral 14.
why it matters
This verification populates the table of small semiprimes required for rung assignments on the phi-ladder and later mass formulas. It rests on the isSemiprime definition and the bigOmega arithmetic function, aligning with the number-theoretic scaffolding needed to reach constants such as alpha inverse inside the interval (137.030, 137.039). No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.