coprime_threehundredsixty_thirtyseven
plain-language theorem explainer
360 and 37 share no common prime factors. Researchers applying arithmetic functions such as the Möbius function within Recognition Science number theory cite this coprimality when handling specific constants. The verification proceeds by direct computation via a native decision procedure.
Claim. $ gcd(360, 37) = 1 $
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Local conventions treat these as footholds for later Dirichlet inversion and related algebra. The declaration depends on the upstream result that supplies an explicit log-derivative bound M, yielding the angular Lipschitz constant logDerivBound = M * r on the circle of radius r.
proof idea
One-line wrapper that applies native_decide to confirm the gcd equals 1.
why it matters
The result supplies a basic coprimality fact inside the arithmetic-functions module. It supports potential applications of the Möbius function to constants appearing in the Recognition framework, such as those tied to the phi-ladder or the alpha band near 137. No downstream theorems currently invoke it, leaving its precise placement in the T0-T8 forcing chain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.