`RCLCombiner_zero_separatelyAdditive`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.BranchSelection
domain: Foundation
line: 130 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.BranchSelection on GitHub at line 130.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 127/-- For `c = 0`, the RCL combiner is the additive combiner
 128`P(u, v) = 2u + 2v`, separately additive with `p(u) = 2u` and
 129`q(v) = 2v`. -/
 130theorem RCLCombiner_zero_separatelyAdditive :
 131    SeparatelyAdditive (RCLCombiner 0) := by
 132  refine ⟨fun u => 2 * u, fun v => 2 * v, ?_⟩
 133  intro u v
 134  unfold RCLCombiner
 135  ring
 136
 137/-- For `c ≠ 0`, the RCL combiner has nonvanishing interaction defect
 138at the test point `(1, 1)`. -/
 139theorem RCLCombiner_nonzero_couples (c : ℝ) (hc : c ≠ 0) :
 140    interactionDefect (RCLCombiner c) 1 1 ≠ 0 := by
 141  rw [interactionDefect_RCLCombiner]
 142  simpa using hc
 143
 144/-- **The RCL combiner is a coupling combiner iff `c ≠ 0`.** -/
 145theorem RCLCombiner_isCoupling_iff (c : ℝ) :
 146    IsCouplingCombiner (RCLCombiner c) ↔ c ≠ 0 := by
 147  rw [isCouplingCombiner_iff_interactionDefect_nonzero]
 148  constructor
 149  · rintro ⟨u, v, huv⟩
 150    intro hc
 151    apply huv
 152    rw [interactionDefect_RCLCombiner, hc]
 153    ring
 154  · intro hc
 155    exact ⟨1, 1, RCLCombiner_nonzero_couples c hc⟩
 156
 157/-! ## Branch Selection Theorem -/
 158
 159/-- **Branch selection by non-degeneracy.**
 160

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.