IndisputableMonolith.Foundation.LogicAsFunctionalEquation.Canonicality

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.DirectProof
   3
   4/-!
   5# Canonicality of the logic encoding
   6
   7This module formalises the paper's canonicality step at the level Lean can
   8check: once a comparison operator is read as a magnitude of mismatch, the
   9operator-level conditions used in `LogicAsFunctionalEquation` are the
  10canonical structural content of that reading.
  11
  12Lean verifies the implication from the magnitude-of-mismatch package to the
  13encoded logical conditions.  The philosophical claim that this package is the
  14right reading of Aristotle is documented in the paper, not proved by Lean.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Foundation
  19namespace LogicAsFunctionalEquation
  20
  21/-- The magnitude-of-mismatch interpretation of a comparison operator.
  22
  23The fields correspond to:
  24* trivial value at match,
  25* symmetry of the unordered pair,
  26* total/continuous determinability,
  27* scale-free comparison,
  28* nontriviality.
  29
  30Finite pairwise polynomial closure is kept separate: it is not part of the
  31interpretation itself, but the finite-algebra condition needed to force RCL. -/
  32structure MagnitudeOfMismatch (C : ComparisonOperator) : Prop where
  33  trivial_at_match : Identity C
  34  pair_symmetric : NonContradiction C
  35  determinate_continuous : ExcludedMiddle C
  36  scale_free : ScaleInvariant C
  37  nontrivial : NonTrivial C
  38
  39/-- The magnitude-of-mismatch interpretation determines the operative
  40positive-ratio comparison structure. -/
  41theorem mismatch_to_operative
  42    (C : ComparisonOperator)
  43    (hM : MagnitudeOfMismatch C) :
  44    OperativePositiveRatioComparison C where
  45  identity := hM.trivial_at_match
  46  non_contradiction := hM.pair_symmetric
  47  continuous := hM.determinate_continuous
  48  scale_invariant := hM.scale_free
  49  non_trivial := hM.nontrivial
  50
  51/-- Under the magnitude-of-mismatch interpretation, identity is exactly the
  52zero self-cost condition used in the logic encoding. -/
  53theorem canonical_identity
  54    (C : ComparisonOperator)
  55    (hM : MagnitudeOfMismatch C) :
  56    Identity C :=
  57  hM.trivial_at_match
  58
  59/-- Under the magnitude-of-mismatch interpretation, non-contradiction is
  60encoded as symmetric single-valued comparison. -/
  61theorem canonical_non_contradiction
  62    (C : ComparisonOperator)
  63    (hM : MagnitudeOfMismatch C) :
  64    NonContradiction C :=
  65  hM.pair_symmetric
  66
  67/-- Under the magnitude-of-mismatch interpretation, excluded middle on the
  68continuous positive quadrant is encoded as determinate continuous comparison. -/
  69theorem canonical_excluded_middle
  70    (C : ComparisonOperator)
  71    (hM : MagnitudeOfMismatch C) :
  72    ExcludedMiddle C :=
  73  hM.determinate_continuous
  74
  75/-- Under the magnitude-of-mismatch interpretation, the scale-free character
  76of logical comparison gives the scale-invariance bridge. -/
  77theorem canonical_scale_invariance
  78    (C : ComparisonOperator)
  79    (hM : MagnitudeOfMismatch C) :
  80    ScaleInvariant C :=
  81  hM.scale_free
  82
  83/-- The canonical encoding, packaged: a magnitude-of-mismatch comparison plus
  84finite pairwise polynomial closure satisfies the Level-1 `SatisfiesLawsOfLogic`
  85structure. -/
  86theorem canonicality_of_encoding
  87    (C : ComparisonOperator)
  88    (hM : MagnitudeOfMismatch C)
  89    (hFinite : FinitePairwisePolynomialClosure C) :
  90    SatisfiesLawsOfLogic C :=
  91  operative_to_laws_of_logic C (mismatch_to_operative C hM) hFinite
  92
  93/-- The RCL family follows from the canonical magnitude-of-mismatch reading
  94plus finite pairwise polynomial closure. -/
  95theorem rcl_from_canonical_mismatch_encoding
  96    (C : ComparisonOperator)
  97    (hM : MagnitudeOfMismatch C)
  98    (hFinite : FinitePairwisePolynomialClosure C) :
  99    ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
 100      DAlembert.Inevitability.HasMultiplicativeConsistency (derivedCost C) P ∧
 101      (∀ u v, P u v = 2 * u + 2 * v + c * u * v) :=
 102  rcl_polynomial_closure_theorem C (mismatch_to_operative C hM) hFinite
 103
 104end LogicAsFunctionalEquation
 105end Foundation
 106end IndisputableMonolith
 107