IndisputableMonolith.Verification.Exclusivity.RCLDerivation

   1/-
   2  RCLDerivation.lean — Bridge B2 Scaffold
   3
   4  This file now contains the honest algebraic adapter for Bridge B2.
   5  The raw associativity-only scaffold was inconsistent with the proved
   6  boundary law `f(a,0) = 2a`, so the classification is stated in the
   7  factorization-gate form used by the forcing chain.
   8
   9  What is PROVED (zero sorry):
  10  - The d'Alembert composition rule satisfies the boundary conditions.
  11  - Boundary condition 1: f(0,0) = 0  (from J(1)=0).
  12  - Boundary condition 2: f(a,0) = 2a (from y=1 substitution).
  13  - Associativity of `f` itself contradicts the boundary law.
  14  - Under the factorization gate, the combiner is forced to the RCL polynomial.
  15
  16  Still open in the paper sense:
  17  - derive the factorization gate itself directly from multiplicative
  18    recognition structure, without packaging right-affine response as a
  19    separate hypothesis.
  20
  21  Paper §8.2: Bridge B2.
  22-/
  23
  24import Mathlib
  25import IndisputableMonolith.Foundation.DAlembert.FactorizationForcing
  26import IndisputableMonolith.Verification.Exclusivity.Framework
  27
  28namespace IndisputableMonolith
  29namespace Verification
  30namespace Exclusivity
  31namespace RCLDerivation
  32
  33set_option autoImplicit false
  34
  35open IndisputableMonolith.Foundation.DAlembert.FactorizationForcing
  36
  37/-- A composition rule: a symmetric binary function on ℝ specifying how
  38    compound cost values decompose:  J(xy) + J(x/y) = f(J(x), J(y)). -/
  39structure CompositionRule where
  40  f         : ℝ → ℝ → ℝ
  41  symmetric : ∀ a b, f a b = f b a
  42
  43/-- The d'Alembert composition rule: f(a,b) = 2(a+1)(b+1) - 2.
  44    Equivalently: f(a,b) = 2ab + 2a + 2b. -/
  45noncomputable def dAlembertRule : CompositionRule where
  46  f         := fun a b => 2 * (a + 1) * (b + 1) - 2
  47  symmetric := by intro a b; ring
  48
  49/-- Boundary condition 1 (proved): f(0,0) = 0.
  50    Derivation: set x = y = 1 in J(xy)+J(x/y) = f(J(x),J(y)).
  51    J(1)+J(1) = f(J(1),J(1)) = f(0,0), so f(0,0) = 0. -/
  52theorem composition_rule_f00_eq_zero
  53    (f : CompositionRule) (J : ℝ → ℝ)
  54    (hJ0   : J 1 = 0)
  55    (hComp : ∀ x y, 0 < x → 0 < y →
  56               J (x * y) + J (x / y) = f.f (J x) (J y)) :
  57    f.f 0 0 = 0 := by
  58  have h := hComp 1 1 one_pos one_pos
  59  simp [hJ0] at h
  60  linarith
  61
  62/-- Boundary condition 2 (proved): f(a,0) = 2a.
  63    Derivation: set y = 1.  J(x)+J(x) = f(J(x),0), so f(a,0) = 2a. -/
  64theorem composition_rule_f_at_zero
  65    (f : CompositionRule) (J : ℝ → ℝ)
  66    (hJ0   : J 1 = 0)
  67    (hComp : ∀ x y, 0 < x → 0 < y →
  68               J (x * y) + J (x / y) = f.f (J x) (J y))
  69    (x : ℝ) (hx : 0 < x) :
  70    f.f (J x) 0 = 2 * J x := by
  71  have h := hComp x 1 hx one_pos
  72  simp [hJ0, mul_one, div_one] at h
  73  linarith
  74
  75/-- The d'Alembert rule satisfies both boundary conditions. -/
  76theorem dAlembert_satisfies_boundaries :
  77    dAlembertRule.f 0 0 = 0 ∧ ∀ a, dAlembertRule.f a 0 = 2 * a :=
  78  ⟨by simp [dAlembertRule], by intro a; simp [dAlembertRule]; ring⟩
  79
  80/-- The original associativity-only scaffold is inconsistent with the proved
  81    boundary law `f(a,0) = 2a`.
  82
  83    Indeed, symmetry gives `f(0,1) = 2` and `f(0,2) = 4`, while associativity
  84    at `(0,0,1)` would force `f(0,1) = f(0,2)`. So the old Open Problem B
  85    statement was malformed: the actual closure step cannot be associativity
  86    of `f` itself. -/
  87theorem associativity_contradicts_boundary
  88    (f        : CompositionRule)
  89    (h00      : f.f 0 0 = 0)
  90    (hbdry    : ∀ a, f.f a 0 = 2 * a)
  91    (h_assoc  : ∀ a b c, f.f (f.f a b) c = f.f a (f.f b c)) :
  92    False := by
  93  have h01 : f.f 0 1 = 2 := by
  94    calc
  95      f.f 0 1 = f.f 1 0 := f.symmetric 0 1
  96      _ = 2 * 1 := hbdry 1
  97      _ = 2 := by norm_num
  98  have h02 : f.f 0 2 = 4 := by
  99    calc
 100      f.f 0 2 = f.f 2 0 := f.symmetric 0 2
 101      _ = 2 * 2 := hbdry 2
 102      _ = 4 := by norm_num
 103  have h_assoc001 := h_assoc 0 0 1
 104  rw [h00, h01] at h_assoc001
 105  linarith
 106
 107/-- Bridge B2 classification in the honest form used by the forcing chain.
 108
 109    The RS algebraic closure does not use associativity of `f` itself.
 110    What is actually needed, and already proved elsewhere in the forcing
 111    chain, is the factorization gate:
 112
 113    - symmetry,
 114    - right-affine response in the second argument,
 115    - the zero-boundary law `f(a,0) = 2a`,
 116    - and the canonical normalization `f(1,1) = 6`.
 117
 118    Under those hypotheses the combiner is forced exactly to the RCL
 119    polynomial. -/
 120theorem composition_rule_classification
 121    (f        : CompositionRule)
 122    (hbdry    : ∀ a, f.f a 0 = 2 * a)
 123    (hAffine  : ∀ a, ∃ α β, ∀ b, f.f a b = α * b + β)
 124    (h11      : f.f 1 1 = 6) :
 125    ∀ a b, f.f a b = 2 * (a + 1) * (b + 1) - 2 := by
 126  let hGate : FactorizationAssociativityGate f.f :=
 127    { symmetric := f.symmetric
 128      rightAffine := hAffine
 129      zeroBoundary := hbdry
 130      unitDiagonal := h11 }
 131  intro a b
 132  calc
 133    f.f a b = 2 * a * b + 2 * a + 2 * b := gate_forces_rcl f.f hGate a b
 134    _ = 2 * (a + 1) * (b + 1) - 2 := by ring
 135
 136end RCLDerivation
 137end Exclusivity
 138end Verification
 139end IndisputableMonolith
 140