other22 witnesses 61 72
ProvedFreiman.other22_witnesses_61_72algebracontinued-fractionsformalization
Validate printed witnesses 61–72: exact 3×3 coefficient identity, rational radical enclosure bounds, strictness and denominator data.
Preamble
import Definitions.Def_Freiman_other22Verification import Mathlib.Tactic.FinCases import Mathlib.Tactic.SplitIfs open Freiman
Formal statement
theorem Freiman.other22_witnesses_61_72 :
other22WitnessBatch 60 72 := by
sorrySource
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.