semiprime_fiftyfive
plain-language theorem explainer
The theorem confirms that 55 factors as the product of two distinct primes and therefore satisfies the semiprime predicate. Number theorists extending the arithmetic functions layer in Recognition Science would cite it when populating small-case tables for big-Omega or Möbius computations. The proof reduces to a single native_decide call that evaluates the predicate by direct computation.
Claim. $55$ is semiprime, that is, the total number of its prime factors counted with multiplicity equals two.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The predicate isSemiprime is defined by the equation bigOmega n = 2, where bigOmega counts prime factors with multiplicity. This supplies the concrete check for n = 55 = 5 × 11 inside the primes arithmetic file.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to compute and confirm bigOmega 55 = 2.
why it matters
This declaration supplies a concrete verification of the semiprime predicate for 55 inside the arithmetic functions module. It supports the development of Möbius inversion and prime factorization tools in Recognition Science, though it does not engage the forcing chain, the Recognition Composition Law, or physical constants such as the alpha band. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.