Freiman.lowerHistory_bindings_0000_0050

Proved

Freiman.lowerHistory_bindings_0000_0050

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

hall-raynumber-theory

Exact DNF/residual/witness membership and complete alternative/endpoint inventory for path-array entries 0..49.

Preamble

import Definitions.Def_Freiman_lowerHistoryVerification
import Mathlib.Tactic

open Freiman

Formal statement

theorem Freiman.lowerHistory_bindings_0000_0050 :
    lowerHistoryBindingBatch 0 50 := by
  sorry

Source

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: all_suffix_histories_printed.json: paths/records

View graph