Freiman marked initial bridges: strip bounds

Proved

Freiman.lower_bridge_strip_bounds

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

certificatesfreimanlower-construction

The two outer strip contacts enclose the actual parity-dependent missing H strip between endpoint values of the bridge chain.

Preamble

import Definitions.Def_Freiman_lowerBridgeCatalog
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Push

open Freiman

Formal statement

theorem Freiman.lower_bridge_strip_bounds (c : LowerBridgeCase) (n : ℕ) (hc : lowerBridgeZero c = decide (n=0)) (hf : lowerBridgeFamily c ≠ .C) (h : lowerBridgeFacts c n 0) (he : lowerBridgeEndpointFacts c n 0) : ∀ t ∈ lowerBridgeInterval (lowerBridgeFamily c) n 0 0, ∃ a ∈ lowerBridgeLabels (lowerBridgeFamily c) n, ∃ b ∈ lowerBridgeLabels (lowerBridgeFamily c) n, lowerEndpoint (lowerPhysicalAdd (lowerFamilyPair (lowerBridgeFamily c) n 0 0) a) false ≤ t ∧ t ≤ lowerEndpoint (lowerPhysicalAdd (lowerFamilyPair (lowerBridgeFamily c) n 0 0) b) true := by
  sorry

Source

Freiman report, initial_bridges.tex, corrected marked H entries; H_entry_bridges.json 185 exact polynomial records.

View graph