semiprime_twentysix
plain-language theorem explainer
26 equals 2 times 13 and therefore has exactly two prime factors counted with multiplicity. Researchers using arithmetic functions to track semiprimes in the Recognition Science number theory layer would cite this verification. The proof reduces immediately to a native decision procedure that computes bigOmega 26 and checks equality to 2.
Claim. $26$ is semiprime, i.e., the total number of prime factors of $26$ counted with multiplicity equals $2$.
background
The module supplies lightweight wrappers for arithmetic functions from Mathlib, beginning with the Möbius function. The predicate isSemiprime is defined by bigOmega n = 2, where bigOmega counts the total number of prime factors with multiplicity. This instance confirms the property for n=26 directly from the definition. Upstream results include the definition of isSemiprime together with general interface structures from foundation modules that supply collision-free and ledger primitives.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the Boolean expression isSemiprime 26.
why it matters
This theorem supplies a concrete verified instance of the semiprime predicate within the arithmetic functions module. It supports the broader development of number-theoretic tools that may feed into Recognition Science constructions involving prime factorizations, such as those appearing in the phi-ladder or Möbius inversion steps. No downstream uses are recorded yet, leaving it as a foundational check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.