Freiman lower construction: entry aux matrix

Proved

Freiman.lower_entry_aux_matrix

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

freimanlower-construction

Auxiliary B has period exponent n+1, no zero-period case and no run parameter. This identity is for the raw displayed words; actual normalization is proved separately from the parameter domain.

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_aux_matrix 
    (hp : ∀ n : ℕ, 0 < n → lowerInitialWordMatrix (lowerRepeat lowerPeriod n) =
      lowerInitialMatScale (lowerInitialU n:ℝ) (lowerInitialP false (lowerInitialX n)))
    (hu : ∀ n : ℕ, 0 < n → 0 < lowerInitialU n)
    (n k p : ℕ) :
    ∃ a : ℝ, 0 < a ∧
      lowerInitialWordMatrix (lowerFamilyPair .auxB n k p).1 =
        lowerInitialMatScale a (lowerEntryAuxMatrices (lowerInitialX (n+1))).1 ∧
      lowerInitialWordMatrix (lowerFamilyPair .auxB n k p).2 =
        lowerInitialMatScale a (lowerEntryAuxMatrices (lowerInitialX (n+1))).2 := 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