Freiman p97: finite transfer

Proved

Freiman.lower_h5_finite_transfer

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

certificatesfreimanp97

Logical application of the finite ledger: append the negated endpoint goal to the reconstructed premises, exclude all89 recorded residuals, retain only automatic comparisons and explicitly named branch5 priority alternatives. Complements retain strictness.

Preamble

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

open Freiman

Formal statement

theorem Freiman.lower_h5_finite_transfer (hex : ∀ (c : LowerH5Case) (record : LowerH5Record), LowerH5RecordBinding c record →
      certWitnessValid (lowerH5Witness record.witness) → ∀ r s q : ℝ,
      certRectangleMem c.rectangle r s → lowerHistoryConditions (lowerH5RecordBounds record) r s q → False) (hb : lowerH5AllBindings) (hw : lowerH5AllWitnesses) :
    ∀ c ∈ lowerH5Cases, lowerH5Numeric c := 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