pith. machine review for the scientific record. sign in
theorem proved term proof

branch_selection

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 173theorem branch_selection (c : ℝ)
 174    (hCoupling : IsCouplingCombiner (RCLCombiner c)) :
 175    c ≠ 0 :=

proof body

Term-mode proof.

 176  (RCLCombiner_isCoupling_iff c).mp hCoupling
 177
 178/-- The contrapositive: if `c = 0`, the RCL combiner is not coupling. The
 179additive branch fails the strengthened (L4*). -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.