IndisputableMonolith.Foundation.LogicAsFunctionalEquation.QuarticLogCounterexample

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.DirectProof
   3
   4/-!
   5# Quartic-log counterexample
   6
   7This module formalises the algebraic heart of the counterexample from the
   8Logic Functional Equation paper:
   9
  10`C(x,y) = (log (x/y))^4`
  11
  12has a continuous symmetric combiner on the nonnegative range,
  13
  14`Φ(a,b) = 2a + 2b + 12 sqrt(a b)`,
  15
  16but no constant `c` can make the square-root term equal to `c a b` for all
  17positive `a,b`.  Thus arbitrary continuous compositionality does not force
  18the RCL family; finite pairwise polynomial closure is essential.
  19-/
  20
  21namespace IndisputableMonolith
  22namespace Foundation
  23namespace LogicAsFunctionalEquation
  24
  25open Real
  26
  27/-- The quartic-log comparison used as the counterexample. -/
  28noncomputable def quarticLogComparison : ComparisonOperator :=
  29  fun x y => (Real.log (x / y)) ^ (4 : Nat)
  30
  31/-- The continuous non-polynomial combiner associated to the quartic-log
  32comparison on the nonnegative range. -/
  33noncomputable def quarticCombiner (a b : ℝ) : ℝ :=
  34  2 * a + 2 * b + 12 * Real.sqrt (a * b)
  35
  36theorem quarticCombiner_symmetric :
  37    ∀ a b : ℝ, quarticCombiner a b = quarticCombiner b a := by
  38  intro a b
  39  unfold quarticCombiner
  40  rw [mul_comm a b]
  41  ring
  42
  43theorem quarticCombiner_nonneg_on_nonneg :
  44    ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → 0 ≤ quarticCombiner a b := by
  45  intro a b ha hb
  46  unfold quarticCombiner
  47  have h2a : 0 ≤ 2 * a := by positivity
  48  have h2b : 0 ≤ 2 * b := by positivity
  49  have hsqrt : 0 ≤ 12 * Real.sqrt (a * b) := by positivity
  50  linarith
  51
  52/-- The square-root term in the quartic combiner cannot be represented by a
  53single bilinear coefficient `c*a*b` on all positive inputs. -/
  54theorem quartic_sqrt_term_not_bilinear :
  55    ¬ ∃ c : ℝ, ∀ a b : ℝ, 0 < a → 0 < b →
  56      12 * Real.sqrt (a * b) = c * a * b := by
  57  intro h
  58  rcases h with ⟨c, hc⟩
  59  have h11 := hc 1 1 (by norm_num) (by norm_num)
  60  have hc_eq : c = 12 := by
  61    norm_num [Real.sqrt_one] at h11
  62    linarith
  63  have h44 := hc 4 4 (by norm_num) (by norm_num)
  64  have hsqrt16 : Real.sqrt (4 * 4) = 4 := by
  65    norm_num
  66  rw [hsqrt16, hc_eq] at h44
  67  norm_num at h44
  68
  69/-- Therefore the quartic combiner is not in the RCL bilinear family. -/
  70theorem quarticCombiner_not_rcl_family :
  71    ¬ ∃ c : ℝ, ∀ a b : ℝ, 0 < a → 0 < b →
  72      quarticCombiner a b = 2 * a + 2 * b + c * a * b := by
  73  intro h
  74  rcases h with ⟨c, hc⟩
  75  apply quartic_sqrt_term_not_bilinear
  76  refine ⟨c, ?_⟩
  77  intro a b ha hb
  78  have hab := hc a b ha hb
  79  unfold quarticCombiner at hab
  80  linarith
  81
  82end LogicAsFunctionalEquation
  83end Foundation
  84end IndisputableMonolith
  85