bibkey: hohn2025a390148 authors: Charles L. Hohn year: 2025 title: A390148 — primitive radii of four mutually tangent spheres and a plane doi: null url: https://oeis.org/A390148 claim: The entry conjectures that exactly three radii have the same positive 3-adic order. strata_touched:

• D5/S3/Arith/Descartes/PrimitiveSphereRadii license: citation-only triage: anchor

The 3-adic clause of A390148

Verified locator

url: https://oeis.org/A390148

doi: null

Revision 23 of https://oeis.org/A390148/internal, dated 2025-11-17, introduces its claims as observed for 1000 rows and conjectured for infinitely many rows. It supplies no proof of the 3-adic clause. The displayed equation has coefficient 3 and describes four spheres together with a plane.

Statement and proof

Let r be four positive natural radii with common gcd 1. Suppose the square of the sum of their reciprocals equals three times the sum of the squares of their reciprocals, over the rational numbers. There is a positive integer e such that three of the radii have 3-adic order e and the fourth has order zero. No ordering of the radii is needed.

Set L to the least common multiple of the radii and b_i=L/r_i. These integer curvatures have gcd 1: a common divisor d would make L/d a common multiple of all radii, which contradicts minimality unless d=1. Clearing denominators gives (sum b_i)^2=3 sum b_i^2. First 3 divides the sum; then 3 divides the sum of squares. Each nonzero square modulo 3 is 1, so the number of nonzero residues is a positive multiple of 3 at most 4. It is therefore 3. The identity v3(b_i)+v3(r_i)=v3(L) transfers this count to the largest radius valuation. The common gcd of the radii forces the one remaining valuation to be zero.

Proof scope

Mathlib supplies the gcd/lcm divisibility API, rational cast of exact natural division, prime divisibility of a square, the finite-field power identity, and the product valuation formula; these are reused directly.

The implementation addresses only the 3-adic clause. The other prime conditions, repetition formula and chains are separate conjectures. A390583 is the coefficient-2 circle problem and is not used here. No publication priority or exhaustive literature coverage is claimed.