Source cone admissibility
Abstract
Compact source data satisfy eventual positive definiteness of the cone matrix.
Theorem 1.1 (Equation eleven gap).
Lean statement: D5/S3/FluidDynamics/Cone/SourceConeAdmissibility.compact_equation_eleven_gap
Proof. Machine-checked in Lean as D5/S3/FluidDynamics/Cone/SourceConeAdmissibility.compact_equation_eleven_gap (✓ std3). ∎
Source. Repository-derived.
Commentary.
The strict source criterion yields uniform relaxed cone inequalities above one amplitude threshold.
Theorem 1.2 (Source derived matrix positivity).
Lean statement: D5/S3/FluidDynamics/Cone/SourceConeAdmissibility.compact_source_coneMatrix_posDef
Proof. Machine-checked in Lean as D5/S3/FluidDynamics/Cone/SourceConeAdmissibility.compact_source_coneMatrix_posDef (✓ std3). ∎
Source. Repository-derived.
Commentary.
For compact continuous source data and an explicit lower bound on the matrix parameter, all sufficiently large amplitudes give positive definite cone matrices.