other22 witnesses 85 92
ProvedFreiman.other22_witnesses_85_92algebracontinued-fractionsformalization
Validate printed witnesses 85–92: 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_85_92 :
other22WitnessBatch 84 92 := 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.