IndisputableMonolith.Foundation.LogicAsFunctionalEquation.FiniteLogicalComparison

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.CountOnceComparison
   3import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.RealityStructure
   4
   5/-!
   6# Finite logical comparison
   7
   8This module packages the paper's sharpened theorem:
   9
  10finite logical comparison on positive ratios forces the RCL family.
  11
  12The finite-pairwise-polynomial condition is not removed; it is named as the
  13finite algebraic content of logical comparison.  The counterexamples prove why
  14that finite condition is necessary.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Foundation
  19namespace LogicAsFunctionalEquation
  20
  21open IndisputableMonolith.Foundation.DAlembert.Inevitability
  22
  23/-- A finite logical comparison is a truth-evaluable positive-ratio comparison
  24whose composite value is determined by a finite pairwise polynomial algebra. -/
  25structure FiniteLogicalComparison (C : ComparisonOperator) : Prop where
  26  identity : Identity C
  27  non_contradiction : NonContradiction C
  28  totality : ExcludedMiddle C
  29  scale_invariant : ScaleInvariant C
  30  nontrivial : NonTrivial C
  31  counted_once_algebra : CountedOnceComposition C
  32
  33/-- Finite logical comparison supports truth-evaluable comparison. -/
  34theorem finite_logical_to_truth_evaluable
  35    (C : ComparisonOperator)
  36    (h : FiniteLogicalComparison C) :
  37    TruthEvaluableComparison C where
  38  self_evaluable := h.identity
  39  reorder_single_valued := h.non_contradiction
  40  determinate_continuous := h.totality
  41  composite_determinate := counted_once_to_finite_pairwise_polynomial C h.counted_once_algebra
  42  scale_free := h.scale_invariant
  43  nontrivial := h.nontrivial
  44
  45/-- Finite logical comparison is operative positive-ratio comparison. -/
  46theorem finite_logical_to_operative
  47    (C : ComparisonOperator)
  48    (h : FiniteLogicalComparison C) :
  49    OperativePositiveRatioComparison C where
  50  identity := h.identity
  51  non_contradiction := h.non_contradiction
  52  continuous := h.totality
  53  scale_invariant := h.scale_invariant
  54  non_trivial := h.nontrivial
  55
  56/-- Finite logical comparison carries finite pairwise polynomial closure. -/
  57theorem finite_logical_has_finite_closure
  58    (C : ComparisonOperator)
  59    (h : FiniteLogicalComparison C) :
  60    FinitePairwisePolynomialClosure C :=
  61  counted_once_to_finite_pairwise_polynomial C h.counted_once_algebra
  62
  63/-- Finite logical comparison carries counted-once composition. -/
  64theorem finite_logical_has_counted_once
  65    (C : ComparisonOperator)
  66    (h : FiniteLogicalComparison C) :
  67    CountedOnceComposition C :=
  68  h.counted_once_algebra
  69
  70/-- Finite logical comparison satisfies the encoded laws of logic. -/
  71theorem finite_logical_satisfies_laws
  72    (C : ComparisonOperator)
  73    (h : FiniteLogicalComparison C) :
  74    SatisfiesLawsOfLogic C :=
  75  operative_to_laws_of_logic C
  76    (finite_logical_to_operative C h)
  77    (finite_logical_has_finite_closure C h)
  78
  79/-- Finite logical comparison on positive ratios forces the RCL family. -/
  80theorem finite_logical_comparison_forces_rcl
  81    (C : ComparisonOperator)
  82    (h : FiniteLogicalComparison C) :
  83    RCLFamily (derivedCost C) :=
  84  counted_once_combiner_forces_rcl C
  85    (finite_logical_to_operative C h)
  86    (finite_logical_has_counted_once C h)
  87
  88/-- Searchable boundary theorem: arbitrary continuous composition is not enough
  89to force the RCL family. -/
  90theorem continuous_composition_not_enough :
  91    ¬ ∃ c : ℝ, ∀ a b : ℝ, 0 < a → 0 < b →
  92      quarticCombiner a b = 2 * a + 2 * b + c * a * b :=
  93  quarticCombiner_not_rcl_family
  94
  95/-- Searchable boundary theorem: analytic composition is not enough to force
  96degree-two RCL form. -/
  97theorem analytic_composition_not_enough :
  98    ¬ ∃ c : ℝ, ∀ s : ℝ, reparamDiagonal s = degreeTwoDiagonal c s :=
  99  reparam_diagonal_not_degree_two
 100
 101end LogicAsFunctionalEquation
 102end Foundation
 103end IndisputableMonolith
 104