other22 anchor represented

Proved

Freiman.other22_anchor_represented

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

algebracontinued-fractionsformalization

Expand the actual earlier32 upper endpoint (or birth lower endpoint when the old left ends31) into one of the source endpoint cases, with true case conditions and nonnegative exact tails.

Preamble

import Definitions.Def_Freiman_other22Verification
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.SplitIfs

open Freiman

Formal statement

theorem Freiman.other22_anchor_represented (Z B R S : LowerPair) (h : LowerOther22Geometry Z B R S) (k : Fin 6) (hc : lowerHistoryContextFits Z (other22Context k)) :
    other22EndpointRepresented Z (other22Context k) (other22Ancestor k) (other22AncestorUpper k) (other22AnchorValue Z) := by
  sorry

Source

Report §7.3, Lemma 7.4 (lem:old23-other22-target), printed p.43; other22_target.tex and Appendix other22_certificates.tex; original 144-obligation exact certificate.

View graph