# `mehler_kernel.lean` — Informal Summary

> **Source**: [`future/mehler_kernel.lean`](../../future/mehler_kernel.lean)
> **Generated**: 2026-03-10
> **Note**: Auto-generated by `/lean-summarize`. Re-run to refresh.

## Overview

Documentation-only file parking the `mehlerKernel_eq_series` axiom as a future proof
target. The axiom remains in `HeatKernel/PositionKernel.lean` (off the main build path)
and is only used by the cylinder QFT heat kernel, not by the lattice approach used by pphi2.

## Status

**Main result**: N/A (documentation only, no Lean declarations)

**Length**: 83 lines, 0 definition(s) + 0 theorem(s)/lemma(s)

---

## Future proof target

### `mehlerKernel_eq_series`

**Statement**: The Mehler kernel (closed-form heat kernel of $H = -d^2/dx^2 + x^2$) equals
its Hermite eigenfunction expansion:
$$K_{\text{Mehler}}(t, x_1, x_2) = \sum_{n=0}^\infty e^{-t(2n+1)}\,\psi_n(x_1)\,\psi_n(x_2)$$
where $\psi_n$ are the $L^2$-normalized Hermite functions.

**Approach A**: Generating function identity for Hermite polynomials — write both sides as
power series in $r = e^{-2t}$ and match coefficients. Key identity:
$$\sum_n \frac{r^n H_n(x) H_n(y)}{2^n n!} = (1-r^2)^{-1/2} \exp\!\bigl(\tfrac{2rxy}{1+r} - \tfrac{r^2(x^2+y^2)}{1-r^2}\bigr)$$

**Approach B**: Heat equation uniqueness — show both sides satisfy $\partial_t K = -HK$ with
$K(0, x_1, x_2) = \delta(x_1 - x_2)$.

**Key blocker**: Generating function for Hermite polynomials (not in Mathlib).
Estimated ~400–700 LOC.

**Dependents**: 6 proofs in `HeatKernel/PositionKernel.lean` (eigenfunction reproduction,
semigroup property, cylinder kernel series). All on the cylinder QFT path.

---

*This is a documentation-only file with no Lean declarations.*