A 2-adic constraint on the separable baseline.
ProvedHalfPlane.four_pow_omega_dvd_circleCountaether-catalogmachinelearning
A 2-adic constraint on the separable baseline. For odd squarefree N,
4^ω(N) divides C(N): every local factor p - χ_p(-1) is divisible by 4,
since p ≡ 1 (mod 4) gives 4 ∣ p - 1 and p ≡ 3 (mod 4) gives 4 ∣ p + 1.
theorem HalfPlane.four_pow_omega_dvd_circleCount{N : ℕ} (hodd : ¬ 2 ∣ N) (hsq : Squarefree N) :
4 ^ N.primeFactors.card ∣ circleCount N := by sorry
Formalization Note Transplanted verbatim from the Aether Catalog source MachineLearning/HalfPlaneClosedForm.lean; the statement is byte-identical to the source declaration, elaborated with autoImplicit disabled in the platform environment.
Preamble
-- Thm stub generated from MachineLearning/HalfPlaneClosedForm.lean
import Mathlib
import Definitions.Def_MachineLearning_HalfPlaneCircleBasic
import Definitions.Def_MachineLearning_HalfPlaneClosedForm
import Definitions.Def_MachineLearning_HalfPlaneSemiprime
/-!
# Cycle 4: the separable baseline in closed form
The circle count is an arithmetic function in the technical sense, and it is
multiplicative. Combined with the odd-prime conic count this gives a closed
product formula for every odd squarefree modulus:
`C(N) = ∏_{p ∣ N} (p - χ_p(-1))`.
This is the exact "free-witness / CRT-separable" baseline: `C` is computable from the
factorisation of `N` in `O(ω(N))` arithmetic operations, while the non-separable
half-plane count `H` studied in the other files admits no such product formula
(`halfPlaneCount_not_multiplicative`).
-/
open HalfPlane
open FinsetFormal statement
theorem HalfPlane.four_pow_omega_dvd_circleCount{N : ℕ} (hodd : ¬ 2 ∣ N) (hsq : Squarefree N) :
4 ^ N.primeFactors.card ∣ circleCount N := by sorrySource