Freiman.lowerHistory_source_choices_from_tails
ProvedFreiman.lowerHistory_source_choices_from_tailshall-raynumber-theory
Unfold the actual A/H branch tables using the fourteen exact source-tail identities.
Preamble
import Definitions.Def_Freiman_lowerHistoryVerification import Mathlib.Tactic open Freiman
Formal statement
theorem Freiman.lowerHistory_source_choices_from_tails (ht : ∀ i ∈ ([3,20,22,25,28,35,36,63,65,66,68,70,90,94] : List ℕ), certFieldVal (lowerHistoryTheta i) = lowerTheta i) :
LowerHistoryChoiceLaw := by
sorrySource
Freiman's Hall ray: Proof report and corrected English text (8 September 2026); global_selection.tex, lem:global-suffix-targets; history_certificates.tex, app:all-suffix-histories; verification/families/target_selection/verify_suffix_targets_independent.py; certificates/target_selection/all_suffix_histories_printed.json; role: source branch tables