The quadratic potential has its unique minimum at zero
AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.blockPrecision_unique_minimizer · theorem · Teaching coverage
Mathematical statement
Under the same n≥3,n≤d,kappa≥4 and orthogonal tuple assumptions, the actual potential f_A(x)=(1/2)x^T A x has f_A(0)=0, is nonnegative for every x, and equals zero if and only if x=0. Thus its unique minimizer is0 and its minimum value is0.
Lean statement · blockPrecision_unique_minimizer
Coordinates are Fin d with the exact quotient/remainder adapter; dotProduct represents the Euclidean quadratic form.
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.
theorem blockPrecision_unique_minimizer {d n : ℕ} (hn : 3 ≤ n) (hnd : n ≤ d)
{κ : ℝ} (hκ : 4 ≤ κ)
(O : Fin (d / n) → Matrix.orthogonalGroup (Fin n) ℝ) :
let f : (Fin d → ℝ) → ℝ := fun x => (1 / 2 : ℝ) * (x ⬝ᵥ (blockPrecision κ O *ᵥ x))
f 0 = 0 ∧ ∀ x, 0 ≤ f x ∧ (f x = 0 ↔ x = 0)Proof roadmap
- 1The origin has value zero
The literal quadratic expression vanishes at the zero vector.
- 2The lower spectral bound gives nonnegativity
Apply the actual full-precision theorem to the same x. Since its coordinate squared sum is nonnegative, so is the potential.
- 3Zero energy forces every coordinate to vanish
If f_A(x)=0, the lower bound forces the sum of squared coordinates to be0. Each nonnegative summand is at most this sum, hence each coordinate is0. Conversely x=0 has zero energy. Combined with nonnegativity, this gives strict positivity for x≠0 and the unique minimum.
Full assumptions and notation
All objects and hypotheses
- d and n are natural dimensions; kappa is a real number.
- n≥3, n≤d and kappa≥4 are the source standing range.
- O is a tuple indexed by Fin(d/n), with each matrix in the full real orthogonal group on Fin n.
Mathematical proof
1. The origin has value zero
The literal quadratic expression vanishes at the zero vector.
Corresponding Lean step
The first conjunct unfolds the displayed potential and simplifies zero matrix-vector and dot products.
2. The lower spectral bound gives nonnegativity
Apply the actual full-precision theorem to the same x. Since its coordinate squared sum is nonnegative, so is the potential.
Corresponding Lean step
hlow is produced by blockPrecision_regular, with the same hn,hnd,hκ and O. hnonneg is the finite sum of coordinate squares.
3. Zero energy forces every coordinate to vanish
If f_A(x)=0, the lower bound forces the sum of squared coordinates to be0. Each nonnegative summand is at most this sum, hence each coordinate is0. Conversely x=0 has zero energy. Combined with nonnegativity, this gives strict positivity for x≠0 and the unique minimum.
Corresponding Lean step
The proof uses Finset.single_le_sum and mul_self_eq_zero. The theorem packages nonnegativity and the exact zero set; this is equivalent to the source unique-minimizer conclusion.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · blockPrecision_unique_minimizer
The adjacent checked Lean body supplies the actual matrix assembly and all internal dependencies.
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.
theorem blockPrecision_unique_minimizer {d n : ℕ} (hn : 3 ≤ n) (hnd : n ≤ d)
{κ : ℝ} (hκ : 4 ≤ κ)
(O : Fin (d / n) → Matrix.orthogonalGroup (Fin n) ℝ) :
let f : (Fin d → ℝ) → ℝ := fun x => (1 / 2 : ℝ) * (x ⬝ᵥ (blockPrecision κ O *ᵥ x))
f 0 = 0 ∧ ∀ x, 0 ≤ f x ∧ (f x = 0 ↔ x = 0) := by
dsimp
constructor
· simp
intro x
have hlow := ((blockPrecision_regular hn hnd hκ O).2 x).1
have hnonneg : 0 ≤ x ⬝ᵥ x :=
Finset.sum_nonneg (fun i _ => mul_self_nonneg (x i))
constructor
· nlinarith
constructor
· intro h
have hzero : x ⬝ᵥ x = 0 := by nlinarith
ext i
change x i = 0
have hi := Finset.single_le_sum (fun j (_ : j ∈ (Finset.univ : Finset (Fin d))) =>
mul_self_nonneg (x j)) (Finset.mem_univ i)
change x i * x i ≤ x ⬝ᵥ x at hi
rw [hzero] at hi
exact mul_self_eq_zero.mp (le_antisymm hi (mul_self_nonneg (x i)))
· intro h
subst x
simp
end AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamilySource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| n>=3,n<=d,kappa>=4; k=floor(d/n); residual d-k*n. | The theorem retains n>=3,n<=d,kappa>=4; Fin(d/n) blocks and Fin(d%n) residual, with contiguous coordinate equivalence. | same | Euclidean division identifies d%n with d-k*n. Real Hermitianity and universal dot-product bounds express source symmetry and Loewner bounds; no Pi norm or entrywise matrix order is used. |
| Unique minimizer0 and minimum value0; strict positivity for nonzero x. | Value0 at0, nonnegativity at every x, and zero value iff x=0. | same | Over the reals, nonnegativity and the exact zero set imply positivity off0 and the same unique minimum. The potential is the actual displayed quadratic form, not an unspecified objective. |
Only determinant-family regularity and the quadratic minimum in Lemma3.4/B.8. Gaussian normalization, Haar posterior laws, oracle indistinguishability, test separation and both main complexity lower bounds remain open.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- conclusion: The unique-minimum assertion is expressed by the equivalent nonnegativity, value-at-origin and exact-zero-set conditions. — For real-valued f these conditions are logically equivalent to the source assertion; the definition is the actual quadratic potential, not an abstract supplied function.
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
- Only determinant-family regularity and the quadratic minimum in Lemma3.4/B.8. Gaussian normalization, Haar posterior laws, oracle indistinguishability, test separation and both main complexity lower bounds remain open.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.blockPrecisionAutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.blockPrecision_regular
Mathlib API called (external library)
- Finset.single_le_sum
- mul_self_eq_zero
Mathematical sources
- Source block family and full regularity lemma — Literal equation(5), block quadratic bounds and unique minimum only.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.