Freiman late: mixed virtual-upper holding case unique

Proved

Freiman.late_mixed_virtual_holding_unique

by Koki Yamada · Sep 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-certificatesfreimanhall-raylate

In the mixed-parity virtual-upper case, at most one source case holds at a matching cover. Complementary width tests cannot both hold, so the orientation is unique; the inner equal-parity family of the virtual pair is then unique by the $7/5$ cut versus its complement. Consequently any two holding members of the mixed source list have the same recorded tails.

(z,cs),\ (z',cs')\ \text{hold}\quad\Longrightarrow\quad z=z'.

Preamble

import Definitions.Def_Freiman_lateGeometry
import Mathlib.Tactic

set_option maxRecDepth 8000
set_option maxHeartbeats 0

open Freiman

Formal statement

theorem Freiman.late_mixed_virtual_holding_unique (hw : LowerHistoryWidthLaw) (p : LowerPair) (e : LateEndpoint) (hm : lateMatches p e.right3) (hp : lowerHistoryWordParity (lateContext e.right3) e.words false ≠ lowerHistoryWordParity (lateContext e.right3) e.words true) (hvirt : e.upper = ! lowerHistoryWordParity (lateContext e.right3) e.words (decide (¬ lowerWidth ((lowerNormalize p).2 ++ e.words.2) ≤ lowerWidth ((lowerNormalize p).1 ++ e.words.1)))) (z z' : CertField × CertField) (cs cs' : List CertBound) (h : (z, cs) ∈ lateEndpointCases e.right3 e.words e.upper) (h' : (z', cs') ∈ lateEndpointCases e.right3 e.words e.upper) (hat : lowerHistoryAtBase (lowerNormalize p) cs) (hat' : lowerHistoryAtBase (lowerNormalize p) cs') : z = z' := by
  sorry

Source

Freiman report, §15, printed source pages 140–144; uniqueness half of Freiman.late_mixed_virtual_endpoint_from_width_cf.

View graph