Freiman p97: initial fixed

Proved

Freiman.lower_h5_initial_fixed

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

certificatesfreimanp97

The 23 actual fixed roots have no mixed shortened-left state, checking both strict normalization possibilities without equal-width swap invariance.

Preamble

import Definitions.Def_Freiman_lowerH5Verification
import Definitions.Def_Freiman_lowerInitialEntry
import Mathlib.Tactic

open Freiman

Formal statement

theorem Freiman.lower_h5_initial_fixed (p : LowerPair) (hp : p ∈ lowerFixedRoots) : ¬(lowerMixed p ∧ lowerL p) := by
  sorry

Source

Freiman report, 'The carried target in the shortened-left case of Section 14', sec:h5-source-target, Lemma lem:h5-original-two (source printed p. 97), report/source/staging/parts/h5_target.tex; global_selection.tex priority rule; certificates/target_selection/h5_cases.json and h5_original_appendix_printed.json; verification/families/target_selection/verify_h5_original_independent.py.

View graph