Freiman §14: section14 record from pair

Proved

Freiman.section14_record_from_pair

by tp · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-certificatesfreimanhall-raysection14

Generic record semantics: its two cited premises contradict the shared Bernstein witness on an enclosing rectangle. This is a finite-list/index and interval-containment argument; its numerical input is exactly cert_witness_excludes.

Preamble

import Definitions.Def_Freiman_section14Geometry
import Mathlib.Tactic.FinCases

open Freiman

Formal statement

theorem Freiman.section14_record_from_pair (hw : ∀ w : CertWitness, certWitnessValid w → ∀ r s q : ℝ, certRectangleMem w.rectangle r s → ¬ (certBoundHolds w.lowerBound r s q ∧ certBoundHolds w.upperBound r s q)) : ∀ (C : Section14Catalog) (si : ℕ) (rec : Section14Record), section14RecordValid C si rec → section14RecordSound C si rec := by
  sorry

Source

Freiman report, active §14; Appendix Complete finite certificates for the scalar geometry of §14; full_readable_model.json.

View graph