six_almost_prime_threehundredfiftytwo
plain-language theorem explainer
352 factors as 2^5 times 11 and therefore meets the definition of a 6-almost prime. Number theorists referencing Recognition Science arithmetic checks would cite this result. The proof evaluates the predicate through native decision.
Claim. The integer 352, which admits the prime factorization $2^5 times 11$, is a 6-almost prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to predicates such as isSixAlmostPrime. The predicate isSixAlmostPrime n holds when n has exactly six prime factors counted with multiplicity. The local setting keeps statements minimal before layering Dirichlet algebra. Upstream dependencies include audit entry points and structure definitions that enforce framework consistency without introducing new axioms.
proof idea
The proof is a one-line wrapper that invokes native_decide to reduce the boolean equality to direct computation.
why it matters
This verification supplies a concrete instance supporting Recognition Science number-theoretic checks, particularly those tied to the factor 11. It feeds into broader audit and mechanism-design components listed among the dependencies. No open questions are discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.