other22 endpoint inventory

Proved

Freiman.other22_endpoint_inventory

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

algebracontinued-fractionsformalization

The row1 comparison inventory is exactly the earlier32/base endpoint against the residual upper endpoint at relative words (221,312). No endpoint swap equality is asserted.

Preamble

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

open Freiman

Formal statement

theorem Freiman.other22_endpoint_inventory :
    ∀ k : Fin 6, lowerHistoryEndpointComparisons (other22Paths k) =
    lowerHistoryComparisons (other22Context k) (other22Ancestor k) other22ResidualWords (other22AncestorUpper k) false := 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