IndisputableMonolith.Foundation.LogicAsFunctionalEquation.CountOnceComparison

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.AnalyticCounterexample
   3import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.RealityStructure
   4
   5/-!
   6# Counted-once comparison
   7
   8This module formalises the phrase "each constituent comparison is counted
   9once."  Algebraically, for two component costs `u` and `v`, this means the
  10combiner is affine in each variable separately:
  11
  12`a + b*u + c*v + d*u*v`.
  13
  14Identity and symmetry then force the RCL-family form.
  15The resource-syntax and no-hidden-state bridges in sibling modules show how
  16this algebra arises from using each comparison resource once, with no hidden
  17route memory.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace Foundation
  22namespace LogicAsFunctionalEquation
  23
  24open IndisputableMonolith.Foundation.DAlembert.Inevitability
  25
  26/-- The RCL family predicate for a one-variable derived cost. -/
  27def RCLFamily (F : ℝ → ℝ) : Prop :=
  28  ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
  29    HasMultiplicativeConsistency F P ∧
  30    (∀ u v, P u v = 2 * u + 2 * v + c * u * v)
  31
  32/-- A combiner is counted-once when it is affine in each input separately. -/
  33def CountedOnceCombiner (P : ℝ → ℝ → ℝ) : Prop :=
  34  ∃ a b c d : ℝ, ∀ u v, P u v = a + b * u + c * v + d * u * v
  35
  36/-- A combiner is symmetric when exchanging its arguments does not change it. -/
  37def SymmetricCombiner (P : ℝ → ℝ → ℝ) : Prop :=
  38  ∀ u v, P u v = P v u
  39
  40/-- Counted-once composition for a comparison operator. -/
  41def CountedOnceComposition (C : ComparisonOperator) : Prop :=
  42  ∃ P : ℝ → ℝ → ℝ,
  43    CountedOnceCombiner P ∧
  44    SymmetricCombiner P ∧
  45    (∀ x y : ℝ, 0 < x → 0 < y →
  46      derivedCost C (x * y) + derivedCost C (x / y) =
  47        P (derivedCost C x) (derivedCost C y))
  48
  49/-- Counted-once composition is a special case of finite pairwise polynomial
  50closure. -/
  51theorem counted_once_to_finite_pairwise_polynomial
  52    (C : ComparisonOperator)
  53    (hCount : CountedOnceComposition C) :
  54    FinitePairwisePolynomialClosure C := by
  55  rcases hCount with ⟨P, ⟨a, b, c, d, hP⟩, hSym, hCons⟩
  56  refine ⟨P, ?_, hSym, hCons⟩
  57  refine ⟨a, b, c, d, 0, 0, ?_⟩
  58  intro u v
  59  rw [hP]
  60  ring
  61
  62/-- Counted-once operative comparison forces the RCL family. -/
  63theorem counted_once_combiner_forces_rcl
  64    (C : ComparisonOperator)
  65    (hOp : OperativePositiveRatioComparison C)
  66    (hCount : CountedOnceComposition C) :
  67    RCLFamily (derivedCost C) := by
  68  rcases hCount with ⟨P, ⟨a, b, c, d, hP⟩, hSym, hCons⟩
  69  rcases rcl_direct_theorem C hOp P a b c d hP hSym hCons with
  70    ⟨c0, hRCL⟩
  71  exact ⟨P, c0, hCons, hRCL⟩
  72
  73/-- Continuous non-counted composition is not enough to force the RCL family:
  74the quartic-log combiner has a square-root interaction term. -/
  75theorem double_counting_not_allowed :
  76    ¬ ∃ c : ℝ, ∀ a b : ℝ, 0 < a → 0 < b →
  77      quarticCombiner a b = 2 * a + 2 * b + c * a * b :=
  78  quarticCombiner_not_rcl_family
  79
  80/-- Analytic reparameterisation is not counted-once: it changes the polynomial
  81degree of the combiner. -/
  82theorem analytic_reparameterization_not_counted_once :
  83    ¬ ∃ c : ℝ, ∀ s : ℝ, reparamDiagonal s = degreeTwoDiagonal c s :=
  84  reparam_diagonal_not_degree_two
  85
  86end LogicAsFunctionalEquation
  87end Foundation
  88end IndisputableMonolith
  89