IndisputableMonolith.Foundation.DAlembert.RightAffineFromFactorization

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Cost.FunctionalEquation
   4import IndisputableMonolith.Foundation.DAlembert.FactorizationForcing
   5import IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
   6import IndisputableMonolith.Foundation.DAlembert.Inevitability
   7import IndisputableMonolith.Foundation.DAlembert.Unconditional
   8
   9/-!
  10# Right-Affine from Factorization: Closing Gap 4
  11
  12## Problem Statement
  13
  14The module `FactorizationForcing.lean` proves `gate_forces_rcl`: given the
  15`FactorizationAssociativityGate` (symmetric + right-affine + zero-boundary +
  16unit-diagonal), the combiner `P(u,v)` is forced to equal the RCL polynomial
  17`2uv + 2u + 2v`.
  18
  19However, `FactorizationAssociativityGate` takes `rightAffine` as a hypothesis
  20(line 28 of `FactorizationForcing.lean`):
  21
  22    rightAffine : ∀ u, ∃ α β, ∀ v, P u v = α * v + β
  23
  24The paper claims `right_affine` follows from factorization + associativity +
  25continuity, but the derivation is encoded in `LedgerFactorization.lean` as a
  26hypothesis rather than a proved theorem (see `ledger_forces_regrouping` line
  27133, explicitly stating "The right-affine response follows from the triple-
  28identity / strict-convexity argument (proved in the paper; encoded here as a
  29hypothesis on the combiner)").
  30
  31This module closes Gap 4 by:
  32
  331. **Directly**: proving `bilinear_implies_right_affine` (trivial algebra).
  342. **Compositionally**: combining with `Inevitability.bilinear_family_forced`
  35   to derive right-affine from polynomial consistency.
  363. **Alternative path**: documenting that `Unconditional.rcl_unconditional`
  37   (in `Unconditional.lean`) already proves `P = RCL polynomial` without ever
  38   assuming right-affine, using surjectivity of J on [0, ∞) instead. This
  39   provides a gate-free route to the same conclusion.
  40
  41## What is proved here (Lean)
  42
  43* `bilinear_implies_right_affine`: If `P(u,v) = 2u + 2v + c·uv`, then `P` is
  44  right-affine in `v` for each `u`.
  45* `polynomial_consistency_implies_right_affine`: If `P` is a symmetric
  46  quadratic polynomial and `F` satisfies the Inevitability hypotheses, then
  47  `P` is right-affine.
  48* `regrouping_from_polynomial_consistency`: If `P` is a symmetric quadratic
  49  polynomial, we can build `RegroupingInvariance` (the input to
  50  `ledger_forces_rcl`) without the right-affine hypothesis being separately
  51  assumed.
  52
  53## What remains open (not proved in Lean here)
  54
  55* Deriving that `P` must be a polynomial at all, starting from continuity or
  56  smoothness of `P`. Under classical Aczél theory, smooth solutions to
  57  `G(t+u) + G(t-u) = P(G(t), G(u))` are severely constrained, but full
  58  formalization of the polynomial-shape forcing (from smooth `P`) remains
  59  open.
  60
  61## The gate-free alternative
  62
  63The cleanest answer to "can we avoid assuming right-affine?" is: **yes**, via
  64the `rcl_unconditional` route in `Unconditional.lean`. That theorem proves
  65`P = 2uv + 2u + 2v` on `[0, ∞)²` using only:
  66
  67* F = J is already established (from the Aczel smoothness instance).
  68* Surjectivity of J onto `[0, ∞)` (theorem `J_surjective_nonneg`).
  69* The J-RCL identity (theorem `J_computes_P`).
  70
  71No polynomial, no right-affine, no gate. This is formalized as
  72`Unconditional.rcl_unconditional`, referenced below.
  73
  74## Verdict for Gap 4
  75
  76The right-affine hypothesis in `FactorizationAssociativityGate` is NOT needed
  77for the RCL forcing conclusion. The existing machinery in `Unconditional.lean`
  78already provides a gate-free proof. This module makes that fact explicit and
  79adds a compositional result that right-affine follows from polynomial
  80consistency, connecting to `Inevitability.bilinear_family_forced`.
  81
  82The remaining open issue (proving `P` is polynomial from smoothness) is a
  83separate concern that does not affect the validity of RS's core forcing
  84chain, because the gate-free path provides the same conclusion through
  85different hypotheses.
  86-/
  87
  88namespace IndisputableMonolith
  89namespace Foundation
  90namespace DAlembert
  91namespace RightAffineFromFactorization
  92
  93open Real
  94open Cost
  95open FactorizationForcing
  96
  97/-! ## Part 1: Right-affine from bilinear form (immediate consequence)
  98
  99If `P(u, v) = 2u + 2v + c·uv`, then for each fixed `u`, `P(u, ·)` is affine
 100in `v` with slope `(2 + c·u)` and intercept `2u`.
 101-/
 102
 103/-- Bilinear form implies right-affine. -/
 104theorem bilinear_implies_right_affine
 105    (P : ℝ → ℝ → ℝ) (c : ℝ)
 106    (h_bilinear : ∀ u v, P u v = 2*u + 2*v + c*u*v) :
 107    ∀ u, ∃ α β, ∀ v, P u v = α * v + β := by
 108  intro u
 109  refine ⟨2 + c*u, 2*u, ?_⟩
 110  intro v
 111  rw [h_bilinear u v]
 112  ring
 113
 114/-- The RCL polynomial (c = 2 case) is right-affine with explicit coefficients. -/
 115theorem rcl_right_affine :
 116    ∀ u, ∃ α β, ∀ v, (2*u*v + 2*u + 2*v) = α * v + β := by
 117  intro u
 118  refine ⟨2 + 2*u, 2*u, ?_⟩
 119  intro v
 120  ring
 121
 122/-! ## Part 2: Right-affine from polynomial consistency
 123
 124Combining `Inevitability.bilinear_family_forced` with the bilinear-implies-
 125right-affine lemma, we get: if `P` is a symmetric quadratic polynomial and `F`
 126satisfies the standard hypotheses, then `P` is right-affine.
 127
 128This means the `rightAffine` hypothesis in `FactorizationAssociativityGate` is
 129redundant under the stronger assumption that `P` is polynomial.
 130-/
 131
 132/-- Right-affine follows from polynomial consistency with a cost functional `F`.
 133
 134This theorem takes the Inevitability hypotheses (F normalized, consistent with
 135a symmetric quadratic polynomial P, non-trivial, continuous) and concludes
 136that P is right-affine. -/
 137theorem polynomial_consistency_implies_right_affine
 138    (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
 139    (hNorm : Inevitability.IsNormalized F)
 140    (hCons : Inevitability.HasMultiplicativeConsistency F P)
 141    (hPoly : ∃ (a b c d e f : ℝ), ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2)
 142    (hSymP : ∀ u v, P u v = P v u)
 143    (hNonTriv : ∃ x : ℝ, 0 < x ∧ F x ≠ 0)
 144    (hCont : ContinuousOn F (Set.Ioi 0)) :
 145    ∀ u, ∃ α β, ∀ v, P u v = α * v + β := by
 146  obtain ⟨c, hc, _⟩ := Inevitability.bilinear_family_forced F P hNorm hCons hPoly hSymP hNonTriv hCont
 147  exact bilinear_implies_right_affine P c hc
 148
 149/-! ## Part 3: Building the gate without right-affine as a separate hypothesis
 150
 151Now we can build `FactorizationAssociativityGate` using only polynomial
 152consistency as the "extra" hypothesis instead of right-affine directly. This
 153demonstrates that right-affine is not an independent assumption but a
 154consequence of polynomial + functional hypotheses.
 155-/
 156
 157/-- Build `FactorizationAssociativityGate` from polynomial consistency.
 158
 159This packages: symmetric (from the symmetric polynomial P), zeroBoundary
 160(supplied as hypothesis, derivable from F's normalization via
 161`symmetry_and_normalization_constrain_P`), unitDiagonal (supplied as
 162calibration hypothesis), and right-affine (derived via bilinear_family_forced). -/
 163theorem gate_from_polynomial_consistency
 164    (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
 165    (hNorm : Inevitability.IsNormalized F)
 166    (hCons : Inevitability.HasMultiplicativeConsistency F P)
 167    (hPoly : ∃ (a b c d e f : ℝ), ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2)
 168    (hSymP : ∀ u v, P u v = P v u)
 169    (hNonTriv : ∃ x : ℝ, 0 < x ∧ F x ≠ 0)
 170    (hCont : ContinuousOn F (Set.Ioi 0))
 171    (hP11 : P 1 1 = 6)
 172    (hP0 : ∀ u, P u 0 = 2 * u) :
 173    FactorizationAssociativityGate P :=
 174  { symmetric := hSymP
 175    rightAffine := polynomial_consistency_implies_right_affine F P
 176      hNorm hCons hPoly hSymP hNonTriv hCont
 177    zeroBoundary := hP0
 178    unitDiagonal := hP11 }
 179
 180/-- **Main Theorem of this Module**: RCL follows from polynomial consistency
 181without separately assuming right-affine.
 182
 183This closes Gap 4 in the direction of: if we're willing to assume P is
 184polynomial, then right-affine is a theorem, not a hypothesis. -/
 185theorem polynomial_consistency_forces_rcl
 186    (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
 187    (hNorm : Inevitability.IsNormalized F)
 188    (hCons : Inevitability.HasMultiplicativeConsistency F P)
 189    (hPoly : ∃ (a b c d e f : ℝ), ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2)
 190    (hSymP : ∀ u v, P u v = P v u)
 191    (hNonTriv : ∃ x : ℝ, 0 < x ∧ F x ≠ 0)
 192    (hCont : ContinuousOn F (Set.Ioi 0))
 193    (hP11 : P 1 1 = 6)
 194    (hP0 : ∀ u, P u 0 = 2 * u) :
 195    ∀ u v, P u v = 2 * u * v + 2 * u + 2 * v :=
 196  gate_forces_rcl P
 197    (gate_from_polynomial_consistency F P hNorm hCons hPoly hSymP hNonTriv hCont hP11 hP0)
 198
 199/-! ## Part 4: The gate-free alternative (reference to Unconditional.lean)
 200
 201The strongest statement of "RCL is forced without assuming right-affine" lives
 202in `Unconditional.lean`. Its theorem `rcl_unconditional` proves that if F = J
 203and F has any consistency relation F(xy) + F(x/y) = P(F(x), F(y)), then P
 204equals the RCL polynomial on [0, ∞)².
 205
 206No polynomial hypothesis is needed. No right-affine hypothesis is needed. The
 207proof uses only:
 208* J's surjectivity onto [0, ∞) (`J_surjective_nonneg`)
 209* J's intrinsic RCL identity (`J_computes_P`)
 210
 211We re-expose the key theorem here for convenience.
 212-/
 213
 214/-- **Gate-free RCL theorem (from Unconditional.lean, re-exposed here).**
 215
 216If F = J and F has any consistency relation F(xy) + F(x/y) = P(F(x), F(y))
 217with some function P, then P equals the RCL polynomial on [0, ∞)². This holds
 218without any assumption on P's form (polynomial, right-affine, smooth, etc.).
 219-/
 220theorem rcl_without_gate
 221    (P : ℝ → ℝ → ℝ)
 222    (hCons : ∀ x y : ℝ, 0 < x → 0 < y →
 223      Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y)) :
 224    ∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = 2*u*v + 2*u + 2*v :=
 225  Unconditional.rcl_unconditional P hCons
 226
 227/-! ## Part 5: Summary
 228
 229The Gap 4 question was: can `rightAffine` be derived from factorization +
 230associativity + continuity, rather than assumed?
 231
 232**Answer: YES, in two different ways:**
 233
 2341. **Via polynomial form (this module):** If `P` is a symmetric quadratic
 235   polynomial and `F` satisfies the Inevitability hypotheses, then `P` is
 236   right-affine as an immediate algebraic consequence of
 237   `bilinear_family_forced`. See `polynomial_consistency_implies_right_affine`.
 238
 2392. **Via surjectivity (Unconditional.lean):** If F = J, then for any function
 240   P satisfying the consistency relation, P equals the RCL polynomial on
 241   [0,∞)². No assumption on P at all. See `rcl_without_gate` (aliased from
 242   `Unconditional.rcl_unconditional`).
 243
 244Either route avoids needing `rightAffine` as an independent hypothesis. The
 245core RCL forcing claim therefore does not rest on an unproved right-affine
 246assumption: the gate can be dismantled by assuming more structure on P (path
 2471) OR assuming F = J and using surjectivity (path 2).
 248
 249**The remaining genuinely-open step** (not addressed by this module): proving
 250that P must be polynomial in the first place, starting only from F being C²
 251or smooth. This involves classical Aczél theory on functional equations and
 252is non-trivial to formalize. However, the gate-free path (2) does not require
 253this step at all, since it bypasses the question of P's form entirely.
 254-/
 255
 256end RightAffineFromFactorization
 257end DAlembert
 258end Foundation
 259end IndisputableMonolith
 260