trunk boundary corner contradiction

Proved

Freiman.trunk_boundary_corner_contradiction

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

algebracontinued-fractionsformalization

The touching rectangle edges and r=s force the unique common corner; H0 then equals1. An actually present source lower bound has positive numerator-minus-denominator at that corner, so its threshold exceeds1 and contradicts q≤1. This is exact evaluation of an existing source threshold, not a new polynomial.

Preamble

import Definitions.Def_Freiman_trunkGeometry
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.Linarith

open Freiman

Formal statement

theorem Freiman.trunk_boundary_corner_contradiction (R : CertRectangle) (bs : List CertBound) (hb : trunkBoundaryBound R bs)
    (r s q : ℝ) (hm : certRectangleMem R r s) (hrs : r = s) (h : trunkHolds bs r s q) :
    False := by
  sorry

Source

Report Proposition4.1 s15:trunk, printed report p28; original source pp120–126. Complete sixteen-state trunk certificate,58230 records,90 case plans, with three explicitly unfilled interfaces.

View graph