Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

For every real kappa and phase point, define the exact source block-matrix quadratic form Q_kappa

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang. Exact source numerical phase/metric, explicit constant elaboration, actual normalized-curvature producer boundary.

arXiv:2609.06906v1 · Proposition4.7 HTML590-620; exact M_kappa display preceding Theorem4.5 · faithful paraphrase

Complete source statement (Samplinglib restatement)

For every real kappa and phase point, define the exact source block-matrix quadratic form Q_kappa. Valid norm use is restricted to kappa>=1 by the compiled comparisons.

  • Arbitrary real inner-product E, with no finite-dimension or measurability premise. Kappa>=1 for the comparisons; the total definition accepts every real kappa.

Exact source metric/actual contraction

\[Q_\kappa(x,p)=\left(\frac1{2\kappa}+\frac12\right)\|x\|^2+\langle x,p\rangle+\|p\|^2.\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

For every real kappa and phase point, define the exact source block-matrix quadratic form Q_kappa

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric.phaseQuadraticForm · def · Teaching coverage

Read this first

Mathematical statement

For every real kappa and phase point, define the exact source block-matrix quadratic form Q_kappa. Valid norm use is restricted to kappa≥1 by the compiled comparisons.

\[Q_\kappa(x,p)=\left(\frac1{2\kappa}+\frac12\right)\|x\|^2+\langle x,p\rangle+\|p\|^2.\]
Lean statement · phaseQuadraticForm

For every real kappa and phase point, define the exact source block-matrix quadratic form Q_kappa. Valid norm use is restricted to kappa>=1 by the compiled comparisons.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
def phaseQuadraticForm (kappa : ℝ) (z : E × E) : ℝ

Exact module and namespace context

Proof roadmap

  1. 1Evaluate the source block matrix

    Both off-diagonal entries are1/2, so their sum is the cross inner product. This reuses the existing definition unchanged; public visibility enables the actual numerical contraction consumer.

Full assumptions and notation

All objects and hypotheses

  • Arbitrary real inner-product E, with no finite-dimension or measurability premise. Kappa≥1 for the comparisons; the total definition accepts every real kappa.

Construction and meaning

1. Evaluate the source block matrix

Both off-diagonal entries are1/2, so their sum is the cross inner product. This reuses the existing definition unchanged; public visibility enables the actual numerical contraction consumer.

\[\tfrac12\langle x,p\rangle+\tfrac12\langle p,x\rangle=\langle x,p\rangle.\]
Corresponding Lean step

phaseQuadraticForm

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean construction · phaseQuadraticForm

Exact source form and compiled parent composition, with all source domains/constant absorption and zero cases explicit. Existing Q/comparison proofs unchanged.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
def phaseQuadraticForm (kappa : ℝ) (z : E × E) : ℝ :=
  (1 / (2 * kappa) + 1 / 2) * ‖z.1‖ ^ 2 + inner ℝ z.1 z.2 + ‖z.2‖ ^ 2

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Finite Euclidean source domain with the exact M_kappa block form.Arbitrary real inner-product E, with no finite-dimension or measurability premise. Kappa>=1 for the comparisons; the total definition accepts every real kappa.generalizationReal inner-product presentation preserves the exact source form. Background comparisons need neither finite dimension nor measurable structure; nonlinear algorithm uses complete finite E and BorelSpace.
Universal c and C in the source Proposition4.7 step/contraction.For every real kappa and phase point, define the exact source block-matrix quadratic form Q_kappa. Valid norm use is restricted to kappa>=1 by the compiled comparisons.source-implicitExplicit conservative c=1/65536 is proved using the actual C8 algorithm remainder and source drift. Q/API definitions and comparison proofs are unchanged, with no extra completed-paper credit.
Actual V_eta from Lemma4.1.Genuine global C2 f with explicit normalized curvature for the nonlinear consumer.unresolvedThe source smoothing/C2/curvature producer must be joined before claiming Proposition4.7 at V_eta or the full main result. Definitions and energy comparisons are already exact and independent of that producer.

Existing source Q/API promotion with unchanged proof, no separate mathematical progress credit. Actual deterministic exact-gradient numerical phase contraction at the explicit normalized C2 curvature interface. Actual f=V_eta smoothing/C2/curvature producer remains independently open. No Khat/Kbar substitution, increment/logLambda/B2, invariant law/local errors/history/query work, PBPS, either full main theorem or actual-input expected-cost composition. TV proximity does not transfer unbounded expected cost.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries
  • Existing source Q/API promotion with unchanged proof, no separate mathematical progress credit. Actual deterministic exact-gradient numerical phase contraction at the explicit normalized C2 curvature interface. Actual f=V_eta smoothing/C2/curvature producer remains independently open. No Khat/Kbar substitution, increment/logLambda/B2, invariant law/local errors/history/query work, PBPS, either full main theorem or actual-input expected-cost composition. TV proximity does not transfer unbounded expected cost.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    No direct Mathlib call recorded; see the Samplinglib parents.

    Mathematical sources

    • SPHMC actual numerical contraction and M_kappa — Existing source Q/API promotion with unchanged proof, no separate mathematical progress credit. Actual deterministic exact-gradient numerical phase contraction at the explicit normalized C2 curvature interface. Actual f=V_eta smoothing/C2/curvature producer remains independently open. No Khat/Kbar substitution, increment/logLambda/B2, invariant law/local errors/history/query work, PBPS, either full main theorem or actual-input expected-cost composition. TV proximity does not transfer unbounded expected cost.

    Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

    Which proof obligations and prerequisites are covered?

    • Independently verified prerequisite For every real kappa and phase point, define the exact source block-matrix quadratic form Q_kappa. Valid norm use is restricted to kappa>=1 by the compiled comparisons.
    • TODO — not closed by these contributions Actual smoothed potential and full main result (remaining)