`rcl_from_truth_evaluable_comparison`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.LogicAsFunctionalEquation.RealityStructure
domain: Foundation
line: 85 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.RealityStructure on GitHub at line 85.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.