semiprime_seventyseven
plain-language theorem explainer
77 factors as 7 times 11 and therefore satisfies the semiprime condition that the total number of prime factors counted with multiplicity equals 2. Researchers enumerating small semiprimes for the Recognition Science phi-ladder mass assignments cite this result when populating the arithmetic layer. The proof is a one-line native_decide wrapper that evaluates the bigOmega definition directly at 77.
Claim. $77 = 7 · 11$ and therefore satisfies $Ω(77) = 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 μ. The predicate isSemiprime n holds precisely when bigOmega n equals 2, with bigOmega counting prime factors with multiplicity as defined in the sibling bigOmega_def. This theorem sits among similar statements for other small semiprimes that appear in the Recognition Science arithmetic scaffolding.
proof idea
The proof is a one-line native_decide wrapper that applies the definition of isSemiprime at 77 and reduces the equality to a direct computation of bigOmega 77.
why it matters
This result populates the catalog of semiprimes required by the Recognition Science mass formula on the phi-ladder. It feeds no downstream theorems in the current graph but supports the enumeration of factors that enter the yardstick scaling. The declaration closes a small computational gap in the arithmetic functions module without touching the J-uniqueness or eight-tick octave steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.