Trace — 2607.19283v1

DECLARATION: Central claim — for the paper's standard data-dependent order-k ENO reconstruction of compactly supported cell averages on the unit grid, the nonnegative source Q_k uniformly controls the (k+1)-moment of neighboring jumps after multiplication by the amplitude to power k-1 exactly when k=2 or k is odd; it fails structurally for every even k>=4 (with further quasi-uniform and cohomological refinements). Declared target — R3 core: first give a faithful Lean 4/mathlib statement using the paper's actual ENO stencil recursion and reconstruction, then verify its finite decidable/numerical claims, and formalize and prove the new hidden-square/even-difference energy lemma on which the odd-order parity argument rests.

Phase 1 setup: inspected the full local mathlib checkout (Lean 4.33.0-rc1) and existing worktree. The repository contains unrelated user changes and the stock mathlib Counterexamples root; I will preserve them and create only new reproduction files.

API search found Mathlib.LinearAlgebra.Lagrange.interpolate for the faithful cumulative-interface interpolation definition. Plan: use finitely supported integer-indexed cell averages, the paper's recursive left endpoints, cumulative values, and the derivative of the Lagrange interpolant evaluated at the interface.

First R1 elaboration attempt failed only at two API details: Lean could not infer the `Fin (k+1)` index of `Lagrange.interpolate`, and this mathlib exposes generic `Odd k` rather than `Nat.Odd k`. Added explicit indices and corrected the parity name; no mathematical definition changed.

R1 achieved: `lake env lean Repro.lean` elaborates cleanly. `theoremA_statement` quantifies the exact parity iff using the standard recursive ENO endpoints, cumulative-interface Lagrange reconstruction, reconstructed trace jump, compactly supported amplitude, and the actual data-dependent source Q_k.

First R2 file attempt hit a version/API dead end: this checkout has no `Mathlib.Tactic.NativeDecide` module. I also rejected native-code proof certificates for the final artifact because the axiom audit should remain kernel-transparent; switched the finite computations to kernel `decide`.

Second R2 approach using mathlib `MvPolynomial` failed: its ring and variable constructors are noncomputable, so kernel `decide` cannot normalize coefficient expressions (and native evaluation would compromise the desired audit). Replaced it with a transparent four-variable coefficient-function implementation of addition, Cauchy multiplication, powers, partial derivatives, and the Appendix-A functional.

The transparent but naive recursive polynomial-power evaluator was mathematically correct but simplification remained exponential (over two minutes for twelve degree-seven coefficients), so I terminated it. Third R2 approach: use the multinomial coefficient formula for powers of linear forms and only one bounded Cauchy product, matching the actual structure of G_raw.

R2 finite audit succeeded with `lake env lean Computations.lean`: Gaussian-binomial/partition count dim H^1_{2,7}=10; 120 degree-seven monomials; all 120 checks L∘N_7=0; all twelve coefficients used by Appendix A; L(G_raw)=-32; and eta_*''>=3/7. `#print axioms` reports only standard propext/Classical.choice/Quot.sound and no sorryAx or native-evaluation axiom.

First R3 elaboration attempt failed before the proof because the minimal imports did not instantiate the real numbers' algebraic structures. Switched `Core.lean` to the umbrella Mathlib import; the summation-by-parts argument itself had not yet been typechecked.

Declared R3 achieved: `lake env lean Core.lean` proves equation (3.20), its s-fold iteration, Lemma 3.3's exact hidden-square identity (3.18), and the localized-amplitude inequality (3.19) for every finitely supported real sequence. Axiom prints contain only propext/Classical.choice/Quot.sound, with no sorryAx.

R4 feasibility check: mathlib contains a Gagliardo-Nirenberg-Sobolev development but no cardinal B-spline API or the paper's discrete L-infinity interpolation inequality. A full proof would additionally require formalizing the data-dependent localized FMT identity/source equivalence and the Euler-polynomial strict-comparison counterexample family; these are distinct major developments beyond the completed core lemma.

R2 overshoot: added exact fourth-order Euler-block computations at (L,N)=(2,4) and (4,16). The finite jump moment/amplitude/localized-source triples are (6040,10,106) and (49577664,84,1034); both jump lists sum to zero, and the normalized moment/localized-source quotient increases, matching the counterexample mechanism.

Final audit passed: Repro.lean, Computations.lean, and Core.lean all elaborate consecutively with `lake env lean`; source scan finds no sorry, axiom, or admit; all printed axiom sets contain only standard Lean/mathlib axioms; every trace.jsonl line parses as JSON. Removed the temporary rendered PDF pages.

VERDICT reproduced at declared target R3. R1, R2, and R3 are complete; R4 was not claimed and remains beyond this run because it requires the full localized FMT/source-equivalence theory, discrete B-spline Gagliardo-Nirenberg development, and asymptotic strict-stencil Euler counterexamples.