IndisputableMonolith.Foundation.MagnitudeOfMismatch

   1import Mathlib
   2import IndisputableMonolith.Foundation.PrimitiveDistinction
   3
   4/-!
   5# Magnitude of Mismatch: Symmetry from Single-Valued Predication
   6
   7The Logic_FE rigidity theorem encodes the Aristotelian condition (L2)
   8Non-Contradiction as symmetry of the comparison operator,
   9`C x y = C y x`. The companion paper
  10`RS_Magnitude_of_Mismatch_Uniqueness.tex` argues that this encoding is not
  11an interpretive choice but a structural necessity: any comparison that
  12returns a single value when applied to an unordered pair `{x, y}` must be
  13symmetric. The asymmetric "directed revision" reading does not produce a
  14single binary function; it produces two distinct directional functions.
  15
  16This module formalises that argument. The relevant primitive is the
  17observation that a function `K → K → Cost` is the same data as a
  18function `Sym2 K → Cost` exactly when it is symmetric. We prove both
  19directions:
  20
  21* `singleValued_implies_symmetric`: if `C` factors through `Sym2 K`, it
  22  is symmetric.
  23* `symmetric_implies_factorsThrough`: any symmetric `C` factors through
  24  `Sym2 K`.
  25
  26The combined `singleValued_iff_symmetric` is the Lean form of
  27Theorem 4 of the companion paper. Together with the `PrimitiveDistinction`
  28result that (L1), (L2), (L3a) are definitional, this leaves the
  29magnitude-of-mismatch encoding without any interpretive freedom: it is
  30the unique reading consistent with single-valued predication on a
  31distinguished pair.
  32-/
  33
  34namespace IndisputableMonolith
  35namespace Foundation
  36namespace MagnitudeOfMismatch
  37
  38open Classical
  39
  40/-! ## Single-Valuedness on the Unordered Pair -/
  41
  42/-- A comparison operator `C : K → K → Cost` is **single-valued on the
  43unordered pair** if it factors through the type of unordered pairs `Sym2 K`.
  44
  45Operationally: there is a single function `f` such that the cost
  46`C x y` is `f s(x, y)` and the order in which the arguments are
  47presented does not affect the value. -/
  48def SingleValuedOnUnorderedPair {K Cost : Type*} (C : K → K → Cost) : Prop :=
  49  ∃ f : Sym2 K → Cost, ∀ x y, C x y = f s(x, y)
  50
  51/-! ## Symmetry Forced by Single-Valuedness -/
  52
  53/-- **Single-valued predication forces symmetry.**
  54
  55If a comparison operator factors through the unordered pair, then the
  56order of its arguments does not matter. The asymmetric reading (where
  57`C x y` and `C y x` are different values) is not a single function on
  58pairs; it is two distinct directional functions. -/
  59theorem singleValued_implies_symmetric
  60    {K Cost : Type*} (C : K → K → Cost)
  61    (h : SingleValuedOnUnorderedPair C) :
  62    ∀ x y : K, C x y = C y x := by
  63  intro x y
  64  rcases h with ⟨f, hf⟩
  65  have hxy := hf x y
  66  have hyx := hf y x
  67  have hsym : (s(x, y) : Sym2 K) = s(y, x) := Sym2.eq_swap
  68  rw [hxy, hyx, hsym]
  69
  70/-- **Conversely: symmetric comparisons factor through unordered pairs.**
  71
  72Any symmetric function on `K × K` is the lift of a single function on
  73`Sym2 K`. So symmetry and single-valuedness on the unordered pair are
  74equivalent. -/
  75theorem symmetric_implies_factorsThrough
  76    {K Cost : Type*} (C : K → K → Cost)
  77    (hsymm : ∀ x y : K, C x y = C y x) :
  78    SingleValuedOnUnorderedPair C := by
  79  refine ⟨Sym2.lift ⟨fun a b => C a b, fun a b => hsymm a b⟩, ?_⟩
  80  intro x y
  81  simp [Sym2.lift_mk]
  82
  83/-- **Equivalence: single-valuedness on the unordered pair is symmetry.** -/
  84theorem singleValued_iff_symmetric
  85    {K Cost : Type*} (C : K → K → Cost) :
  86    SingleValuedOnUnorderedPair C ↔ ∀ x y : K, C x y = C y x :=
  87  ⟨singleValued_implies_symmetric C,
  88   fun h => symmetric_implies_factorsThrough C h⟩
  89
  90/-! ## Asymmetry Splits the Operator -/
  91
  92/-- The negation: if `C` is asymmetric on at least one pair, it cannot
  93factor through the unordered pair. Single-valuedness fails the moment the
  94two orderings give different values.
  95
  96This is the Lean form of Theorem 3 of the companion paper: asymmetry
  97splits a single binary function into two directional functions. -/
  98theorem asymmetric_not_singleValued
  99    {K Cost : Type*} (C : K → K → Cost)
 100    (h : ∃ x y : K, C x y ≠ C y x) :
 101    ¬ SingleValuedOnUnorderedPair C := by
 102  rintro hSV
 103  rcases h with ⟨x, y, hxy⟩
 104  exact hxy (singleValued_implies_symmetric C hSV x y)
 105
 106/-! ## Connection to PrimitiveDistinction
 107
 108The `PrimitiveDistinction.equalityCost` is the canonical equality-induced
 109cost. By the equivalence above, it is single-valued on the unordered pair
 110iff it is symmetric — and `non_contradiction_from_equality` already proves
 111symmetry of the equality-induced cost. So the equality-induced cost is in
 112the canonical magnitude-of-mismatch shape automatically, with no further
 113choice. -/
 114
 115open IndisputableMonolith.Foundation.PrimitiveDistinction
 116
 117/-- The equality-induced cost is single-valued on the unordered pair. -/
 118theorem equalityCost_singleValued (K : Type*) (weight : ℝ) :
 119    SingleValuedOnUnorderedPair (equalityCost K weight) :=
 120  symmetric_implies_factorsThrough (equalityCost K weight)
 121    (non_contradiction_from_equality K weight)
 122
 123/-! ## Headline: Magnitude-of-Mismatch is Forced
 124
 125Combining the two directions, the magnitude-of-mismatch encoding of (L2)
 126(symmetry) is the unique encoding consistent with treating a comparison
 127as a single-valued predicate on a distinguished pair.
 128
 129Asymmetric ("directed revision") readings are not single binary functions;
 130they are two-valued, hence multi-valued by the standard meaning of
 131single-valuedness. The Aristotelian Non-Contradiction reading on operator
 132structure forces symmetry.
 133-/
 134
 135/-- **Magnitude-of-Mismatch theorem (combined).**
 136
 137On any carrier and cost type, a comparison operator is single-valued on
 138the unordered pair if and only if it satisfies (L2) Non-Contradiction
 139in operator form (`C x y = C y x`). The two are equivalent statements;
 140neither is more primitive than the other. The asymmetric reading of
 141Non-Contradiction does not produce a single comparison operator. -/
 142theorem magnitude_of_mismatch_forced
 143    {K Cost : Type*} (C : K → K → Cost) :
 144    SingleValuedOnUnorderedPair C ↔ ∀ x y : K, C x y = C y x :=
 145  singleValued_iff_symmetric C
 146
 147end MagnitudeOfMismatch
 148end Foundation
 149end IndisputableMonolith
 150