pith. sign in

arxiv: 2606.21738 · v1 · pith:THAI5MELnew · submitted 2026-06-19 · 🧮 math.LO

Pointwise Mean Value Theorems in Constructive Mathematics

Jananan Arulseelan , James E. Hanson This is my paper

Pith reviewed 2026-06-26 12:27 UTC · model grok-4.3

classification 🧮 math.LO
keywords constructive mathematicsmean value theoremlaw of bounded changeconstancy principlelocatorstopos modelscountable choice
0
0 comments X

The pith

The natural approximate versions of the mean value theorem fail to hold in neutral constructive mathematics.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper demonstrates that approximate forms of the Mean Value Theorem, Law of Bounded Change, and Constancy Principle do not hold in neutral constructive mathematics, unlike the approximate Intermediate Value Theorem which does hold. The failure is established by appealing to a model in which the reals are in bijection with the naturals. Under the addition of countable choice or suitable locator conditions on functions, the approximate statements are recovered. An even weaker approximate version of the Mean Value Theorem is shown to hold without extra assumptions.

Core claim

In neutral constructive mathematics the natural approximate Mean Value Theorem, Law of Bounded Change and Constancy Principle all fail, as shown by the existence of a topos in which the reals are bijective with the naturals; the same statements hold once functions are equipped with locators or once countable choice is assumed, while a strictly weaker approximate Mean Value Theorem holds unconditionally.

What carries the argument

Booij's locators, which supply constructive information sufficient to recover the approximate theorems from the neutral setting.

If this is right

  • The Law of Bounded Change fails in its natural approximate form without countable choice.
  • The Constancy Principle fails in its natural approximate form without countable choice.
  • A weaker approximate Mean Value Theorem holds in neutral constructive mathematics.
  • The approximate statements become provable once functions carry locators.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The results separate pointwise derivative conditions from their integral consequences more sharply than in classical analysis.
  • Constructive proofs of change-of-variable or fundamental-theorem statements may need to track locator data explicitly.
  • The contrast with the approximate Intermediate Value Theorem indicates that different classical theorems have different constructive thresholds.

Load-bearing premise

There exists a topos in which the real numbers are in bijection with the natural numbers.

What would settle it

An explicit real-valued function on a closed interval together with a constructive proof that it satisfies the approximate mean value statement in every model of neutral constructive mathematics would falsify the failure claim.

Figures

Figures reproduced from arXiv: 2606.21738 by James E. Hanson, Jananan Arulseelan.

Figure 1
Figure 1. Figure 1: The construction from the proof of Proposition 3.1. c ′ and d ′ are found first using the constructive approximate IVT. Then c and d are found in the same way. Choosing c ′ and d ′ first ensures a minimum distance of d ′ − c ′ between c and d. Proof. Let e0 = a and eN = b. Fix rational e1 < e2 < · · · < eN−1 in (a, b) satisfying that for each n < N − 1, |en+1 − en| = |en+2 − en+1| < 1 2 δ. Let r be the fix… view at source ↗
read the original abstract

We answer some questions regarding the mean value theorem and related results in constructive mathematics. The answers to these questions reveal interesting properties of the Mean Value Theorem, Law of Bounded Change, and Constancy Principle. We see that, in contrast to the Intermediate Value Theorem whose approximate analogue was shown to hold constructively by Frank, the natural approximate versions of these theorems fail to hold in neutral constructive mathematics. Our proof of this makes use of the existence of a topos in which the real numbers are in bijection with the naturals, which was shown by Bauer and the second author. Using Booij's notion of locators, we show that the aforementioned approximate analogues do hold in the presence of a small amount of countable choice, and also under suitable locator lifting hypotheses. We also show that an even weaker approximate analogue of the Mean Value Theorem holds in neutral constructive mathematics.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 0 minor

Summary. The paper claims that the natural approximate versions of the Mean Value Theorem, Law of Bounded Change, and Constancy Principle fail to hold in neutral constructive mathematics, as shown by counterexamples in the Bauer-Hanson topos (where the reals are in bijection with the naturals). It establishes that these statements become provable under countable choice or suitable locator-lifting hypotheses (using Booij's notion of locators), and that an even weaker approximate analogue of the Mean Value Theorem holds in neutral constructive mathematics.

Significance. If the results hold, the work delineates precise boundaries between neutral constructive mathematics and its extensions by choice or locators, using a standard model-theoretic method to establish non-provability. The concrete use of the Bauer-Hanson topos and the positive results with locators provide falsifiable distinctions and strengthen the literature on constructive analysis.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary, significance assessment, and recommendation to accept the manuscript. No major comments were raised that require point-by-point response.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper proves non-provability of the approximate MVT, Law of Bounded Change, and Constancy Principle in neutral constructive mathematics by citing the prior construction of the Bauer-Hanson topos (Bauer and co-author Hanson) and verifying failure of the statements inside that model. This is a standard external model-theoretic argument for independence; the cited existence result is a separate mathematical construction, not derived within the present paper. The paper's additional positive results (provability under countable choice or locator-lifting hypotheses, plus a weaker approximate MVT that holds neutrally) are developed independently using Booij's locator notion and do not reduce to the cited model by definition or fitting. No self-definitional equations, fitted inputs renamed as predictions, ansatzes smuggled via citation, or renaming of known results appear. The self-citation is load-bearing only for the model existence, which is externally verifiable and does not collapse the derivation chain.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Abstract-only review; the central negative result depends on an external topos model whose internal axioms are not re-derived here.

axioms (1)
  • domain assumption Existence of a topos in which the real numbers are in bijection with the naturals (Bauer-Hanson construction)
    Used to exhibit the failure of the approximate statements in neutral constructive mathematics.

pith-pipeline@v0.9.1-grok · 5672 in / 1125 out tokens · 28647 ms · 2026-06-26T12:27:53.546067+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

10 extracted references · 1 canonical work pages

  1. [1]

    Hanson , title =

    Andrej Bauer and James E. Hanson , title =. 2024 , note =

    2024

  2. [2]

    Booij , title =

    Auke B. Booij , title =. Mathematical Structures in Computer Science , volume =

  3. [3]

    Schuster , title =

    Douglas Bridges and Fred Richman and Peter M. Schuster , title =. Proceedings of the American Mathematical Society , volume =. 2000 , doi =

    2000

  4. [4]

    Indagationes Mathematicae , volume =

    Douglas Bridges and Dirk van Dalen and Hajime Ishihara , title =. Indagationes Mathematicae , volume =

  5. [5]

    Logical Methods in Computer Science , volume =

    Morgan Frank , title =. Logical Methods in Computer Science , volume =

  6. [6]

    Hardin and Daniel J

    Christopher S. Hardin and Daniel J. Velleman , title =. Journal of Symbolic Logic , volume =. 2001 , doi =

    2001

  7. [7]

    Journal of Symbolic Logic , volume =

    Hajime Ishihara , title =. Journal of Symbolic Logic , volume =. 1991 , doi =

    1991

  8. [8]

    Schuster , title =

    Peter M. Schuster , title =. Theoretical Computer Science , volume =. 2003 , doi =

    2003

  9. [9]

    A constructive proof of Simpson’s Rule , ISSN =

    Coquand, Thierry and Spitters, Bas , year =. A constructive proof of Simpson’s Rule , ISSN =. doi:10.4115/jla.2012.4.15 , journal =

    work page doi:10.4115/jla.2012.4.15 2012

  10. [10]

    and Bridges, Douglas S

    Bishop, E. and Bridges, Douglas S. Constructive Analysis