Freiman.lowerEarlyTerminal_parameter_h7
ProvedFreiman.lowerEarlyTerminal_parameter_h7hall-raynumber-theory
Identify this exact four-coordinate field threshold with the unchanged lowerA test, including its weak/strict direction.
Preamble
import Definitions.Def_Freiman_lowerEarlyTerminalGeometry open Freiman
Formal statement
theorem Freiman.lowerEarlyTerminal_parameter_h7 (p : LowerPair) : lowerEarlyTerminalAt p [lowerEarlyTerminalH7] ↔ ¬ lowerA p 3 := by sorry
Source
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), pp.120–132, §§ s15:early-residual and s15:terminal-extension; pp.133–139, Proposition l139chain and Appendix app:l139cert. Source constants in independent_residual.py, independent_extensions.py, verify_independent.py; report threshold table and scalar tests.