IndisputableMonolith.Foundation.DAlembert.NecessityGates

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Foundation.DAlembert.Counterexamples
   4
   5/-!
   6# Necessity Gates for RCL Inevitability
   7
   8The counterexample in `Foundation/DAlembert/Counterexamples.lean` shows that
   9
  10> (symmetry + normalization + C² + calibration + existence of *some* combiner P)
  11
  12does **not** force the d'Alembert/RCL structure.
  13
  14Therefore, any honest ``full inevitability'' statement must include at least one
  15additional nondegeneracy gate that rules out the additive/quadratic-log branch.
  16
  17This module implements the **minimal** such gate:
  18
  19## Gate: Interaction / Non-additivity
  20
  21If costs were purely additive under composition, then in log-coordinates the cost is quadratic:
  22
  23`F(x) = (log x)^2 / 2`
  24
  25and the combiner is `P(u,v)=2u+2v`. This branch does not produce the RCL.
  26
  27The interaction gate asserts that there exists at least one pair of comparisons
  28whose combined cost is **not** purely additive in the two individual costs.
  29
  30This is the weakest possible ``anti-quadratic'' gate and is satisfied by `Jcost`.
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Foundation
  35namespace DAlembert
  36namespace NecessityGates
  37
  38open Real
  39open IndisputableMonolith.Cost
  40open IndisputableMonolith.Foundation.DAlembert.Counterexamples
  41
  42/-! ## Gate definition -/
  43
  44/-- **Interaction / non-additivity gate** for a cost `F`.
  45
  46`HasInteraction F` means there exist `x,y>0` such that the product/quotient combined cost
  47is not purely additive in the two individual costs. -/
  48def HasInteraction (F : ℝ → ℝ) : Prop :=
  49  ∃ x y : ℝ, 0 < x ∧ 0 < y ∧
  50    F (x * y) + F (x / y) ≠ 2 * F x + 2 * F y
  51
  52/-! ## The quadratic-log branch fails the gate -/
  53
  54lemma Fquad_additive (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
  55    Fquad (x * y) + Fquad (x / y) = 2 * Fquad x + 2 * Fquad y := by
  56  -- This is exactly `Fquad_consistency` with `Padd u v = 2u+2v`.
  57  simpa [Padd] using (Fquad_consistency x y hx hy)
  58
  59theorem Fquad_noInteraction : ¬ HasInteraction Fquad := by
  60  intro h
  61  rcases h with ⟨x, y, hx, hy, hneq⟩
  62  exact hneq (Fquad_additive x y hx hy)
  63
  64/-! ## Jcost satisfies the gate -/
  65
  66theorem Jcost_hasInteraction : HasInteraction Jcost := by
  67  -- Concrete witness: x = y = 2.
  68  refine ⟨2, 2, by norm_num, by norm_num, ?_⟩
  69  -- Evaluate numerically: J(4) + J(1) ≠ 2J(2) + 2J(2).
  70  -- J(1)=0, J(2)=1/4, J(4)=9/8.
  71  norm_num [Jcost]
  72
  73end NecessityGates
  74end DAlembert
  75end Foundation
  76end IndisputableMonolith
  77