Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help


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.