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