Freiman M2B certificate: cert diagonal bilinear interpolation
ProvedFreiman.cert_diagonal_bilinear_interpolationfinite-certificatesfreimanhall-raymiddle
A bilinear polynomial with nonnegative four corners is nonnegative throughout the full closed rectangle, including its boundary.
Preamble
import Definitions.Def_Freiman_certDiagonal open Freiman
Formal statement
theorem Freiman.cert_diagonal_bilinear_interpolation :
∀ (w : CertDiagonalData), certDiagonalDataValid w → (∀ i j : Fin 2, 0 ≤ certFieldVal (w.corners i j)) → ∀ r s : ℝ, certRectangleMem w.rectangle r s → 0 ≤ (if w.positiveDirection then (1:ℝ) else -1)*certDiagonalFactor w.a w.b w.c r s := by
sorrySource
Freiman report (8 September 2026), M2B §§8–9 and complete middle-interval certificate appendix; m2b_readable_model.json, SHA256 a5ac6d3c8e0148e2e3137e8cfa09a2715de6a993dd6ab01eda4842a96bba4cdf.