pith. machine review for the scientific record. sign in
theorem

branch_selection

proved
show as:
view math explainer →
module
IndisputableMonolith.Foundation.BranchSelection
domain
Foundation
line
173 · github
papers citing
385 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.BranchSelection on GitHub at line 173.

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

used by

formal source

 170addressed by separate generator-calibration / higher-derivative /
 171action-functional conditions, none of which are part of the
 172operator-level Aristotelian content. -/
 173theorem branch_selection (c : ℝ)
 174    (hCoupling : IsCouplingCombiner (RCLCombiner c)) :
 175    c ≠ 0 :=
 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*). -/
 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 :