# Verification report — AMR-074-0117 (Montalbán, Question 17: the Lebesgue differentiation theorem and WWKL0)

Verification date: 2026-10-18.

**Verdict.** The note answers the question **relative to the formalisation**, which the source does not fix; every
statement it makes is proved, and the scope is as follows.
- **Answer No** under the null-cover reading (Yu; Brown–Giusto–Simpson) with the extensional measure or with the
  measure μ̄ of Nies–Triplett–Yokoyama, under the existence reading (Lebesgue points exist and are dense) and under
  the randomness reading: RCA0 proves the LDT in these readings (Theorem A, Corollary 1.1), so the ω-model REC
  separates LDT from WWKL0. The null-cover reading with the intensional measure is vacuous in models without WWKL0
  (Lemma 4.6, Remark 4.7), and the randomness reading is vacuous in REC.
- **Answer Yes** under the outer reading of Nies–Triplett–Yokoyama (every open set containing all Lebesgue points
  has measure 1), for all three measures (Theorem B); the reversal comes from the behaviour of Lebesgue measure in
  RCA0 (their Remark 6.9), not from differentiation. With the intensional measure this already holds for f = 0.
- **Judgement (not a theorem).** The null-cover reading, the convention of Yu and of Brown, Giusto and Simpson for
  almost-everywhere statements about L1 functions, fits Simpson's remark in the source; under it the answer is no.
- **Not new.** The convergence of p_n(x) outside a Martin-Löf null set in RCA0 (Yu 1994, Lemma 2.1, as reported by
  Avigad–Dean–Rute 2012; computably Pathak 2009, Lemma 3.2); the maximal-function method (Pathak 2009;
  Pathak–Rojas–Simpson 2014; Rute 2013, Theorem 4.10); the open set of the reversal and the existence-versus-
  almost-surely pattern (Nies–Triplett–Yokoyama 2021). New to our knowledge: Lemma 3.1 (finite exceptional sets),
  the cube averages and parts (a), (c) of Theorem A, and Theorem B for L1 functions; close to known techniques.

The note is unrefereed.

## Statement checked
- **Primary source.** A. Montalbán, "Open questions in reverse mathematics", Bull. Symbolic Logic 17(3) (2011)
  431–454, doi:10.2178/bsl/1309952320. Read in the author's preprint
  https://math.berkeley.edu/~antonio/papers/questionsRM.pdf (downloaded 2026-10-18, 299,540 bytes),
  Section 3.4 "Randomness and measure theory".
  - Pathak proved the LDT at Martin-Löf random reals; Simpson noticed that it follows that the LDT can be proved in
    WWKL0 and asked about the reversal.
  - LDT (paraphrase): for an L1 function f on [0,1]^d, represented as a Cauchy limit of polynomials, for almost all
    x the averages of f over the open cubes containing x converge to f(x).
  - Question 17, exactly: "Does LDT imply WWKL0?" The base theory is RCA0.
- **Corpus record** (release v1.8.0): "Over RCA0, does the Lebesgue differentiation theorem imply WWKL0?" — a
  faithful compression.
- **Not fixed by the source:** the value f(x) at a point, the measure of an open set in RCA0, the meaning of
  "for almost all x", the rate of the Cauchy sequence. The note fixes f(x) := lim p_n(x) where it exists (Pathak's
  canonical representative at random points; Brown–Giusto–Simpson, Remark 4.3) and the rate 2^(−n) (constant
  factors of other conventions do not matter), and treats every reading found in this literature.

## Readings
| Reading of "for almost every x" | Result over RCA0 | Answer | Where |
|---|---|---|---|
| (N_int) null cover, intensional measure | provable; vacuous without WWKL0 | no (degenerate) | Lemma 4.6, Remark 4.7 |
| (N_ext), (N_bar) null cover, extensional measure / μ̄ (box codes; binary codes for d = 1) | provable | no | Theorem A, Corollary 1.1 |
| (E) Lebesgue points exist; are dense | provable | no | Lemma 4.3 |
| (R) at every point Martin-Löf random relative to f | provable; vacuous in REC | no (weak reading) | Corollary 1.1 |
| (O_int) outer, intensional measure | equivalent to WWKL0, already for f = 0 | yes (degenerate) | Proposition 5.2, Remark 4.7 |
| (O_ext), (O_bar) outer | equivalent to WWKL0 | yes, through measure | Theorem B |
| value f(x) := limit of the averages; cubes leaving [0,1]^d | same answers | — | Remarks 4.8, 5.5 |

## Results in the paper
- **Lemma 3.1 (RCA0).** For a rational polynomial g, rational λ > 0 and n: a finite list V of grid boxes with
  μ(∪V) ≤ c_d‖g‖₁/λ + 2^(−n), c_d = 4^(d+1) + 2, outside which |g| ≤ 3λ/4 and every cube average of |g| is ≤ λ.
  Proof by grid cubes, grid boxes of bounded eccentricity, and a finite Vitali selection (constant 4^d).
- **Theorem A (RCA0).** For an L1 function f = (p_n) on [0,1]^d (‖p_n − p_(n+1)‖₁ ≤ 2^(−n)): open sets U_N, Δ^0_1 in f,
  with μ_int, μ_ext, μ̄ ≤ eps_N = (4c_d + 2)2^(−⌈N/2⌉); every point outside U_N is a Lebesgue point with
  f(x) = lim p_n(x); the measure of C ∩ U_N is located, and every rational box C with μ(C) > eps_N meets the
  complement of U_N. (Lemmas 4.1–4.4, Corollary 4.5.)
- **Corollary 1.1.** LDT under (N_int), (N_ext), (N_bar), (E) (dense form) and (R) in RCA0; REC separates.
- **Lemma 4.6 (RCA0).** Without WWKL0 there are open sets of intensional measure ≤ 2^(−k) containing every point.
- **Remark 4.9.** Consistency with Nies–Triplett–Yokoyama, Theorem 6.8 (1 ⇔ 5) (pseudo-differentiability at some
  point of every effectively uniformly continuous, absolutely continuous, rationally presented function is equivalent
  to WWKL0): in a model of RCA0 + ¬WWKL0 their function is not the indefinite integral of any L1 function with the rate
  of Definition 2.1, since by Theorem A(c) it would be pseudo-differentiable at a Lebesgue point.
- **Theorem B.** For m ∈ {int, ext, bar}: LDT under (O_m) ⟺ WWKL0 over RCA0. Forward: Lemma 5.1 (WWKL0 covering
  lemma in [0,1]^d) and Proposition 5.2 (box and binary codes). Reversal: Lemma 5.3 (the open set of NTY, measure
  ≤ 1 − α, complement of dyadic first coordinates) and Lemma 5.4 (explicit polynomials (1 − (x₁ − r_k)²)^M,
  M = 2^(6(j+k)+6), with L1 rate 2^(−n) and divergence at every dyadic first coordinate).

## Computations (sanity checks; programs and outputs in reproducibility/)
No proof depends on a computation.
- **check_note.py** (standard library, exact, about 23 s, 20 checks, "ALL CHECKS PASSED"): constants of Lemma 3.1
  and formula (1); Lemma 3.1 for d = 1 on 40 random polynomials with (P1)–(P4), (i), and (ii) at all 3,721 points of
  a fine grid outside V with all grid intervals containing them (largest μ(∪V)/(‖g‖₁/λ) = 2.745 against 18); the
  Vitali step in d = 2, 3; the descent of Lemma 4.3; Lemma 5.3 on 150 random trees; the constants of Lemma 5.4
  (exact ∫_{−1}^{1}(1 − u²)^4096 du = 0.027692… < 1/4); the boxes of Lemma 5.1; the weights in Lemma 4.6; the
  trapezoids of Corollary 4.5. Deliberately wrong thresholds (V1, V2) and a wrong definition of E were rejected.
- **original/** (first version of the results): the numerical inequalities (mpmath) and Lemma 3.1 for d = 1 on 60
  polynomials, the Vitali step in d = 2, 3.
- **verification_run_A/**: exact constants and an independent d = 2 implementation of Lemma 3.1.
- **verification_run_B/**: Lemma 3.1 exactly for d = 1 (297 polynomials, 7,832 points, all intervals) and for d = 2
  (210 polynomials, 4,795 points); the Vitali step (1,260 families) and the weak-type bound for 1,650 random step
  functions; Lemmas 5.3, 5.4; the descent of Lemma 4.3 (170 families); each with deliberately wrong inputs, which
  were rejected.
- **Re-runs for the package (2026-10-18):** all programs re-run from copies; all recorded outputs reproduced byte for
  byte, except that the last block of `own_thmB.py` now prints six additional lines (Lemma 5.4, 0 failures, and the
  final line); see the README. The verification run 2 repeated this from an extracted copy of `source.zip` with the
  same result (`independent_run_2/package_rerun_comparison.txt`).
- **independent_run_2/** (verification run 2, on the final text; 54 checks, all passed): exact constants of Lemmas
  3.1, 5.4 and formula (1) (exact infinite sums; exact ∫_0^1 (1 − (t − r)²)^4096 dt for six r; Beta values for even
  J ≤ 120); an independent implementation of Lemma 3.1 for d = 1 (101 polynomials; (ii) at 10,197 points outside V for
  498,642 intervals in arbitrary position; negative controls V2 omitted / threshold 2λ caught) and d = 2 (36
  polynomials, all 277 million boxes of F; (ii) at 7,675 points for 207,225 cubes); the descents of Lemmas 4.3 and 4.4;
  the Vitali step in d = 2, 3; the finite combinatorics of Lemmas 4.6, 5.1, 5.3, Corollary 4.5 and Proposition 5.2.

## Independent verification runs
The results were first obtained with written proofs and two sanity-check programs. Two independent verification
runs, both AI-assisted, followed (2026-10-18); each re-derived the proofs and wrote its own programs, and neither read
the other's report. The final text was then written; its exact program `check_note.py` was written and run for it.
A further AI-assisted verification run (run 2) then examined the final text; see below the table.

| Item | Run A | Run B |
|---|---|---|
| Source and statement (Montalbán, Section 3.4) | read; faithful; no formalisation fixed | read; faithful |
| Readings and measures (BGS02, ADR12, NTY21, Rute) | checked against the sources | checked; observed that (N_int) is trivial by cases |
| Lemma 3.1 | re-derived; d = 2 test | re-derived; exact d = 1 and d = 2 tests; V1 redundant |
| Lemmas 4.1–4.4, Corollary 4.5 | re-derived | re-derived; descent tested |
| Lemmas 5.1, 5.3, 5.4, Theorem B | re-derived; constants exact | re-derived; tested; T′ not needed for intervals |
| Literature | Pathak 2009 obtained; Yu 1994 via ADR12 | Rute 2013, BMN16 found; Dean 2009 note not obtained |
| Verdict | claim stands; seven corrections | confirmed with caveats; four corrections |

Corrections required and made: run A — (1) credit Yu 1994 Lemma 2.1 (as reported by ADR12) and Pathak 2009 Lemma 3.2 for the convergence part,
and restrict the novelty; (2) cite NTY Remark 6.3; (3) the binary-code case of μ̄ (Proposition 5.2, Corollary 4.5);
(4) cite Pathak 2009 directly; (5) the vacuity of (R) in REC; (6) C([0,1]^d) versus BGS02, grid points by the least
number principle (F3), NTY's bound in T′; (7) the explicit judgement on the intended reading. Run B — (1) the
case split for (N_int) (Lemma 4.6, Remark 4.7, split rows of Table 1); (2) credit Rute 2013 Theorem 4.10 and the
remark of Brattka–Miller–Nies; (3) the Dean note was not obtained (stated); (4) the bibliographic completions. The
optional simplifications are Remark 3.2 (V1 can be omitted) and the remark after Lemma 5.3 (T itself suffices).

**Run 2 (on the final text, 2026-10-18).** It read again the cited parts of Montalbán, Pathak, Pathak–Rojas–Simpson,
Brown–Giusto–Simpson, Avigad–Dean–Rute, Nies–Triplett–Yokoyama, Rute (thesis and survey) and Brattka–Miller–Nies and
compared every statement about them with these sources; re-derived every proof line by line, among them the parts
written after runs A and B (Lemma 4.6, Remark 4.7, the binary codes in Corollary 4.5 and Proposition 5.2), and
checked that Theorem A uses no more than Δ⁰₁ comprehension and Σ⁰₁ induction; checked the 13 DOIs with Crossref;
repeated the literature search; wrote its own programs (`independent_run_2/`, all checks passed) and ran the whole
package again. It found no error in a proof. Corrections required and made: (1) the covering statement of Yu and
Simpson is reported in Section 3 of ADR12, not Section 2; (2) NTY Theorem 6.8(5) is cited, with Remark 4.9 on why it
does not conflict with Theorem A(c); (3) Remark 4.7 reworded ((N_int) has content only in models of WWKL0, where it
follows from Theorem A), and Table 1 accordingly; (4) Section 6 now says that the wrong variants of `check_note.py`
were modified copies not included in the package; (5) this run is recorded in the note, in this report and in the
package; (6) the remark after Lemma 5.3 (T in place of T′) rewritten as a short argument.

## Relation to the literature, novelty and scope
- **Searches (18 October 2026).** arXiv API, zbMATH API and Crossref (the Lebesgue differentiation theorem with
  reverse mathematics, WWKL0, second-order arithmetic, randomness); Semantic Scholar lists of works citing
  Montalbán 2011 (104), Pathak–Rojas–Simpson 2014 (48), Pathak 2009 (18), Nies–Triplett–Yokoyama 2021 (15), titles
  screened and the reverse-mathematics ones opened; Miyabe–Nies–Zhang 2016; Nies's Logic Blogs; Simpson's lists of
  papers and talks; a few web searches. OpenAlex refused the requests (rate limit). Run 2 repeated the search on the
  same day: arXiv API (15 queries, 2 look-ups by identifier), Crossref (4 queries), zbMATH Open (4 queries), OpenAlex
  (citation counts only; the lists of citing works were refused), one web search, and Nies's 2023 slides on randomness
  and reverse mathematics. No printed answer to the question was found in these sources; a search that finds nothing
  is not a proof of novelty. A 2009 note of
  E. T. Dean on Pathak's theorem, listed by Semantic Scholar without a venue, could not be obtained.
- **Closest prior work.** Pathak 2009 (Theorem 5.1; Lemma 3.2; Definition 3.4); Pathak–Rojas–Simpson 2014 (Theorems
  3.16, 4.7; Lemmas 3.3, 3.6, 3.13); Rute 2013 (Theorem 4.10); Brattka–Miller–Nies 2016 (remark in Section 1 that the
  strength of the LDT can be studied); Yu 1994 (Lemma 2.1, via ADR12); Brown–Giusto–Simpson 2002 (Definition 2.1,
  Proposition 4.1, Remark 4.3, Lemma 5.1); Nies–Triplett–Yokoyama 2021 (Section 5, Remark 6.3, Definition 6.4,
  Lemma 6.6, Theorem 6.8 including item (5), Remark 6.9); Yu–Simpson 1990 (via ADR12 and NTY); Westrick 2025 (a
  related vacuity).
- **What was read.** Montalbán's preprint (Section 3.4); Pathak 2009 (journal's open version); PRS14 and BGS02 in the
  authors' copies (the statements cited); ADR12 (Sections 2 to 4), NTY21 (Sections 5, 6), Rute's survey (Section 3.5)
  and BMN16 (Section 1) in their arXiv versions, whose numbering is used (journal versions not compared); Rute's
  thesis (Section 4.2); Westrick's abstract. Not read: Yu 1994, Yu–Simpson 1990, Simić 2004 (what the note says
  about them is taken from ADR12, NTY21 and Rute's survey). All DOIs were checked with Crossref (13 records), and
  again by run 2.
- **Caveats.** The RCA0-formalisability is argued in prose with explicit moduli (the usual standard), not machine
  checked. Readings in which the measure of the exceptional set must exist as a real (ACA0-level) and higher-order
  formulations are not treated. Which reading Montalbán and Simpson intended is not recorded in the source.
- **Scope.** The note answers Question 17 for each reading above and states a judgement on the intended one. No
  priority is claimed; the results are close to known techniques and may be known to experts.

## Public release and license
This paper, its source files, and this verification report are licensed under the Creative Commons Attribution
4.0 International License (CC BY 4.0): https://creativecommons.org/licenses/by/4.0/