BranchSelectionCert

formal source

 189The structural strengthening of (L4) — coupling, that is, non-additivity —
 190forces the bilinear branch within the polynomial RCL family produced by
 191the translation theorem of `Logic_Functional_Equation.tex`. -/
 192structure BranchSelectionCert where
 193  separately_additive_iff_defect_zero :
 194    ∀ P : ℝ → ℝ → ℝ,
 195      SeparatelyAdditive P ↔ ∀ u v : ℝ, interactionDefect P u v = 0
 196  coupling_iff_defect_nonzero :
 197    ∀ P : ℝ → ℝ → ℝ,
 198      IsCouplingCombiner P ↔ ∃ u v : ℝ, interactionDefect P u v ≠ 0
 199  rcl_coupling_iff :
 200    ∀ c : ℝ, IsCouplingCombiner (RCLCombiner c) ↔ c ≠ 0
 201  bilinear_branch_forced :
 202    ∀ c : ℝ, IsCouplingCombiner (RCLCombiner c) → c ≠ 0
 203  additive_branch_excluded :
 204    ¬ IsCouplingCombiner (RCLCombiner 0)
 205
 206def branchSelectionCert : BranchSelectionCert where
 207  separately_additive_iff_defect_zero :=
 208    fun P => separatelyAdditive_iff_interactionDefect_zero P
 209  coupling_iff_defect_nonzero :=
 210    fun P => isCouplingCombiner_iff_interactionDefect_nonzero P
 211  rcl_coupling_iff := RCLCombiner_isCoupling_iff
 212  bilinear_branch_forced := branch_selection
 213  additive_branch_excluded := additive_branch_not_coupling
 214
 215theorem branchSelectionCert_inhabited : Nonempty BranchSelectionCert :=
 216  ⟨branchSelectionCert⟩
 217
 218end BranchSelection
 219end Foundation
 220end IndisputableMonolith