`truth_eval_implies_composition`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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) :

papers checked against this theorem

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