Prove2Me

other22 path shapes

Proved
Freiman.other22_path_shapes

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

algebracontinued-fractionsformalization

The six fixed descriptor records encode precisely Z→23→20(reflect)→10(no reflection), final row1 and the original suffix contexts; this finite structural check supplies the generic source-DNF induction.

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

open Freiman
Formal statement
theorem Freiman.other22_path_shapes :
    ∀ k : Fin 6, lowerHistoryStructural (other22Paths k) := 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