Freiman lower construction: entry child extends
ProvedFreiman.lower_entry_child_extendsfreimanlower-construction
Finite six-label physical extension check at an already normalized incoming parent.
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_child_extends (p : LowerPair) (hn : lowerNormalize p = p) (l : LowerLabel) (hl : l ∈ lowerEntryLabels) : lowerExtends p (lowerChild p l) := 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