additive_branch_not_coupling

formal source

 177
 178/-- The contrapositive: if `c = 0`, the RCL combiner is not coupling. The
 179additive branch fails the strengthened (L4*). -/
 180theorem additive_branch_not_coupling :
 181    ¬ IsCouplingCombiner (RCLCombiner 0) := by
 182  intro h
 183  exact branch_selection 0 h rfl
 184
 185/-! ## Headline Certificate -/
 186
 187/-- **Branch Selection Certificate.**
 188
 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