Freiman marked initial bridges: binding bZero
ProvedFreiman.lower_bridge_binding_bZerocertificatesfreimanlower-construction
Finite exact coefficient identities for the actual bZero matrix widths, cuts and contacts.
Preamble
import Definitions.Def_Freiman_lowerBridgeCatalog import Mathlib.Tactic.Linarith import Mathlib.Tactic.Push open Freiman
Formal statement
theorem Freiman.lower_bridge_binding_bZero : ∀ r ∈ lowerBridgeRecords .bZero, ∀ x y : ℝ, certPolyEval r.polynomial x y = lowerBridgeNumerator .bZero r x y := by sorry
Source
Freiman report, initial_bridges.tex, corrected marked H entries; H_entry_bridges.json 185 exact polynomial records.