semiprime_thirtyfive
plain-language theorem explainer
The declaration verifies that 35 satisfies the semiprime condition Ω(n) = 2. Number theorists extending arithmetic function interfaces in Recognition Science would reference this as a concrete base case. The proof reduces to a single native decision call that evaluates the bigOmega predicate directly.
Claim. $35$ is semiprime, i.e., the total number of prime factors of $35$ counted with multiplicity equals $2$.
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. Upstream results include the isSemiprime definition itself together with foundational structural guarantees from OptionAEmpiricalProgram, SimplicialLedger, MechanismDesignFromSigma, and RamanujanBridge modules.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the Boolean expression isSemiprime 35.
why it matters
This supplies a verified base instance inside the arithmetic functions module that supports prime classification tools. It sits downstream of the isSemiprime definition and contributes to the number-theoretic scaffolding that may later interface with mass formulas on the phi-ladder, though no direct tie to the T0-T8 forcing chain appears here. No downstream theorems yet cite it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.