lower late anchor goodness

Open

Freiman.lower_late_anchor_goodness

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

algebracontinued-fractionsformalization

Both inherited anchor covers are good by their own explicit strict-goodness records in the original trunk table.

Preamble

import Definitions.Def_Freiman_lowerCertificates

open Freiman

Formal statement

theorem Freiman.lower_late_anchor_goodness (t : ℝ) (p : LowerPair) (hs : lowerState t p)
    (hd : ¬ lowerMixed p ∧ ¬ lowerA p 3 ∧ ¬ lowerA p 9 ∧ lowerL p ∧ ¬ lowerLStar p) :
    lowerGood (lowerChild p ([2],[2])) ∧ lowerGood (lowerChild p ([2],[1])) := 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