Freiman §14: section14 row modes

Proved

Freiman.section14_row_modes

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

finite-certificatesfreimanhall-raysection14

The seven exact source cuts and two natural suffix flags select one of the printed nine rows. H17 and H21 retain their exact tail-difference ratios. The shortened-left H5 row deliberately carries no lower-parent anchor.

Preamble

import Definitions.Def_Freiman_section14Geometry
import Mathlib.Tactic.FinCases

open Freiman

Formal statement

theorem Freiman.section14_row_modes (p : LowerPair) (i : Fin 16) (hm : lowerMixed p)
    (hmatch : section14Matches p (section14State section14Catalog (i.val+1))) :
    ∃ pl ∈ (section14State section14Catalog (i.val+1)).plans,
      pl.labels = section14RawList p ∧ pl.targetLower = section14TargetLower p ∧
      section14Holds (section14Case section14Catalog pl.caseId) (section14R p) (section14S p) (section14Q p) := by
  sorry

Source

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

View graph