# Axiom Audit

*Centralized registry of every textbook axiom in `markov-semigroups`.
Each row records the axiom's literature reference, vetting verdict,
discharge plan (if any), and downstream consumers. Last refreshed:
2026-05-21.*

## Purpose

In this project, an **axiom** is a *vetted provable theorem with a vetted
discharge plan* — not a fundamental unprovable assumption. Each axiom
listed below is:

1. A standard textbook fact, with explicit literature citation.
2. Reviewed for type correctness, hypothesis sufficiency, and
   non-vacuity (typically by a Gemini deep-think pass and/or a
   literature cross-check).
3. Accompanied by a concrete plan to discharge it into a Lean theorem
   (inline in the row, or linked to a dedicated discharge-plan doc).

We use the `axiom` keyword as a *staging point* — it lets the project
proceed to use a result before its full Lean proof is assembled, while
keeping the trust boundary explicit and discharge progress trackable.
The goal is for every entry below to eventually become a proved
theorem.

Format and conventions for this audit doc:
`~/.claude/AXIOM_AUDIT_FORMAT.md`.

## Conventions

**Vetting source codes** (per
[research-dev `AXIOM_MANAGEMENT.md`](https://github.com/mrdouglasny/research-dev/blob/main/library/lean/AXIOM_MANAGEMENT.md)):
- **DT** — Gemini deep-think (slow, high-reasoning vet pass)
- **GR** — Gemini chat review (`gemini-3-pro-preview`)
- **CX** — Codex (independent re-derivation / cross-check)
- **LP** — literature proof with explicit page reference
- **SA** — self-audit (author cross-checked against textbook by hand)
- **PR** — peer review (external mathematician)

**Rating scale:**
- **Standard** — well-established textbook fact with multiple independent references
- **Likely correct** — checked, consistent with textbook(s) but not externally vetted
- **Needs review** — placeholder; statement plausible but not yet vetted
- **Placeholder** — known to need replacement; statement may be approximate (e.g., infrastructure-stub)
- **Flagged** — concern raised; do not consume downstream until resolved

## Summary

13 registered axioms total (11 → 12 on 2026-05-16 when the repo-wide
audit surfaced a previously-undocumented General axiom; → 13 same day
when the `feat/lp-carrier-stdGaussianFin-dirichletmarkov` merge
(`ba9a8de`) added the vetted general `gaussianOU_heatEquation_within_zero`
— see the "Gross-discharge: OU pointwise heat equation" section below).
Of these:
- **2 core hypercontractivity** axioms (Gross 1975) — abstract LSI ↔ HC
- **1 Stroock-Varopoulos** axiom — intermediate-step lemma for Gross,
  added 2026-05-13 as a vetted atomic textbook bridge
- **2 concentration / Poincaré** axioms (Herbst MGF + LSI ⇒ Poincaré)
- **2 Dobrushin-Zegarlinski** axioms — Otto-Reznikoff LSI + Helffer-Sjöstrand Cov
- **1 Matrix** axiom — diamagnetic resolvent inequality
  (`m_matrix_inverse_nonneg` relocated upstream to `SpectralPositivity`
  and re-exported as a theorem, so it is no longer counted here)
- **1 General/SchwartzConvolution** axiom —
  `contDiff_top_convolution_schwartzKernel` (Lieb–Loss Thm 2.16;
  Folland *Real Analysis* 2nd ed. Ch. 8 §2). Was **unregistered in
  this audit doc** until the 2026-05-16 sweep, but **is vetted** in
  its file docstring (`gemini-2.5-pro` Standard + `gemini-3.1-pro-preview`
  Likely correct, 2026-05-12, integrand revised per 3.1-pro). Rating
  **Likely correct**. No internal consumers (staged infrastructure;
  `ouSemigroup_contDiff` was discharged by a different route).
- **GaussianFin** multivariate Gaussian BE-instance primitives
  (merged to main 2026-05-13, commit `8ed9e52`), all
  gemini-3.1-pro-preview vetted **Standard**, all tensor-lift analogues
  of historical 1D primitives discharged in `Gaussian1D`:
  - `ouSemigroupFin_preserves_IsCore` (Mehler smoothing preservation,
    BGL §2.7.1 + §3) — **the one remaining declared GaussianFin axiom**.
  - `ouSemigroupFin_entropy_sq_decay_bound` (entropy decay for `f²`,
    BGL Thm 5.5.2) — **Workstream N1.c, 2026-05-19: FULLY
    DISCHARGED**; converted to an axiom-free `theorem` via the
    Gemini-vetted 1-parameter telescoping route (frozen-slot
    single-real-parameter commutation, abstract slice-derivative step
    lemma, measure-general Cauchy–Schwarz orthogonal Fisher
    monotonicity, `Finset.induction` telescope). The original
    "C∞-iterate / C²-core" plan was superseded — no new core predicate
    was needed. Verified `#print axioms = [propext, Classical.choice,
    Quot.sound]`. See the per-axiom row below.
  - `ouSemigroupFin_l2_sq_hasDerivWithinAt` (de Bruijn-style
    L²-derivative identity, BGL Prop 4.7.1) was **discharged
    2026-05-19** in commit `897b661` via the already-counted G2 axioms
    `gaussianFin_diffQuot_tendsto_Lp` and `gaussianFin_integrationByParts`
  Sub-stage N1 of the OU hypercontractivity discharge is complete;
  Stages N2 + N3 (gaussian-hilbert wire-in to discharge
  `ouSemigroupAct_eLpNorm_hypercontractive`) in progress.

**The entire Gaussian1D / OU chain is now axiom-free.** All BGL Ch. 2
and §5.5 facts have been discharged. The general-purpose
`MarkovSemigroups/General/OUEntropyDecomposition.lean` file is also
axiom-free. Discharges from 2026-05-12:
- **A1** (`ouSemigroup_fisher_info_decay`): Cauchy-Schwarz on the
  Mehler probability kernel.
- **A2-boundary** (`hasDerivWithinAt_entropy_ouSemigroup_zero`):
  derived from A2 interior + DCT-based continuity.
- **A2 interior** (`hasDerivAt_entropy_ouSemigroup`): proved via
  Stein-IBP-based formula for `(P_t g)''` + parametric DCT for the
  entropy integral + bilinear Dirichlet form identity
  (`gaussian_dirichlet_form_bilinear` in EuclideanStein.lean).

**Discharged axioms** (Gaussian1D, was 9 + 2 atomic; now 0 atomic axioms
in the concrete instance):
* All 9 original Gaussian1D axioms (`ouSemigroup_*`) — see "Reduced to
  theorems" sections below for the discharge details.
* The 2 atomic Mehler-kernel axioms (`ouSemigroup_contDiff` via Path C
  Hermite IBP, `ouSemigroup_entropy_sq_decay_bound` via Path A1+A2
  decomposition).

The Wiener-chaos / multivariate-Hermite cluster (3 OU placeholder
axioms + 1 external `polynomial_dense_L2_of_subGaussian`, plus the
proved theorems `hermiteMulti_dense`, `wienerChaos_isHilbertSum`,
`bonami_nelson_*`, `polynomial_chaos_concentration`) **moved to
[gaussian-hilbert](https://github.com/mrdouglasny/gaussian-hilbert)**
on 2026-05-10. See that repo for the current home and audit.

**Excluded by policy (not counted above):**
`Instances/WorkInProgress/EuclideanTests.lean` declares 4 local
scaffolding axioms (`gaussianResolvent`, `gaussianResolvent_ibp`,
`gaussianResolvent_ibp_integrable`, `gaussianBochner_identity`) used
only for a conditional in-file check. They are not textbook axioms,
are not consumed by the main tree, and live in `WorkInProgress`;
acknowledged here for exhaustiveness but deliberately not registered
as project axioms.

## Audit table

### Core: hypercontractivity / Gross duality / Stroock-Varopoulos

The three core axioms are now stated against the bundled
[`DirichletMarkovSemigroup`](MarkovSemigroups/Abstract/Hypercontractivity.lean)
structure after the 2026-05-13 **Lp-carrier refactor** documented in
[`docs/lp-carrier-refactor-design.md`](docs/lp-carrier-refactor-design.md).
This refactor changed the abstract semigroup carrier from the
mathematically flawed pointwise space `(X → ℝ) → (X → ℝ)` to bounded
operators on `L²(μ)`, `Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ`, while keeping the
active axiom count unchanged at 11.

Post-refactor statement shape:
* time remains `t : ℝ` but all semigroup laws are restricted to `t ≥ 0`;
* the form-semigroup compatibility is the right-derivative statement
  `HasDerivWithinAt _ _ (Set.Ici 0) 0`;
* `IsHypercontractive` now quantifies over `f : Lp ℝ 2 μ` with an
  explicit `MemLp` hypothesis at exponent `p`;
* conservation is phrased as fixing any a.e.-constant-`1` `L²` element,
  and symmetry is the `L²` inner-product identity
  `⟪f, P_t g⟫ = ⟪P_t f, g⟫`.

| Axiom | File:Line | Reference | Rating | Vetting | Strategy / Plan | Consumers |
|---|---|---|---|---|---|---|
| `gross_lsi_implies_hypercontractive` | [`Abstract/Hypercontractivity.lean:261`](MarkovSemigroups/Abstract/Hypercontractivity.lean#L261) | Gross (1975) Amer. J. Math. 97, Theorem 1 | Standard | LP, SA, GR (gemini-3.1-pro-preview 2026-05-13: re-vet on the Lp-carrier refactor flagged a real soundness issue — the prior signature without `0 < ρ` would prove `False` because `SatisfiesLogSobolev D ρ` is trivially true for `ρ ≤ 0` while `IsHypercontractive` bakes in `0 < ρ`. Fixed in commit `78b2694` by adding `(hρ : 0 < ρ)` to the signature. Final 3.1-pro verdict on the fixed statement: **Standard / Likely correct.**) | Genuine textbook duality theorem on the Lp ℝ 2 μ →L Lp ℝ 2 μ carrier with the `0 < ρ` firewall. Full proof differentiates `‖P_t f‖_{L^{q(t)}}` along `q(t) = 1 + (p-1)e^{2ρt}` for `f : Lp ℝ 2 μ` ∩ `L^p`, applies LSI to `\|f\|^{q/2}` plus Stroock-Varopoulos. **Discharge route vetted by Gemini deep-think 2026-05-16**: corrected Route A — hille-yosida generator bridge (kills the right-derivative trap), weak-L² difference-quotient + convexity for the moving-exponent derivative, and **S–V as a theorem hypothesis, not proven abstractly** (Beurling–Deny would be circular). Full spec: [`plans/gross-discharge.md`](plans/gross-discharge.md). **Progress 2026-05-19 → 2026-05-20:** the **P2 Leibniz kernel `hasDerivWithinAt_integral_of_strongL2Deriv`** (the analytic crux of P2) is **fully proved axiom-free** in `Abstract/GrossODE.lean`. `#print axioms` reports only `[propext, Classical.choice, Quot.sound]` (the Mathlib core). Proof = 11-lemma toolkit (FTC factoring, M_σ + factorization, a.e./pointwise sub bounds, measurability, MemLp 2, UI, **in-measure convergence**, **Vitali L²-convergence**, target MemLp) + ~150-line 9-step main body (Lp lifting via Classical padding, `Filter.Tendsto.inner`, `L2.inner_def`, integrated factorization + `field_simp`-driven slope close, `MemLp.of_bound` on the compact envelope `Icc (-(M⊔0)) (M⊔0)` for integrability). Vetted-corrected hypothesis (the originally-stated form was Gemini-counterexample false). See [`plans/archive/p2-strongL2-leibniz-discharge.md`](plans/archive/p2-strongL2-leibniz-discharge.md). Statement is project-definition-free → Mathlib-upstreamable. **Update 2026-05-21 — ABSTRACT SPINE COMPLETE:** the hypothesis-parameterised theorem `GrossODE.gross_lsi_implies_hypercontractive_of_hypotheses` is **fully proved and `Abstract/GrossODE.lean` is sorry-free** (`#print axioms` = `[propext, Classical.choice, Quot.sound]`); P2/P3 and the general-`f` reduction all closed, taking four per-instance predicates (`CoreSemigroupInvariant`, `GeneratorCompat`, `StroockVaropoulos` at `1 < q`, `CoreLpL2Approx`). **W DONE (2026-05-22):** the four GaussianFin/OU predicates are discharged in `Instances/WorkInProgress/EuclideanHypercontractive.lean` (`stdGaussianFin_coreSemigroupInvariant` / `_generatorCompat` / `_stroockVaropoulos` / `_coreLpL2Approx`) and assembled into `stdGaussianFin_isHypercontractive` via the proved `_of_hypotheses`. After the same day's generator discharges, `#print axioms stdGaussianFin_isHypercontractive = [propext, Classical.choice, Quot.sound]`. The `StroockVaropoulos` predicate carries `∃ε>0, ε≤u` a.e. (strict positivity for the chain rule, supplied at the unique GrossODE call site). | **No longer consumed by the concrete chain (since 2026-05-22):** `gaussian-hilbert/.../HypercontractivityFromBE.lean` now routes `stdGaussianFin_dirichletMarkovSemigroup_isHypercontractive` (→ `ouSemigroupAct_eLpNorm_hypercontractive` → `bonami_nelson_chaos` → **pphi2**) through the proved `GaussianFin.stdGaussianFin_isHypercontractive`, which does **not** use this axiom. Retained only for the abstract in-repo wrappers `DirichletMarkovSemigroup.hypercontractive_of_logSobolev` / `gross_equivalence`. Not consumed by `lgt`, `pphi2N`. |
| `gross_hypercontractive_implies_lsi` | [`Abstract/Hypercontractivity.lean:271`](MarkovSemigroups/Abstract/Hypercontractivity.lean#L271) | Gross (1975) Amer. J. Math. 97, Theorem 2 | Standard | LP, SA, GR (gemini-3.1-pro-preview 2026-05-13, re-vetted on the post-refactor `Lp ℝ 2 μ` carrier statement) | Reverse implication: differentiate the hypercontractive bound at `t = 0` with `p = 2`, `q = 2 + ε`, and pass `ε → 0`. Same effort scale as the forward direction; the refactor changes only the formal carrier, not the textbook content. | `DirichletMarkovSemigroup.logSobolev_of_hypercontractive`, `DirichletMarkovSemigroup.gross_equivalence` (same in-file-only consumer status) |
| `stroock_varopoulos` | [`Abstract/Hypercontractivity.lean:242`](MarkovSemigroups/Abstract/Hypercontractivity.lean#L242) | Stroock (1992), Varopoulos (1985); BGL Prop 1.7.1 / §1.7 | Standard | GR (gemini-3.1-pro-preview two-pass 2026-05-13: first pass `Needs Revision` flagging vacuous `f ≥ ε > 0` on infinite-measure spaces; revision to `f ≥ 0` applied; second pass `Standard`, confirming the post-refactor statement on `DirichletMarkovSemigroup`, the `p ≥ 2` power regularity at 0, the sharp constant `4(p-1)/p²`, edge cases `p = 2` and `f ≡ 0`, and the general symmetric-Markov scope) | **Bypassed in the concrete Gaussian chain (2026-05-22).** `Diffusion/StroockVaropoulos.lean` proves the *equality* form `BakryEmerySpace.stroockVaropoulos_eq` for any diffusion (carré-du-champ) form satisfying `BakryEmerySpace.RpowChainRule` (`Γ(uʳ,g)=r·u^{r-1}·Γ(u,g)`); `GaussianFin.rpowChainRule` discharges that for `ouGammaFin` via `partialDeriv_rpow`, so `stdGaussianFin_stroockVaropoulos` closes by `le_of_eq` and `#print axioms stdGaussianFin_isHypercontractive` no longer lists this axiom. The axiom is retained for the abstract / non-diffusion (general Markovian Dirichlet form) case, where S–V is a strict inequality proved via Beurling–Deny convexity `(a-b)(a^{p-1}-b^{p-1}) ≥ (4(p-1)/p²)(a^{p/2}-b^{p/2})²` — a marked slot for that proof exists in `Diffusion/StroockVaropoulos.lean`. |

### Concentration / Poincaré

| Axiom | File:Line | Reference | Rating | Vetting | Strategy / Plan | Consumers |
|---|---|---|---|---|---|---|
| `herbst_mgf_bound` | [`Abstract/Concentration.lean:98`](../MarkovSemigroups/Abstract/Concentration.lean#L98) | BGL §5.4.1 (Herbst's lemma); Ledoux (2001) §1; Otto-Villani (2000) JFA 173 §3 | Standard | LP, SA | Three-line proof: differentiate `t ↦ log E[exp(tF)]` and apply LSI to the function `F + t·c`. Direct discharge would require the full LSI-derivative-of-MGF calculus on `Lp`. Estimated 1-2 weeks. | `lipschitz_concentration_of_lsi` and variants; `hasSubgaussianMGF_of_lsi` (proven Mathlib `HasSubgaussianMGF` bridge); `memLp_of_lsi`; the Zegarlinski concentration corollaries in `DobrushinZegarlinski/Concentration.lean` |
| `poincare_of_lsi` | [`Abstract/Concentration.lean:351`](../MarkovSemigroups/Abstract/Concentration.lean#L351) | BGL Proposition 5.1.3 (LSI ⇒ Poincaré with same constant) | Standard | LP, SA | Standard textbook implication: take `f = 1 + εg`, expand both sides of LSI to second order in ε. Estimated 3-5 days to formalize (Taylor expansion + careful bookkeeping). | `variance_lipschitz_le_of_lsi`, `variance_lipschitz_le_of_zegarlinski` |

### General/OU diffusion (axiom-free!)

[`MarkovSemigroups/General/OUEntropyDecomposition.lean`](../MarkovSemigroups/General/OUEntropyDecomposition.lean)
is now axiom-free. The three originally-axiomatized de Bruijn /
Fisher-decay facts have all been proved.

**Proved (2026-05-12):**
* `ouSemigroup_fisher_info_decay` (A1, BGL Proposition 5.5.2) —
  Cauchy-Schwarz on the Mehler probability kernel applied with
  `A := g'/√g, B := √g` gives `(P_t g'(x))² ≤ P_t((g')²/g)(x) · P_t g(x)`.
  Combined with the Mehler derivative formula `(P_t g)' = e^{-t} P_t g'`
  and divided by `P_t g ≥ ε > 0`, then integrated against γ +
  γ-invariance via `ou_kernel_map`. ~400 lines including a
  polynomial-discriminant Cauchy-Schwarz helper for `γ`.
* `hasDerivWithinAt_entropy_ouSemigroup_zero` (A2 at `t = 0+`) —
  derived from A2 (`t > 0` interior version) + DCT-based continuity
  of the entropy and Fisher info at `s = 0+` + Mathlib's
  `hasDerivWithinAt_Ici_of_tendsto_deriv`. ~330 lines.
* `hasDerivAt_entropy_ouSemigroup` (A2 interior, BGL §5.5
  de Bruijn identity for `t > 0`) — proved via a Stein-IBP-based
  formula for `(P_t g)''` (avoiding the need for `g''`), parametric
  DCT for the entropy integral, and the bilinear Dirichlet form
  identity (`gaussian_dirichlet_form_bilinear`). ~740 lines.

### General/SchwartzConvolution

**Unregistered in this audit doc** until the repo-wide sweep on
2026-05-16 — but **vetted in its file docstring**: `gemini-2.5-pro`
returned **Standard** and `gemini-3.1-pro-preview` returned **Likely
correct** (both 2026-05-12), the latter prompting a real revision
(integrand swapped to `K(x−y)·f y` so differentiation-under-the-
integral applies directly, since `f` is only measurable). It has no
internal consumers (staged infrastructure; the OU smoothing fact
`ouSemigroup_contDiff` was ultimately discharged by the Path-C
Hermite-IBP route, not via this axiom), so no proved theorem in the
repo transitively depends on it.

| Axiom | File:Line | Reference | Rating | Vetting | Strategy / Plan | Consumers |
|---|---|---|---|---|---|---|
| `contDiff_top_convolution_schwartzKernel` | [`General/SchwartzConvolution.lean:103`](../MarkovSemigroups/General/SchwartzConvolution.lean#L103) | Lieb–Loss *Analysis* (2nd ed.) Thm 2.16; Folland *Real Analysis* (2nd ed.) Ch. 8 §2; Reed–Simon I Thm V.4 | Likely correct | GR (gemini-2.5-pro 2026-05-12 **Standard**; gemini-3.1-pro-preview 2026-05-12 **Likely correct**, integrand revised `K(x−y)·f y` per 3.1-pro; hypotheses confirmed tight = Sobolev `W^{∞,1}×L^∞`) | For a `C^∞` kernel `K` with all iterated derivatives Lebesgue-integrable and bounded measurable `f`, `x ↦ ∫ K(x−y)·f(y) dy` is `C^∞`. Discharge (~200–400 lines): induction on differentiation order via Mathlib's `hasDerivAt_integral_of_dominated_loc_of_deriv_le`, derivative falling on the smooth factor `K`. | None internal (staged; OU smoothing discharged via Path-C instead). |

### Gaussian1D BGL Ch. 2 (0 axioms — instance is axiom-free)

All originally-axiomatized Mehler-kernel-level facts are now proved.
The two atomic textbook bridges remaining (`ouSemigroup_contDiff` and
`ouSemigroup_entropy_sq_decay_bound`) have been **discharged** via
Path C (Hermite IBP) and the A1+A2 decomposition above, respectively.
See "Reduced to theorems" below.

**Six originally axiomatized 1D facts were reduced to theorems**:
- `ouSemigroup_l2_decay_bound` (FTC + gradient decay)
- `ouSemigroup_ergodic` (double DCT on Mehler integrand)
- `ouSemigroup_entropy_sq_ergodic` (DCT for `s log s` + compactness)
- `ouSemigroup_compose` (Gaussian convolution via `gaussianReal_add_gaussianReal_of_indepFun`)
- `gaussian2D_orthogonal_invariance` (proved by Codex via `stdGaussian_map` + `map_pi_eq_stdGaussian` through the `EuclideanSpace ℝ (Fin 2) ≃ₗᵢ WithLp 2 (ℝ × ℝ)` isometry)
- `ouSemigroup_gradient_decay` (2026-05-12) — proved via the new theorem
  `hasDerivAt_ouSemigroup` (Mehler-derivative formula via Mathlib's
  `hasDerivAt_integral_of_dominated_loc_of_deriv_le`) + Jensen +
  γ-invariance (Fubini + `ou_kernel_map`). Additionally,
  `stein_identity_standard` (Stein's identity for the standard Gaussian,
  BGL §1.15) is now also proved, paving the way for further discharges.
- `ouSemigroup_preserves_IsCore` (2026-05-12) — DECOMPOSED, then FULLY
  DISCHARGED. The bounded parts proved via `ouSemigroup_preserves_bounds`
  (using `hasDerivAt_ouSemigroup_C1` weakened-hypothesis Mehler-derivative
  and `hasDerivAt_deriv_ouSemigroup` second-order formula). Also proved as
  cleanup: the **Gaussian Dirichlet form identity**
  `∫ g · L g dγ = -∫ (g')² dγ` for `IsCore g`
  (`gaussian_dirichlet_form_identity`, BGL §1.6), via Stein applied to
  `h := g · g'` — bridges `BakryEmerySpace` energy and the L²(γ)
  generator inner product. The `C^∞` smoothing residue is now also
  discharged (see `ouSemigroup_contDiff` entry below).
- `ouSemigroup_l2_sq_hasDerivWithinAt` (2026-05-12) — FULLY DISCHARGED.
  The `t > 0` case proved via `hasDerivAt_l2sq_ouSemigroup_pos`
  (heat equation `hasDerivAt_t_ouSemigroup` + Mathlib's parametric
  derivative + Gaussian Dirichlet form identity via Stein). The `t = 0`
  boundary case (initially isolated as the residue axiom
  `ouSemigroup_l2sq_hasDerivWithinAt_zero`) is now also proved
  (`ouSemigroup_l2sq_hasDerivWithinAt_zero` is now a theorem in
  `EuclideanStein.lean`) via Mathlib's `hasDerivWithinAt_Ici_of_tendsto_deriv`
  combined with DCT-based pointwise/integral continuity of `P_s f` and
  `(P_s f')` at `s = 0+`. All proofs live in `EuclideanStein.lean`.
- `ouSemigroup_contDiff` (2026-05-12) — FULLY DISCHARGED via the
  **Hermite IBP path** (Path C) in
  `Instances/WorkInProgress/EuclideanHermite.lean`. The discharge
  establishes the closed-form iterated-derivative identity
  `(P_t f)^{(n)}(x) = (a/b)^n · ∫ y, H_n(y) · f(a·x + b·y) ∂γ`
  by induction on `n`, combining parametric integral differentiation
  with `hermite_ibp_gaussian` (the n-th-order Stein identity:
  `∫ H_n · F' dγ = ∫ H_{n+1} · F dγ`). The C^∞ conclusion then follows
  via `contDiff_of_differentiable_iteratedDeriv`. As part of this
  discharge, `IsCore` was refactored to use `ContDiff ℝ ∞` (C^∞)
  rather than `ContDiff ℝ ⊤` (analyticity / ω) since in current
  Mathlib `⊤ : WithTop ℕ∞ = ω`, and the project's intent throughout
  has been C^∞ smoothing. The new theorem
  `ouSemigroup_contDiff_bounded` and the relocated
  `ouSemigroup_preserves_IsCore` are in `EuclideanHermite.lean`.
- `ouSemigroup_entropy_sq_decay_bound` (2026-05-12) — FULLY DISCHARGED
  via decomposition into 3 atomic axioms in
  `MarkovSemigroups/General/OUEntropyDecomposition.lean`:
  `ouSemigroup_fisher_info_decay` (A1), `hasDerivAt_entropy_ouSemigroup`
  (A2), and `hasDerivWithinAt_entropy_ouSemigroup_zero` (A2-boundary).
  The proof (`ouSemigroup_entropy_sq_decay_bound_proved` in
  `Instances/WorkInProgress/EuclideanEntropyDecay.lean`, ~550 lines)
  composes these via the ε-regularization `g_ε := f² + ε`, FTC inequality,
  and DCT for the `ε → 0` limit. The `bakryEmerySpace` instance was
  relocated to `EuclideanEntropyDecay.lean` (from `EuclideanStein.lean`)
  so its `semigroup_entropy_sq_decay_bound` field can call the proved
  theorem directly. Net: 1 broad Gaussian1D axiom replaced by 3
  focused atomic axioms in `General/` (reusable for any future
  BakryEmerySpace instance); Gaussian1D itself is axiom-free.

### GaussianFin BGL Ch. 2 (multivariate Gaussian BE-instance work-in-progress)

The multivariate analogue of `Gaussian1D` on `(Fin n → ℝ, γ_n)` lives
in `Instances/WorkInProgress/EuclideanFin.lean` (merged to main
2026-05-13, commit `8ed9e52`). The complete BE-instance
`stdGaussianFin.bakryEmerySpace n : BakryEmerySpace (Fin n → ℝ)`
(EuclideanFin.lean:2814) has all 22 BE fields filled.
Before the 2026-05-19 discharge, `#print axioms
stdGaussianFin.bakryEmerySpace` closed over the three GaussianFin
axioms. The de Bruijn slot is now supplied by the proved theorem
`GaussianFin.ouSemigroupFin_l2_sq_hasDerivWithinAt`, whose verified
closure is the two G2 axioms
`gaussianFin_diffQuot_tendsto_Lp` / `gaussianFin_integrationByParts`
plus the still-active smoothing axiom
`ouSemigroupFin_preserves_IsCore` (and the standard Lean trio).

The supporting proved theorems (`ouSemigroupFin_zero/mean/contraction/
selfAdjoint/compose`, `ouSemigroupFin_gradient_decay`,
`ouSemigroupFin_ergodic`, `ouSemigroupFin_entropy_sq_ergodic`,
`ouSemigroupFin_l2_decay_bound`, `fderiv_ouSemigroupFin_eq`,
`contDiffOne_ouSemigroupFin`, kernel-pushforward infrastructure
`mixCLM/rotCLM/ou_kernel_map_fin/charFunDual_γFin`, the sectionwise
Stein identity, and the N1.4 derivative-bridge / N1.5 infrastructure)
land in the same file (~2850 lines, 0 sorries, originally 3 axioms
total; one of those is now discharged in `EuclideanFinBE.lean`).

The `IsCoreFin` definition was harmonized to `ContDiff ℝ ∞` (matching
`Gaussian1D.IsCore`) in commit `6bf390b` to enable the smoothing-axiom
vetting. The harmonization was build-stable; no upstream callers
required adaptation beyond the rename.

Phase 2 (`EuclideanFinLp.lean`, 2026-05-15) adds the concrete
`DirichletMarkovSemigroup` wrapper
`GaussianFin.stdGaussianFin_dirichletMarkovSemigroup n` on the new
`Lp ℝ 2 (γFin n)` carrier introduced by the 2026-05-13
[Lp-carrier refactor](docs/lp-carrier-refactor-design.md). The
operator-valued semigroup laws are now proved theorems. Phase 2.5
removes the interim deviation from the Phase 2 brief: the bundle
field `energy_eq_deriv` is now obtained from the proved theorem
`ouSemigroupFin_l2_sq_hasDerivWithinAt`, and the dependency surfaces
through the already-counted G2 axioms rather than through a dedicated
GaussianFin de Bruijn axiom. This closes one active branch-local
axiom: **19 → 18**.

| Axiom | File:Line | Reference | Rating | Vetting | Strategy / Plan | Consumers |
|---|---|---|---|---|---|---|
| `ouSemigroupFin_l2_sq_hasDerivWithinAt` | [`Instances/WorkInProgress/EuclideanFinBE.lean:446`](../MarkovSemigroups/Instances/WorkInProgress/EuclideanFinBE.lean#L446) | Bakry-Gentil-Ledoux *Analysis and Geometry of Markov Diffusion Operators* (Springer 2014), Proposition 4.7.1 | **DISCHARGED 2026-05-19** | DT, GR (gemini-2.5-pro deep-think 2026-05-13 + gemini-3.1-pro-preview re-vet 2026-05-13; both passes confirmed type-correctness, hypothesis sufficiency, non-vacuity, correct strength, and discharge plan feasibility; 3.1-pro added the nuance that `IsCoreFin` closure under the semigroup is not needed for the statement because Lean integrals are total and `ouSemigroupFin_preserves_core_bounds` already gives the required integrability). Discharged by Codex in commit `897b661`. | Multivariate de Bruijn-style derivative identity `d/ds \|_{s=t} ∫ (P_s f)² dγ_n = -2 · ∫ Γ_n(P_t f, P_t f) dγ_n`. **Discharged 2026-05-19 via the G2 axioms** `gaussianFin_diffQuot_tendsto_Lp` and `gaussianFin_integrationByParts`: identify `∫ (P_s f)^2` with the `L²` pairing `⟪[f], P_{2s}[f]⟫`, differentiate the pairing using the strong-`L²` difference-quotient theorem, then convert the derivative to `-2·E(P_t f, P_t f)` via the multivariate Gaussian integration-by-parts identity. Verified `#print axioms GaussianFin.ouSemigroupFin_l2_sq_hasDerivWithinAt = [propext, Classical.choice, Quot.sound, GaussianFin.gaussianFin_diffQuot_tendsto_Lp, GaussianFin.gaussianFin_integrationByParts, GaussianFin.ouSemigroupFin_preserves_IsCore]`. | Consumed by `ouSemigroupFin_l2_decay_bound` (derived theorem), the multivariate `BakryEmerySpace (Fin n → ℝ)` wrap, and `GaussianFin.stdGaussianFin_dirichletMarkovSemigroup` via `energy_eq_deriv`. Downstream consumer in gaussian-hilbert: `ouSemigroupAct_eLpNorm_hypercontractive` discharge via Gross-LSI-implies-HC route. |
| `ouSemigroupFin_preserves_IsCore` | [`Instances/WorkInProgress/EuclideanFin.lean`](../MarkovSemigroups/Instances/WorkInProgress/EuclideanFin.lean) | Bakry-Gentil-Ledoux §2.7.1 + §3 (heat-kernel smoothing); 1D analogue historically axiomatized at `Euclidean.lean:488` and proved in commit `890e022` (Path C Hermite IBP) | **DISCHARGED 2026-05-19** | GR (gemini-3.1-pro-preview 2026-05-13: **Standard** post-harmonization to `ContDiff ℝ ∞`, recommended the Cameron–Martin kernel route and confirmed no mixed-derivative control is needed). **Discharged 2026-05-19 (Workstream N1.b)** by Claude via the vetted Cameron–Martin kernel route: `cameronMartin1D` (1D Girsanov shift, no integrability hypotheses) → `gaussianFin_cameronMartin` (multivariate tensorization by induction on `n` via `integral_γFin_succAbove`) → `ouSemigroupFin_eq_cmKernel` (move all spatial dependence onto a smooth Gaussian weight) → `contDiff_laplaceFamily` (C^∞ of `x ↦ ∫ F(w)·exp(α⟨x,w⟩) dγ` by `contDiff_succ_iff_fderiv` strong induction, deliberately avoiding `iteratedFDeriv`) → `contDiff_ouSemigroupFin_of_bounded`. The `IsCoreFin` bounds reuse `ouSemigroupFin_preserves_core_bounds`; the section-wise 2nd-derivative bound is transferred via `secondPartial_eq_section_deriv_of_contDiff`. No new axioms, no sorries. Verified `#print axioms GaussianFin.ouSemigroupFin_preserves_IsCore = [propext, Classical.choice, Quot.sound]`. | The `IsCore_semigroup` field of the BE-instance wrap `stdGaussianFin.bakryEmerySpace`. Downstream: same as for the other two GaussianFin axioms — eventual gaussian-hilbert `ouSemigroupAct_eLpNorm_hypercontractive` discharge. |
| `ouSemigroupFin_entropy_sq_decay_bound` | [`Instances/WorkInProgress/EuclideanFin.lean`](../MarkovSemigroups/Instances/WorkInProgress/EuclideanFin.lean) (a `theorem`) | Bakry-Gentil-Ledoux Theorem 5.5.2 / BGL §5.5 (1D analogue was historically axiomatized at `Euclidean.lean:943` and proved in commit `1b3f797` via A1+A2 decomposition) | **DISCHARGED 2026-05-19** | GR (gemini-3.1-pro-preview 2026-05-13 statement vet **Standard**; deep-think 2026-05-19 confirmed the **telescoping route**; deep-think + 3.1-pro 2026-05-19 flagged the original C∞-iterate sub-lemma as mathematically false **and vetted the corrected lower-risk 1-parameter route as SOUND** — frozen-slot decoupling, single-real-parameter differentiation under the γ-integral with a constant dominator, no joint multivariate `C²`, no mixed partials) | **Workstream N1.c, 2026-05-19 — FULLY DISCHARGED (single `sorry` closed).** `axiom` → `theorem`, axiom-free. The original "C∞-iterate / `IsCore2Fin` C²-core" plan was **superseded** by the Gemini-vetted 1-parameter route (no new core predicate needed). **Corrected architecture:** the per-coordinate step lemma `boltzmannEntropyFin_ouCoord_step_le` was refactored to slice-level hypotheses with an *abstract* slice derivative `D` (conclusion `≤ (1−e^{−2t})/2·∫ D²/g dγ`); the telescope iterates' slice-`C¹` + slice-derivative are supplied by the single-real-parameter commutation `hasDerivAt_slice_ouCoordSet` (frozen-slot identity `setShift_update_notMem`, `k∉S`) via `Mathlib.hasDerivAt_integral_of_dominated_loc_of_deriv_le` with the constant dominator (γ a probability measure); slice continuity via `continuous_of_dominated` (`continuous_ouCoordSet`). New axiom-free helpers: `section_contDiff_one`/`section_deriv_of_differentiable` (C¹ section companions), `setShift_update_notMem`, `hasDerivAt_slice_ouCoordSet`, `continuous_ouCoordSet`, `ouCoordSet_slice_contDiff_one` (S2); `cauchy_schwarz_measure` (measure-general CS), `ouCoordSet_kernel_cauchy_schwarz`, `integral_sq_div_ouCoordSet_le` (S4 orthogonal Fisher monotonicity); `boltzmann_ouCoordSet_telescope_le` (S5 `Finset.induction` telescope). Reuses the previously-proved T1 factorization (`ouCoord_ouCoordSet`, `integral_ouCoordSet_eq`, …), ε→0 DCT tail, and `sum_fisherInfoFinCoord_sq_add_const_le`. Verified `#print axioms GaussianFin.ouSemigroupFin_entropy_sq_decay_bound = [propext, Classical.choice, Quot.sound]` (no `sorryAx`, no new axioms); full `lake build` green. | The `semigroup_entropy_sq_decay_bound` field of the BE-instance wrap. Downstream: same as for the other two GaussianFin axioms — eventual gaussian-hilbert `ouSemigroupAct_eLpNorm_hypercontractive` discharge. |

### Gross-discharge: OU general textbook axioms

Added 2026-05-16/17 as the strategic unblock of the Gross-discharge
G2 chain (`plans/gross-discharge.md`): the **three** deep analytic
cruxes (Codex stalled twice on the first, twice on the third) are
promoted to **general, Mathlib-native** textbook axioms — stated with
`fderiv`/`Pi.single`/`Real.exp`/`MeasureTheory.Measure.pi`/
`ProbabilityTheory.gaussianReal`/`MemLp`/`Lp` (the third
operator-parameterized over `P` with a generic Mehler a.e.
characterization), **no project definitions** — so they are reusable
and vetting-amenable. The project lemmas
(`hasDerivWithinAt_t_ouSemigroupFin_zero`,
`ouGeneratorFin_ibp_integral`, `ouSemigroupFinLp_diffQuot_tendsto`)
are **proved theorems** discharged from these axioms by unfolding the
thin project defns / instantiating `P:=ouSemigroupFinLp` (`#print
axioms` per lemma = the 3 Lean built-ins + the one relevant axiom; no
`sorryAx`, no other custom axioms). Net for the Gross chain: the
*abstract* `gross_lsi_implies_hypercontractive` axiom leaves pphi2's
live path, replaced by concrete general Standard-vetted axioms (each
with a recorded discharge route) — conscious abstract→concrete-vetted
trade, user-approved 2026-05-17.

**Live critical path (verified after the 2026-05-22 generator discharges):**
there are now **zero** custom axioms on the concrete GaussianFin Gross chain.
`#print axioms GaussianFin.stdGaussianFin_isHypercontractive` is
`[propext, Classical.choice, Quot.sound]` only. The pointwise endpoint heat
equation `gaussianOU_heatEquation_within_zero`, Gaussian integration-by-parts
`gaussianFin_integrationByParts`, and strong-`L²` difference quotient
`gaussianFin_diffQuot_tendsto_Lp` are all theorem-level infrastructure.

| Axiom | File:Line | Reference | Rating | Vetting | Strategy / Plan | Consumers |
|---|---|---|---|---|---|---|
| `gaussianOU_heatEquation_within_zero` | [`Instances/WorkInProgress/EuclideanGeneratorLimit.lean`](../MarkovSemigroups/Instances/WorkInProgress/EuclideanGeneratorLimit.lean) | Bakry-Gentil-Ledoux *Analysis and Geometry of Markov Diffusion Operators* (2014) §2.7 (OU/heat semigroup + generator); Mehler's formula | **DISCHARGED 2026-05-22** | GR (gemini-3-pro-preview, 2026-05-16 — deep-think model unavailable, used the GR-tier model as for prior project axiom vettings). The vetted statement is now proved axiom-free: differentiate the Mehler integral for `ouSemigroupFin t f x` under the Gaussian product integral on a positive-time neighborhood using `hasDerivAt_integral_of_dominated_loc_of_deriv_le`, rewrite the time derivative through the Pi-valued chain rule and `fderiv_apply_eq_sum_partial`, then evaluate the derivative by the slicewise Stein identity `stein_partialDeriv_ouShiftFin_all` plus `section_secondDeriv_ouSemigroupFin_eq`; the endpoint `t = 0⁺` follows from `hasDerivWithinAt_Ici_of_tendsto_deriv` and pointwise `t → 0` continuity of `ouSemigroupFin`. Verified `lake build MarkovSemigroups.Instances.WorkInProgress.EuclideanGeneratorLimit`, full `lake build`, `#print axioms GaussianFin.gaussianOU_heatEquation_within_zero = [propext, Classical.choice, Quot.sound]`, and the same for `GaussianFin.hasDerivWithinAt_t_ouSemigroupFin_zero`. | Right endpoint `t=0⁺` of the Mehler-semigroup time derivative: for `C^∞` `f` with bounded `f, ∂ᵢf, ∂ᵢ²f`, `HasDerivWithinAt (t ↦ ∫ f(e^{-t}x+√(1-e^{-2t})y) d(⊗ⁿN(0,1))) (Δf(x)-x·∇f(x)) (Ici 0) 0`. This is theorem-level infrastructure with no custom axiom footprint. |
| `gaussianFin_integrationByParts` | [`Instances/WorkInProgress/EuclideanGeneratorLp.lean`](../MarkovSemigroups/Instances/WorkInProgress/EuclideanGeneratorLp.lean) | Bakry-Gentil-Ledoux (2014) §1.6/§2.7 (the OU generator's Dirichlet form: `∫ g·Lf = −E(g,f)`, `E(g,f)=∫⟨∇g,∇f⟩`); Gaussian integration by parts (Stein) | **DISCHARGED 2026-05-22** | GR (gemini-3-pro-preview, 2026-05-16; deep-think unavailable, GR-tier as for prior vettings). The vetted statement is now proved axiom-free by a coordinatewise Fubini lift of `Gaussian1D.gaussian_dirichlet_form_bilinear`: split `γFin (n+1)` along coordinate `i` via `measurePreserving_piFinSuccAbove_γFin`, identify the `insertNth` slice with `coordSection`, apply the 1D bilinear Gaussian IBP on each slice, then sum over `i`. Verified `lake build MarkovSemigroups.Instances.WorkInProgress.EuclideanGeneratorLp` and `#print axioms GaussianFin.ouGeneratorFin_ibp_integral = [propext, Classical.choice, Quot.sound]` (no `gaussianFin_integrationByParts`, no new axiom). | `GaussianFin.ouGeneratorFin_ibp_integral` and `ouGeneratorFin_ibp` are theorem-level infrastructure with no custom axiom footprint. |
| `gaussianFin_diffQuot_tendsto_Lp` | [`Instances/WorkInProgress/EuclideanGeneratorLimit.lean`](../MarkovSemigroups/Instances/WorkInProgress/EuclideanGeneratorLimit.lean) | Bakry-Gentil-Ledoux (2014) §2.7/§1.6 (OU strongly continuous on `L²(γ)`; on the smooth core `t⁻¹(Pₜf−f) → Lf` strongly in `L²`); `Lf=Δf−x·∇f` | **DISCHARGED 2026-05-22** | GR (gemini-3-pro-preview, 2026-05-17; deep-think unavailable, GR-tier as for the prior two Gross-discharge axioms). The vetted statement is now proved axiom-free by combining the endpoint pointwise heat equation with a dominated-convergence `L²` upgrade: derive the pointwise quotient limit from `hasDerivWithinAt_t_ouSemigroupFin_zero`, prove the uniform affine-in-`‖x‖₁` dominator from the positive-time derivative formula and the core bound `‖ouGeneratorFin f x‖ ≤ nM + M·∑ᵢ|xᵢ|`, then apply scalar DCT to `∫ |D_t - Lf|² dγFin` and convert the resulting `eLpNorm → 0` statement back to `Lp` convergence. Verified `lake build MarkovSemigroups.Instances.WorkInProgress.EuclideanGeneratorLimit`, full `lake build`, `#print axioms GaussianFin.gaussianFin_diffQuot_tendsto_Lp = [propext, Classical.choice, Quot.sound]`, `#print axioms GaussianFin.ouSemigroupFinLp_diffQuot_tendsto = [propext, Classical.choice, Quot.sound]`, and `#print axioms GaussianFin.stdGaussianFin_isHypercontractive = [propext, Classical.choice, Quot.sound]`. | Strong-`L²` right difference-quotient limit for the finite-dimensional Gaussian OU semigroup: for core `f`, `t⁻¹•(P_t[f]-[f]) → [Δf-x·∇f]` in `Lp ℝ 2 (⊗ⁿN(0,1))`. This is now theorem-level `GeneratorCompat` infrastructure with no custom axiom footprint; downstream consumers include `GaussianFin.ouSemigroupFinLp_diffQuot_tendsto`, `GaussianFin.ouSemigroupFin_l2_sq_hasDerivWithinAt`, and the fully axiom-free `GaussianFin.stdGaussianFin_isHypercontractive`. |

### Dobrushin-Zegarlinski

| Axiom | File:Line | Reference | Rating | Vetting | Strategy / Plan | Consumers |
|---|---|---|---|---|---|---|
| `zegarlinski_lsi_inequality` | [`DobrushinZegarlinski/GlobalLSI.lean:234`](../MarkovSemigroups/DobrushinZegarlinski/GlobalLSI.lean#L234) | Otto-Reznikoff (2007) J. Funct. Anal. 243 Theorem 1; Zegarlinski (1996) CMP 175; BGL §5.7.5 | Standard | LP | Continuous-spin generalization of the Dobrushin-Stroock-Zegarlinski-Bertini-Cancrini-Cesi LSI theorem: uniform local LSI + weak gradient coupling `J/c ≤ α < 1` ⟹ global LSI with constant `c·(1-α)`. The proof in literature is multi-page entropy iteration; full Lean discharge is estimated multi-month. | `global_lsi_of_zegarlinski` (`DobrushinZegarlinski/GlobalLSI.lean`); declared for downstream consumers (pphi2N strict thermodynamic-limit route) |
| `cov_entrywise_bound_of_zegarlinski` | [`DobrushinZegarlinski/EntrywiseCovariance.lean:146`](../MarkovSemigroups/DobrushinZegarlinski/EntrywiseCovariance.lean#L146) | Helffer-Sjöstrand (1994) J. Stat. Phys. 74; Naddaf-Spencer (1997) CMP 183; BGL §4.5 | Standard | LP | Entrywise covariance bound `|Cov(σ_x, σ_y)| ≤ M⁻¹(x,y)` for `M = Hess V` under uniform local LSI + Zegarlinski. Proof: Helffer-Sjöstrand operator-positivity argument. Multi-month to formalize (requires fairly heavy machinery for the spectral decomposition of the Hessian). | `cov_entrywise_decay_nn` (`DobrushinZegarlinski/EntrywiseCovariance.lean`, the proven exponential-decay corollary `\|Cov(σ_x, σ_y)\| ≤ α^{d(x,y)} / (c·(1-α))` for nearest-neighbor finite-range `V`); declared for pphi2N's `HSData.AdmitsThimbleLocal` |

**DZ-layer audit (verified `#print axioms` 2026-05-01):** the proven
content of `DobrushinZegarlinski/` — `AbstractInfluenceMatrix` theory,
single-site decomposition `entropy_decomposition_single_site`,
DLR-at-Bochner-integral identity `integral_siteSmoothing`, distance-aware
Neumann bounds (`iterate_dist_zero`, `neumann_series_nn_dist_bound`),
and the exponential-decay corollary `cov_entrywise_decay_nn` — is
**axiom-free** (depends only on the three Lean built-ins). Only the two
textbook axioms above are pulled in when the LSI / Cov bridge theorems
themselves are invoked.

### Matrix

| Axiom | File:Line | Reference | Rating | Vetting | Strategy / Plan | Consumers |
|---|---|---|---|---|---|---|
| `diamagnetic_resolvent` | [`Matrix/Diamagnetic.lean:57`](../MarkovSemigroups/Matrix/Diamagnetic.lean#L57) | Diamagnetic inequality (Simon, *Functional Integration and Quantum Physics*, Ch. 22); assembles 5 separate steps in the literature | Standard | LP, SA | `\|(M+iV)⁻¹(x,y)\| ≤ M⁻¹(x,y)` entrywise, where `M` is a Z-matrix and `V` is real-diagonal. Five-step assembly: (i) `(M+iV)⁻¹ = ∫₀^∞ exp(-t(M+iV)) dt`, (ii) Trotter-Lie product formula for `exp(-t(M+iV))`, (iii) `\|exp(-tM_off + tD_real)\| ≤ exp(-tM_off + tD_real)` (entrywise) for diagonally-perturbed Z-matrices, (iv) bound the Trotter slices entrywise, (v) take `n → ∞`. Estimated 3-4 weeks to formalize; (ii) and (iv) are now proved (Trotter formula in `Matrix/Trotter.lean`), so 3 of 5 steps remain. | None internally — declared for external callers (lgt's mass-gap / pphi2 propagator-bound consumers) |

**Previously axiomatized but now proved as theorems:**
- `m_matrix_inverse_nonneg` (now in `Matrix/LaplaceTransform.lean`, derived from heat-kernel positivity + Laplace transform)
- `exp_entryNonneg_of_entryNonneg` (now in `Matrix/HeatKernel.lean`, via Metzler shift)
- `trotter_product_formula` (now in `Matrix/Trotter.lean`)

## Open vetting items

These haven't been independently vetted yet — would be valuable to send
through `mcp__gemini__deep_think_gemini` and/or `codex:codex-rescue`
when the budget allows:

1. **`herbst_mgf_bound`.** Literature review only (LP). A deep-think
   pass would confirm the statement matches Herbst-style assumptions
   (no hidden `IsCore`-flavored constraints).
2. **`zegarlinski_lsi_inequality`.** Multi-page proof in the literature
   with several non-trivial sufficient-condition flavors (Otto-Reznikoff
   vs original Zegarlinski). Worth a careful side-by-side check that
   the formalized statement matches the strongest published version
   (and that the sufficient-condition `J/c ≤ α < 1` is exactly the one
   we use in `LocalLSI.lean` / `InteractionMatrix.lean`).
3. **`diamagnetic_resolvent`.** The 5-step assembly is informal — a
   deep-think pass on whether the statement is the right packaging
   (vs splitting into 5 axioms or 1 cleaner statement) would help.

## Maintenance

When adding or removing an axiom:
1. Update this file (the audit table row).
2. Update `README.md`'s axiom-count line + tables in sync.
3. If the discharge plan changes, update the `docs/<plan>.md` entry and
   re-link from the row's "Strategy / Plan" column.
4. After any new vetting pass, update the row's `Vetting` column.

When *discharging* an axiom (turning it into a proved theorem):
1. Move the row to the "Previously axiomatized but now proved" list at
   the bottom of the relevant section.
2. Update README's axiom count + audit/consumers tables.
3. Update consumers' `#print axioms` in commit messages so the audit
   trail is visible.