MathAudit

Paper metadata

Original submission
October 19, 2026
Claimed MSC
11J82, 11J89
arXiv categories
math.NT
Comments
33 pages. Lean 4 proof sources and reproduction instructions included as ancillary files

Abstract

Let Ω=2∫01(1−t4)−1/2dtΩ=2\int_0^1(1-t^4)^{-1/2}dt. We prove that, for every real ν>2ν>2, there is Q≥2Q\geq2 such that q−ν<∣Ω−p/q∣q^{-ν}<|Ω-p/q| for every integer pp and every integer q≥Qq\geq Q. Consequently ΩΩ is irrational and its irrationality exponent is two. The proof combines elliptic separated-weight interpolation, arithmetic denominator estimates, and an analytic determinant bound on a square complex-multiplication grid. The determinant comparison uses the same selected source columns on both sides. We give the integral-to-lattice normalization, the exact local-coordinate and common-multiplier transport, and the parameter order that makes the two bounds incompatible. The accompanying Lean 4 development proves the endpoint without additional hypotheses. Numbered formal references link the mathematical argument to exact declarations in the complete source distribution; an appendix gives the pinned build environment and the dependency audit.

AI-generated audit

Audit summary

Audited against arXiv v1

Not a correctness certificate. A green “no issues found” result may include yellow suspected typos or minor formal issues that do not affect substantive soundness. It means this audit found no unresolved substantive error under the stated criteria; it does not replace expert scrutiny or formal verification.

Current report

Detailed mathematical audit

Generated October 23, 2026
01Statements4 reported findingsNo statement issues found

The eventual rational-approximation lower bound, irrationality of the integral-defined lemniscate period, and irrationality exponent two are supported. The elliptic interpolation, arithmetic-minor, and same-minor analytic estimates used to obtain the endpoint are stated with compatible hypotheses and quantifier order.

Theorem 1.1 and Corollary 6.3No issue found

The all-denominator approximation bound is supported

PDF pp. 3 and 22–24 · Theorem 1.1, Theorem 6.2, and Corollary 6.3 · arXiv:2610.26539v1

For each real exponent greater than two, the parameter construction first fixes a square-grid dimension with strict arithmetic and collision margins, then selects the rational approximations in the order required by the successive interpolation thresholds. Cofinal nonzero minors satisfy the arithmetic lower bound and the analytic upper bound for the same selected columns. Both possible branches of the analytic maximum are then strictly below the lower bound, excluding unbounded denominators and giving the claimed eventual strict inequality.

Theorem 3.1 and Proposition 3.2No issue found

Separated-weight interpolation is available in the required uniform form

PDF pp. 8–13 · Section 3 · arXiv:2610.26539v1

The successive weight separation is chosen before the centers, while only the final size threshold depends on them. Excess curve contact produces one nonzero auxiliary polynomial with persistent derivative vanishing. The upper and rectangular lower multiplicity estimates apply to the same localized prime and the same local length; the resulting normal-product comparison rules out every forbidden normal-basis change. Differential rigidity forces the elliptic projection to be constant, and the remaining additive fiber satisfies the already established ordinary curve inequality. The curve-degree identities and uniform positive margin then prove ampleness and eventual packet surjectivity on the stated divisibility progression.

Theorem 4.2 and Proposition 5.4No issue found

The lower and upper estimates concern the identical arithmetic determinant

PDF pp. 13–21 · Sections 4–5 · arXiv:2610.26539v1

Denominator clearing uses only the additive logarithm coefficients and the selected source degrees, yielding a nonzero Gaussian-integer lower bound without an extra elliptic denominator. The analytic side first applies an exact determinant-one jet-coordinate change and then multiplies every selected column by the same explicit entire theta factor. Its nonzero constant coefficient gives the displayed determinant product, so the selected columns are unchanged. The finite displacement expansion and collision estimate then supply the claimed normalized upper bound with a remainder tending to zero.

Theorem 6.4No issue found

The conventional irrationality exponent conclusion follows

PDF p. 24 · Theorem 6.4 · arXiv:2610.26539v1

The eventual lower bound first excludes rationality by applying it to arbitrarily large exact representations of a hypothetical rational value. Dirichlet approximation then places exponent two in the reduced-rational approximation set, while the all-denominator bound makes every larger exponent admit only finitely many reduced rationals. These two facts determine the supremum to be exactly two.

02Proofs4 reported findingsNo proof issues found

The manuscript's central determinant argument is complete when read together with its supplied formal source. The deepest geometric steps are implemented as concrete theorem chains rather than retained assumptions, and the final endpoint has no mathematical hypotheses or project-specific axioms.

Section 2No issue found in the reviewed proof

The integral, lattice, and local-germ normalizations agree

PDF pp. 4–8 · Section 2 · arXiv:2610.26539v1

The square lattice is first rescaled to invariants g2=4g_2=4 and g3=0g_3=0 without using the target integral. The real branch, its half-period integral, and the positivity argument identify that scale with the period defined in the paper. Evaluation at the diagonal half-period gives the cubic point used by the determinant, and the logarithmic reparameterization has the required nonzero linear coefficient and exact formal substitutions.

Proposition 3.2 source chainNo issue found in the reviewed proof

The normal-basis rigidity and persistence obligations are discharged

PDF pp. 10–12 and ancillary Lean modules LemniscatePrimeUpper, LemniscatePrimeLower, LemniscateNormalComparison, LemniscatePersistentProjection, LemniscateDifferentialRigidity, LemniscateCurveRigidity, and LemniscateCurveInequality · arXiv:2610.26539v1

The source constructs persistent prime components from the actual derivative ideals retaining the cubic equation. The upper estimate charges the cubic source degree once, while the lower estimate is derived from the concrete local Taylor map in independent frame-normal directions. Their product comparison feeds a proved normal-basis exclusion theorem. The remaining rigidity step is reduced to non-exactness of the elliptic invariant differential on finite function-field extensions and is proved by the twisted-trace rational differential equation described in the manuscript. No interpolation or rigidity assertion is reintroduced as a premise of the final curve inequality.

Proposition 3.3 source chainNo issue found in the reviewed proof

Curve inequalities pass to ampleness and jet surjectivity without a missing geometric hypothesis

PDF pp. 12–13 and ancillary Lean modules LemniscateCurveModel, LemniscateCurveHyperplaneDegree, LemniscateCurveExceptionalDegree, LemniscateBlowupAmple, and LemniscateGlobalInterpolationTheorem · arXiv:2610.26539v1

For each noncontracted curve meeting the affine chart, the construction uses that curve's own normalized function field and proves the hyperplane and exceptional degree formulas. Contracted curves and curves outside the chart are treated separately. A single positive numerical margin therefore holds for every integral curve; the numerical ampleness theorem makes the fixed interpolation bundle ample, and the Rees/cohomology restriction theorem yields eventual surjectivity of the literal packet map. The auxiliary ample exponent does not enter the target bundle or change the center-independent divisibility radius.

Formal endpoint and publication snapshotNo issue found in the reviewed proof

The supplied source evidence is internally consistent

PDF pp. 25–26 · Appendix A and ancillary source snapshot · arXiv:2610.26539v1

The final declaration states the irrationality exponent of the paper's interval-integral definition with no hypotheses. The archived source contains the full local import closure: all 989 manifest entries match their declared SHA-256 hashes, including 975 mathematical modules. The recorded verification covers 316 declarations; every reported dependency is one of propositional extensionality, classical choice, or quotient soundness, and the build logs end with successful endpoint and completion targets. The theorem types inspected along the critical chain agree with the manuscript's period, curve, determinant, and approximation claims.

03Novelty0 reported findingsNo novelty concerns found

No non-novelty findings.

Detailed audit reportFull reasoning, manuscript locations, and references.
Open report PDF ↗

Author response

Challenge an audit finding

Local workflow preview

A listed author may submit formal evidence that an audit is inaccurate. The response would be considered in a fresh AI re-evaluation; it would not edit the audit automatically.

Paper
arXiv:2610.26539v1
Authors listed
Gregory V. Chudnovsky
Audit date
October 23, 2026
  1. 01Establish identityMatch an authenticated scholarly identity to this paper.
  2. 02Submit evidenceIdentify the finding and give a formal mathematical response.
  3. 03Re-evaluateA separate agent checks the response and records a disposition.
Recommended production method

Authenticate with ORCID, then require an exact arXiv match

MathAudit should accept the identity only when ORCID OAuth authenticates the claimant's iD and this exact arXiv paper appears in arXiv's public authority feed for that iD. A matching name alone is not sufficient.

ORCID OAuth and arXiv authority-record lookup are not connected in this local prototype.

Email fallback for papers without a linked ORCID

A production fallback could send a one-time link only when the submitted address matches an independently maintained author-contact allowlist for this paper. MathAudit must return the same message for every address so the form cannot reveal which contacts are on that list.

This demonstration does not send, store, or compare the address.

Structured response preview

This form remains unavailable until production identity verification succeeds. Nothing entered here is submitted.

This panel never establishes authorship in the local prototype. A production result should be described narrowly as an authenticated ORCID match or control of a separately allowlisted author-contact mailbox.