IndisputableMonolith.Foundation.BranchSelection

   1import Mathlib
   2
   3/-!
   4# Branch Selection: Coupling Combiner Forces the Bilinear Branch
   5
   6The Logic_FE rigidity theorem produces the Recognition Composition Law
   7family
   8\[
   9F(xy) + F(x/y) = 2 F(x) + 2 F(y) + c\,F(x)F(y)
  10\]
  11with combiner `P(u, v) = 2u + 2v + c·u·v` for some `c ∈ ℝ`. Under
  12calibration, the family splits into a bilinear branch (`c ≠ 0`, with
  13`α = 1` representative `J(x) = ½(x + x⁻¹) − 1`) and an additive branch
  14(`c = 0`, with representative `½(ln x)²`). The translation theorem alone
  15does not select between them.
  16
  17The companion paper `RS_Branch_Selection.tex` introduces a structural
  18strengthening of (L4) Composition Consistency: the combiner must be a
  19**coupling combiner**, not separately additive in its arguments. Since the
  20RCL polynomial combiner is `P(u,v) = 2u + 2v + c·u·v`, coupling is
  21equivalent to `c ≠ 0`. Hence the strengthened (L4*) excludes the additive
  22branch.
  23
  24This module formalises that argument:
  25
  26* `IsCouplingCombiner P`: `P` is not separately additive in its arguments.
  27* `interactionDefect P`: the canonical witness for non-coupling.
  28* `RCLCombiner c`: the polynomial combiner attached to RCL parameter `c`.
  29* `RCLCombiner_isCoupling_iff`: the RCL combiner is coupling iff `c ≠ 0`.
  30* `branch_selection`: under the strengthened (L4*), the bilinear branch
  31  is forced.
  32
  33Together with Logic_FE this isolates `J` modulo the residual α-coordinate
  34freedom acknowledged in §5 of `RS_Branch_Selection.tex`.
  35-/
  36
  37namespace IndisputableMonolith
  38namespace Foundation
  39namespace BranchSelection
  40
  41/-! ## Coupling Combiners -/
  42
  43/-- A combiner `P : ℝ → ℝ → ℝ` is **separately additive** when there
  44exist single-argument functions `p, q` with `P(u, v) = p(u) + q(v)` for
  45all `u, v`. This is the structural shape we exclude from genuine
  46composition consistency. -/
  47def SeparatelyAdditive (P : ℝ → ℝ → ℝ) : Prop :=
  48  ∃ p q : ℝ → ℝ, ∀ u v : ℝ, P u v = p u + q v
  49
  50/-- A combiner is a **coupling combiner** when it is not separately
  51additive. Equivalently, the joint structure of the two arguments enters
  52the output; the cost of a composite genuinely depends on how its
  53components fit together. -/
  54def IsCouplingCombiner (P : ℝ → ℝ → ℝ) : Prop :=
  55  ¬ SeparatelyAdditive P
  56
  57/-- The **interaction defect** of a combiner at a pair `(u, v)`:
  58\[
  59\Delta P(u, v) := P(u, v) - P(u, 0) - P(0, v) + P(0, 0).
  60\]
  61For a separately additive combiner this is identically zero. The defect
  62is the canonical detector of coupling. -/
  63def interactionDefect (P : ℝ → ℝ → ℝ) (u v : ℝ) : ℝ :=
  64  P u v - P u 0 - P 0 v + P 0 0
  65
  66/-! ## Equivalent Forms -/
  67
  68/-- A separately additive combiner has identically vanishing interaction
  69defect. -/
  70theorem interactionDefect_eq_zero_of_separatelyAdditive
  71    {P : ℝ → ℝ → ℝ} (h : SeparatelyAdditive P) :
  72    ∀ u v : ℝ, interactionDefect P u v = 0 := by
  73  rcases h with ⟨p, q, hP⟩
  74  intro u v
  75  unfold interactionDefect
  76  rw [hP u v, hP u 0, hP 0 v, hP 0 0]
  77  ring
  78
  79/-- Conversely: a combiner whose interaction defect is identically zero is
  80separately additive. The witness functions are `p(u) := P(u, 0) - P(0, 0)`
  81and `q(v) := P(0, v)`. -/
  82theorem separatelyAdditive_of_interactionDefect_zero
  83    {P : ℝ → ℝ → ℝ} (h : ∀ u v : ℝ, interactionDefect P u v = 0) :
  84    SeparatelyAdditive P := by
  85  refine ⟨fun u => P u 0 - P 0 0, fun v => P 0 v, ?_⟩
  86  intro u v
  87  have h_uv := h u v
  88  unfold interactionDefect at h_uv
  89  linarith
  90
  91/-- **Equivalence: separate additivity is identical vanishing of the
  92interaction defect.** -/
  93theorem separatelyAdditive_iff_interactionDefect_zero
  94    (P : ℝ → ℝ → ℝ) :
  95    SeparatelyAdditive P ↔ ∀ u v : ℝ, interactionDefect P u v = 0 :=
  96  ⟨interactionDefect_eq_zero_of_separatelyAdditive,
  97   separatelyAdditive_of_interactionDefect_zero⟩
  98
  99/-- **Equivalence: coupling is non-vanishing interaction defect.** -/
 100theorem isCouplingCombiner_iff_interactionDefect_nonzero
 101    (P : ℝ → ℝ → ℝ) :
 102    IsCouplingCombiner P ↔ ∃ u v : ℝ, interactionDefect P u v ≠ 0 := by
 103  unfold IsCouplingCombiner
 104  rw [separatelyAdditive_iff_interactionDefect_zero]
 105  constructor
 106  · intro h
 107    by_contra hno
 108    push_neg at hno
 109    exact h hno
 110  · rintro ⟨u, v, huv⟩ hall
 111    exact huv (hall u v)
 112
 113/-! ## The RCL Combiner -/
 114
 115/-- The polynomial combiner attached to the RCL family with parameter
 116`c`: `P(u, v) = 2u + 2v + c·u·v`. -/
 117def RCLCombiner (c : ℝ) : ℝ → ℝ → ℝ :=
 118  fun u v => 2 * u + 2 * v + c * u * v
 119
 120/-- The interaction defect of the RCL combiner at `(u, v)` is exactly
 121`c · u · v`. -/
 122theorem interactionDefect_RCLCombiner (c u v : ℝ) :
 123    interactionDefect (RCLCombiner c) u v = c * u * v := by
 124  unfold interactionDefect RCLCombiner
 125  ring
 126
 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
 161If the RCL polynomial combiner is required to be a coupling combiner
 162(the strengthened (L4*) of the companion paper), then the parameter
 163`c` is forced to be nonzero. Equivalently, the additive branch
 164(`c = 0`, with calibrated representative `½(ln x)²`) is excluded.
 165
 166This is the branch-selection theorem of `RS_Branch_Selection.tex` in
 167its Lean form. The bilinear branch is forced; `J` is the
 168`α = 1` representative of the bilinear `α`-family. The residual
 169`α`-coordinate freedom is acknowledged in §5 of the paper and is
 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 :
 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
 221