Freiman lower construction: entry core arithmetic threeOdd

Proved

Freiman.lower_entry_core_arithmetic_threeOdd

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

freimanlower-construction

All 23 exact source core endpoint comparisons for terminal class threeOdd. Every upper/lower word, equality flag and parity is concrete in lowerInitialEntry. After clearing denominators the goal is a grouped finite biquadratic inequality on the printed closed rational r,s,q box; source tables supply Bernstein witnesses. No history or unbounded family remains in this leaf.

Preamble

import Definitions.Def_Freiman_lowerInitialEntry
import Definitions.Def_Freiman_lowerCertificates
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Push

open Freiman

Formal statement

theorem Freiman.lower_entry_core_arithmetic_threeOdd : ∀ e ∈ lowerEntryCoreRows .threeOdd, lowerEntryRowValid e := by
  sorry

Source

Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/lower_core.tex, prop:lc-H-entry; source H certificate appendix

View graph