Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite Li Curvature Reconstruction

Abstract

Normalized Hermitian second differences reconstruct finite Toeplitz quadratic forms, with a smallest-eigenvalue obstruction and a two-point absolute growth bound.

Throughout, T(c,n) has row and column indices in Fin(n), and e(n) is the complex all-ones vector on the same type. Both indices are cast to integers before subtraction.

Ico(1,n) is the natural interval from one inclusive to n exclusive. Real and Int in the formulas denote casts; NatSub is truncated natural subtraction. For positive n, last(n) is the element of Fin(card(Fin(n))) with value n minus one. The eigenvaluesZero enumeration is Mathlib’s descending eigenvalues enumeration.

Theorem 1.1 (Weighted curvature reconstruction).

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/LiCurvatureFiniteReconstruction.recurrence_eq_weighted_curvature_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

The repository’s second_difference_recurrence_unique is applied to the displayed candidate sequence. Mathlib’s finite interval extension identities verify its initial values and second differences. This is the finite algebraic reconstruction, including zero and one and without division by L.

Theorem 1.2 (Signed finite diagonal count).

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/LiCurvatureFiniteReconstruction.toeplitz_ones_diagonal_count (✓ std3). ∎

Source. Repository-derived.

Commentary.

Mathlib’s interval Fubini and reflection identities split the square into its diagonal and two strict triangles. Each signed gap has n minus k entries. The identity requires neither Hermitian symmetry nor normalization, and retains both complex coefficients before taking real parts.

Theorem 1.3 (The actual size-n quadratic form).

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/LiCurvatureFiniteReconstruction.recurrence_eq_toeplitz_ones_quadratic (✓ std3). ∎

Source. Repository-derived.

Commentary.

Weighted reconstruction and the signed count give this sequence-to-matrix identity. Conjugation and c(0)=1 give its real part. The existing toeplitzMatrix(c,n-1) is transported through the value-preserving equivalence Fin(n-1+1) to Fin(n); the submatrix and dot-product equivalence theorems also transport the all-ones vector. No measure representation is a premise.

Theorem 1.4 (Full Toeplitz positivity).

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/LiCurvatureFiniteReconstruction.recurrence_nonneg_of_toeplitz_posSemidef (✓ std3). ∎

Source. Repository-derived.

Commentary.

The preceding quadratic identity and Mathlib’s PosSemidef.re_dotProduct_nonneg give the nonnegative coefficient for every positive size. The prescribed initial value supplies size zero.

Theorem 1.5 (A negative spectral obstruction).

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/LiCurvatureFiniteReconstruction.negative_recurrence_bounds_smallest_eigenvalue (✓ std3). ∎

Source. Repository-derived.

Commentary.

The classical finite-dimensional Rayleigh infimum theorem is supplied by Mathlib’s hasEigenvalue_iInf_of_finiteDimensional. The public eigenvalue enumeration and its antitonicity put the last eigenvalue below that infimum. Evaluation uses WithLp.toLp(2,e(n)), whose squared Euclidean norm is n and which is nonzero. Conjugate symmetry identifies the real numerator with the preceding quadratic identity. Strict positivity of n times L gives the second inequality.

Theorem 1.6 (Two-point absolute bound).

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/LiCurvatureFiniteReconstruction.two_point_posSemidef_abs_recurrence_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Only injective two-point principal compressions are assumed positive. Selecting indices zero and k in the block of size k+1 gives determinant one minus the squared complex norm of c(k). Mathlib’s determinant nonnegativity and two-by-two determinant formula bound that norm by one. The repository’s quadratic_of_bounded_second_difference then supplies the absolute growth bound. Mathlib’s finite Gauss identity evaluates the displayed sum, also at zero and one. Full-matrix positivity is not needed for this bound.

References