IndisputableMonolith.Foundation.LogicAsFunctionalEquation.RealityStructure

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.Canonicality
   3
   4/-!
   5# Truth-evaluable reality structures
   6
   7This module formalises the "Reality ⇒ Logic" leg used by the Logic Functional
   8Equation paper.  The starting point is a comparison operator whose values are
   9truth-evaluable: self-comparison has a trivial value, reordering is
  10single-valued, every positive pair has a determinate continuous comparison,
  11and composite comparisons have a determinate finite pairwise combiner.
  12
  13Lean verifies the object-level implication from truth-evaluability to the
  14encoded logical conditions (L1)--(L4).
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Foundation
  19namespace LogicAsFunctionalEquation
  20
  21/-- A truth-evaluable comparison is the minimal structure needed to evaluate
  22statements about positive-ratio comparisons.  The four fields are stated in
  23semantic language; the lemmas below translate them into (L1)--(L4). -/
  24structure TruthEvaluableComparison (C : ComparisonOperator) : Prop where
  25  self_evaluable : ∀ x : ℝ, 0 < x → C x x = 0
  26  reorder_single_valued : ∀ x y : ℝ, 0 < x → 0 < y → C x y = C y x
  27  determinate_continuous :
  28    ContinuousOn (Function.uncurry C) (Set.Ioi (0 : ℝ) ×ˢ Set.Ioi (0 : ℝ))
  29  composite_determinate : FinitePairwisePolynomialClosure C
  30  scale_free : ScaleInvariant C
  31  nontrivial : NonTrivial C
  32
  33/-- Truth-evaluability of self-statements gives identity. -/
  34theorem truth_eval_implies_identity
  35    (C : ComparisonOperator)
  36    (hT : TruthEvaluableComparison C) :
  37    Identity C :=
  38  hT.self_evaluable
  39
  40/-- Truth-evaluability of reordered pair-statements gives non-contradiction. -/
  41theorem truth_eval_implies_non_contradiction
  42    (C : ComparisonOperator)
  43    (hT : TruthEvaluableComparison C) :
  44    NonContradiction C :=
  45  hT.reorder_single_valued
  46
  47/-- Truth-evaluability of every positive pair gives totality/continuity on the
  48open positive quadrant. -/
  49theorem truth_eval_implies_totality
  50    (C : ComparisonOperator)
  51    (hT : TruthEvaluableComparison C) :
  52    ExcludedMiddle C :=
  53  hT.determinate_continuous
  54
  55/-- Truth-evaluability of composite comparison-statements gives finite pairwise
  56composition. -/
  57theorem truth_eval_implies_composition
  58    (C : ComparisonOperator)
  59    (hT : TruthEvaluableComparison C) :
  60    FinitePairwisePolynomialClosure C :=
  61  hT.composite_determinate
  62
  63/-- Truth-evaluable comparisons are operative positive-ratio comparisons. -/
  64theorem truth_eval_to_operative
  65    (C : ComparisonOperator)
  66    (hT : TruthEvaluableComparison C) :
  67    OperativePositiveRatioComparison C where
  68  identity := truth_eval_implies_identity C hT
  69  non_contradiction := truth_eval_implies_non_contradiction C hT
  70  continuous := truth_eval_implies_totality C hT
  71  scale_invariant := hT.scale_free
  72  non_trivial := hT.nontrivial
  73
  74/-- Truth-evaluable comparisons satisfy the encoded laws of logic. -/
  75theorem reality_satisfies_logic
  76    (C : ComparisonOperator)
  77    (hT : TruthEvaluableComparison C) :
  78    SatisfiesLawsOfLogic C :=
  79  operative_to_laws_of_logic C
  80    (truth_eval_to_operative C hT)
  81    (truth_eval_implies_composition C hT)
  82
  83/-- Consequently, truth-evaluable finite pairwise positive-ratio comparison
  84forces the RCL family. -/
  85theorem rcl_from_truth_evaluable_comparison
  86    (C : ComparisonOperator)
  87    (hT : TruthEvaluableComparison C) :
  88    ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
  89      DAlembert.Inevitability.HasMultiplicativeConsistency (derivedCost C) P ∧
  90      (∀ u v, P u v = 2 * u + 2 * v + c * u * v) :=
  91  rcl_polynomial_closure_theorem C
  92    (truth_eval_to_operative C hT)
  93    (truth_eval_implies_composition C hT)
  94
  95end LogicAsFunctionalEquation
  96end Foundation
  97end IndisputableMonolith
  98