slug: calderon-2026-quadratic-order-reciprocal-moments bibkey: calderon2026rectangular doi: 10.48550/arXiv.2608.00347 url: https://arxiv.org/abs/2608.00347v1 triage: theorem motivation_gids:
- D5/S3/Arith/Congruence/QuadraticOrderMoments/CalderonReciprocalMoments.result
Calderon’s reciprocal moments in imaginary quadratic orders
Problem
Kevin Calderon, Ljunggren–Jacobsthal and Bailey-Type Congruences for Rectangular Gaussian Binomial Coefficients, arXiv:2608.00347v1, Conjecture 6.3, PDF page 19:
Let satisfy (6.1), and let satisfy (6.3). Then, for every , , .
Equation (6.1) is , with and . Equation (6.3) requires a rational prime , , and . The local order is . Its positive representatives are
The coordinate condition excludes simultaneous divisibility by ; both
intervals include . The Lean ring R is the adjoin-root of
over PadicInt p, and U is the finite image of exactly this filtered
positive rectangle. All its elements are units in the admissible setting.
Consequently Ring.inverse in H1 and H2 is the underlying inverse unit
value, without adding an assumption or a term to the source’s sums.
The fully quantified statement is: for every natural prime , every pair
of integers satisfying all four admissibility clauses, and every
natural , both displayed memberships hold. The public claim
encodes this statement; result : claim has no additional hypotheses.
Motivation
Issue #13205 preregisters this external, first-tier named conjecture. It asks whether the extra power of in the first moment is uniform in the quadratic order and its chosen basis. The conclusion supplies the local reciprocal-moment premise used in the source’s proposed omega-Ljunggren extension of Gaussian rectangular congruences.
Gap
The cited v1 states the assertion as Conjecture 6.3. The preregistration records no proof in its searched Semantic Scholar, OpenAlex, MathDB and formal-conjectures surfaces; those external search readings are producer reported. They do not exclude every unpublished or unindexed proof. The full target is not a named theorem in the searched pinned Mathlib Padics, QuadraticAlgebra, finite-field and finite-sum scope. Existing universal lifts, unit norms, residue maps and sum permutations are reused. The settlement asserts the stated theorem, without claiming exhaustive historical priority.
Route
Write . Positive coordinates identify the finite grid bijectively with the units of the quadratic ring modulo . Multiplication by permutes those units. The resulting relation modulo , and cancellation of the unit , give . The same calculation puts the scalar inverse-square sum in .
Reflect each coordinate to , keeping fixed. The exact affine identity is , where . The inverse identity modulo gives , with . The two boundary-strip sums satisfy and modulo . Thus ; cancellation of the unit gives . Principal divisibility is exactly membership in the singleton-generated ideals appearing in the public statement.
proof_shape: result: bind-only
escape_witness: none
admission_basis: open-problem-resolution (#13205; Proved)
The computational-content classification is utility: none: this is a
symbolic theorem for arbitrary admissible parameters, rather than bounded
enumeration, a checker, numerical reduction or a certified finite instance.
Information-escape registration is paused under CLAUDE.md §3.9.
Falsifier
An admissible with either or
falsifies the conjecture. A mismatch between the literal
finite image U and the unit grid, failure of the affine reflection at an
endpoint, or failure of either boundary congruence invalidates the stated
route. Finite agreement alone does not prove the universal claim.
Evidence
The theorem is CalderonReciprocalMoments.result in
D5/S3/Arith/Congruence/QuadraticOrderMoments/CalderonReciprocalMoments.lean.
Its public surface consists of R, element, Admissible, U, H1, H2,
claim, and this one theorem. The axiom closure of every public declaration
is contained in {propext, Classical.choice, Quot.sound}.
The producer reports a compiled exact check inhabiting the assumptions
at and inhabiting R by zero; its command and exit code
are not independently verified here. No sorry, private axiom or
native_decide is used.
The Scribe result carries a ResolutionKind.Proved claim for this dossier.
The source formulas and the interpretation of their positive endpoints
are recorded in Library/QuadraticForms/calderon2026rectangular.md.
Triage
theorem; resolution Proved for Conjecture 6.3, for all its parameters.
What the settlement shows
- Proved in this module: the two moment bounds, simultaneously and
uniformly in the chosen imaginary quadratic order and basis, by
D5/S3/Arith/Congruence/QuadraticOrderMoments/CalderonReciprocalMoments.result. The decisive mechanism is the combination of the doubling permutation with the affine reflection and its two endpoint strips. - Computed, probe-reported: exact arithmetic checks cover 730 distinct
admissible cases, with , , , ,
and for . The generating commands are
/tmp/op-calderon/checks 2 31,/tmp/op-calderon/checks 3 13, and/tmp/op-calderon/checks 3 19 17 3; the union removes repeated cases. These readings are not premises of the kernel proof. - Open: weakening the admissibility conditions, changing the representative rectangle, higher reciprocal powers, and sharpness of the two valuations. The delivered theorem asserts no relaxed version.
- Open: Conjecture 6.4, the omega-Ljunggren analogue. Its stated hypotheses are those of Conjecture 6.3, with , and . The preceding derivation assumes and ; Conjecture 6.3 discharges these moment bounds. The translated-block and Newton-identity conclusion remains open.
- Open: Conjecture 6.5, the omega-Bailey analogue, under its stated inert-prime condition (6.3), and . The source gives Frobenius strip factorizations without a Conjecture 6.3 reciprocal-moment premise, so Conjecture 6.3 discharges no such premise here. The resulting congruence remains open.
ASSUMED-UNVERIFIED
The external literature-search counts, finite numerical checks and compiled exact check above are producer-reported. Exhaustive absence of an earlier proof and historical priority are not verified. Sharpness, relaxed hypotheses and the source’s remaining conjectures are open; this settlement does not prove them.