IndisputableMonolith.Foundation.LogicAsFunctionalEquation.DirectProof

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation
   3
   4/-!
   5# Direct RCL theorem for operative positive-ratio comparison
   6
   7This module gives the paper-facing "operative comparison" wrapper around the
   8already-formalised translation theorem.  It isolates the finite pairwise
   9polynomial closure hypothesis as the precise regularity condition needed to
  10force the Recognition Composition Law family, and it also proves the strict
  11bi-affine counted-once subcase directly.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace Foundation
  16namespace LogicAsFunctionalEquation
  17
  18open Real
  19open IndisputableMonolith.Foundation.DAlembert.Inevitability
  20
  21/-- An operative positive-ratio comparison is a continuous, nontrivial
  22comparison operator satisfying identity, symmetric single-valued comparison,
  23and scale invariance on positive arguments. -/
  24structure OperativePositiveRatioComparison (C : ComparisonOperator) : Prop where
  25  identity : Identity C
  26  non_contradiction : NonContradiction C
  27  continuous : ExcludedMiddle C
  28  scale_invariant : ScaleInvariant C
  29  non_trivial : NonTrivial C
  30
  31/-- Finite pairwise polynomial closure is the polynomial route-independence
  32condition from the Level-1 logic-as-functional-equation module. -/
  33def FinitePairwisePolynomialClosure (C : ComparisonOperator) : Prop :=
  34  RouteIndependence C
  35
  36/-- Scale invariance descends a two-argument comparison to a cost on the
  37positive ratio of the arguments. -/
  38theorem operative_descends_to_ratio
  39    (C : ComparisonOperator)
  40    (hOp : OperativePositiveRatioComparison C) :
  41    ∀ x y : ℝ, 0 < x → 0 < y → C x y = derivedCost C (x / y) := by
  42  intro x y hx hy
  43  unfold derivedCost
  44  have hy_inv_pos : 0 < y⁻¹ := inv_pos.mpr hy
  45  have hscale := hOp.scale_invariant x y y⁻¹ hx hy hy_inv_pos
  46  have hleft : y⁻¹ * x = x / y := by
  47    rw [div_eq_mul_inv, mul_comm]
  48  have hright : y⁻¹ * y = 1 := by
  49    exact inv_mul_cancel₀ (ne_of_gt hy)
  50  calc
  51    C x y = C (y⁻¹ * x) (y⁻¹ * y) := hscale.symm
  52    _ = C (x / y) 1 := by rw [hleft, hright]
  53
  54/-- Operative comparisons have reciprocal-symmetric derived costs. -/
  55theorem operative_derived_cost_symmetric
  56    (C : ComparisonOperator)
  57    (hOp : OperativePositiveRatioComparison C) :
  58    IsSymmetric (derivedCost C) :=
  59  non_contradiction_and_scale_imply_reciprocal C
  60    hOp.non_contradiction hOp.scale_invariant
  61
  62/-- Package an operative comparison plus finite pairwise closure as the
  63`SatisfiesLawsOfLogic` structure used by the Level-1 theorem. -/
  64theorem operative_to_laws_of_logic
  65    (C : ComparisonOperator)
  66    (hOp : OperativePositiveRatioComparison C)
  67    (hFinite : FinitePairwisePolynomialClosure C) :
  68    SatisfiesLawsOfLogic C where
  69  identity := hOp.identity
  70  non_contradiction := hOp.non_contradiction
  71  excluded_middle := hOp.continuous
  72  scale_invariant := hOp.scale_invariant
  73  route_independence := hFinite
  74  non_trivial := hOp.non_trivial
  75
  76/-- **RCL as the finite pairwise polynomial algebra of positive-ratio comparison.**
  77
  78Any operative positive-ratio comparison with finite pairwise polynomial
  79closure has a derived cost satisfying the Recognition Composition Law family.
  80This theorem uses the existing d'Alembert inevitability theorem, since its
  81hypothesis is the broader polynomial-degree-two closure condition.
  82-/
  83theorem rcl_polynomial_closure_theorem
  84    (C : ComparisonOperator)
  85    (hOp : OperativePositiveRatioComparison C)
  86    (hFinite : FinitePairwisePolynomialClosure C) :
  87    ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
  88      HasMultiplicativeConsistency (derivedCost C) P ∧
  89      (∀ u v, P u v = 2 * u + 2 * v + c * u * v) := by
  90  exact RCL_is_unique_functional_form_of_logic C
  91    (operative_to_laws_of_logic C hOp hFinite)
  92
  93/-- **Direct counted-once algebra.**
  94
  95If the combiner is already known to be bi-affine,
  96`P u v = a + b*u + c*v + d*u*v`, then identity, non-triviality and
  97composition with the identity force `a = 0`, `b = 2`, and `c = 2`.
  98This is the self-contained algebraic proof used for the counted-once
  99subcase, independent of the d'Alembert inevitability theorem. -/
 100theorem rcl_direct_theorem
 101    (C : ComparisonOperator)
 102    (hOp : OperativePositiveRatioComparison C)
 103    (P : ℝ → ℝ → ℝ)
 104    (a b c d : ℝ)
 105    (hP : ∀ u v, P u v = a + b * u + c * v + d * u * v)
 106    (hSym : ∀ u v, P u v = P v u)
 107    (hCons : HasMultiplicativeConsistency (derivedCost C) P) :
 108    ∃ c0 : ℝ, ∀ u v, P u v = 2 * u + 2 * v + c0 * u * v := by
 109  have hF1 : derivedCost C 1 = 0 := by
 110    simpa [derivedCost] using hOp.identity 1 zero_lt_one
 111  rcases hOp.non_trivial with ⟨x0, hx0_pos, hx0_ne⟩
 112  let t := derivedCost C x0
 113  have ht_ne : t ≠ 0 := hx0_ne
 114
 115  have hCons11 := hCons 1 1 zero_lt_one zero_lt_one
 116  have hC11 : C 1 1 = 0 := hOp.identity 1 zero_lt_one
 117  have ha_zero : a = 0 := by
 118    have hp00 : P 0 0 = a := by
 119      simpa using hP 0 0
 120    have hzero : P 0 0 = 0 := by
 121      have htmp : 0 = P 0 0 := by
 122        simpa [derivedCost, hC11] using hCons11
 123      exact htmp.symm
 124    exact hp00 ▸ hzero
 125
 126  have hCons_x1 := hCons x0 1 hx0_pos zero_lt_one
 127  have hb_two : b = 2 := by
 128    have hmain : t + t = a + b * t := by
 129      simpa [derivedCost, t, hC11, hP] using hCons_x1
 130    have hprod : (2 - b) * t = 0 := by
 131      nlinarith [hmain, ha_zero]
 132    have hfactor : 2 - b = 0 := by
 133      exact (mul_eq_zero.mp hprod).resolve_right ht_ne
 134    linarith
 135
 136  have hc_two : c = 2 := by
 137    have hsym_t0 : P 0 t = P t 0 := hSym 0 t
 138    have hleft : P 0 t = c * t := by
 139      simpa [ha_zero] using hP 0 t
 140    have hright : P t 0 = b * t := by
 141      simpa [ha_zero] using hP t 0
 142    have hct : c * t = b * t := by
 143      simpa [hleft, hright] using hsym_t0
 144    have hct' : c * t = 2 * t := by
 145      simpa [hb_two] using hct
 146    have hprod : (c - 2) * t = 0 := by
 147      nlinarith
 148    have hfactor : c - 2 = 0 := by
 149      exact (mul_eq_zero.mp hprod).resolve_right ht_ne
 150    linarith
 151
 152  refine ⟨d, ?_⟩
 153  intro u v
 154  calc
 155    P u v = a + b * u + c * v + d * u * v := hP u v
 156    _ = 2 * u + 2 * v + d * u * v := by
 157      rw [ha_zero, hb_two, hc_two]
 158      ring
 159
 160end LogicAsFunctionalEquation
 161end Foundation
 162end IndisputableMonolith
 163