six_almost_prime_threehundredsixty
plain-language theorem explainer
The declaration verifies that 360 has total prime factor count six, confirming it as a 6-almost prime relevant to superperiod modeling. Number theorists using Recognition Science arithmetic functions would cite this for explicit period checks. The proof is a one-line native_decide evaluation on the bigOmega definition.
Claim. $Ω(360) = 6$, where $Ω(n)$ counts the prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function and extending to predicates such as isSixAlmostPrime. This predicate is defined as bigOmega n = 6, where bigOmega is the standard total prime factor counting function. The local setting is a collection of small interfaces for Dirichlet algebra that remain lightweight until deeper inversion results stabilize.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic. This evaluates the definition isSixAlmostPrime 360 directly by computing bigOmega 360 on the factorization 2³ × 3² × 5.
why it matters
The result supplies a concrete numerical check for the 6-almost prime property on 360, identified in the module as the main superperiod. It supports downstream arithmetic work on the phi-ladder and eight-tick structures even though the declaration has no recorded uses yet. The verification closes a specific instance in the arithmetic functions layer without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.