Freiman marked initial bridges: binding bPos
ProvedFreiman.lower_bridge_binding_bPoscertificatesfreimanlower-construction
Finite exact coefficient identities for the actual bPos 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_bPos : ∀ r ∈ lowerBridgeRecords .bPos, ∀ x y : ℝ, certPolyEval r.polynomial x y = lowerBridgeNumerator .bPos r x y := by sorry
Source
Freiman report, initial_bridges.tex, corrected marked H entries; H_entry_bridges.json 185 exact polynomial records.