Freiman late: mixed virtual-upper selected-mode identity

Proved

Freiman.late_mixed_virtual_endpoint_from_width_cf

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

finite-certificatesfreimanhall-raylate

This is the virtual-upper case of the mixed-parity late endpoint identity. For a matching cover and a recorded late endpoint whose outward words have opposite length parity, write $w$ for the strictly wider physical side after appending those words to the normalized cover, or the left side in a width tie. If the requested endpoint direction equals the virtual-upper choice of $w$ — equivalently, if that side is even-length after the odd-left sign — then every selected mode whose bounds hold reconstructs the actual continued-fraction endpoint by extending $w$ by a virtual digit $1$ and reducing to an equal-parity source case. Strict complementary width tests select a unique orientation.

\mathrm{lateActualEndpoint}(p,e)=\mathrm{lateActualValue}(p,e).

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_endpoint_from_width_cf (hcf : ∀ (w : List ℕ+) (z : CertField), 0 ≤ certFieldVal z → certFieldVal (lowerHistoryCF w z) = prefixEval w (certFieldVal z)) (hw : LowerHistoryWidthLaw) (p : LowerPair) (e : LateEndpoint) (hm : lateMatches p e.right3) (hne1 : e.words.1 ≠ []) (hne2 : e.words.2 ≠ []) (hv : lateEndpointValid lateCatalog e) (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)))) : ∀ ids ∈ e.modes, lateHolds (lateBounds lateCatalog ids) (lateR p) (lateS p) (lateQ p) → lateActualEndpoint p e.words e.upper = lateActualValue p e.value := by
  sorry

Source

Freiman report, §15, printed source pages 140–144; restriction of Freiman.late_mixed_endpoint_from_width_cf to the virtual-upper branch of the mixed source list.

View graph