theorem
proved
truth_eval_to_operative
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.LogicAsFunctionalEquation.RealityStructure on GitHub at line 64.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
nontrivial -
of -
of -
ComparisonOperator -
OperativePositiveRatioComparison -
truth_eval_implies_identity -
truth_eval_implies_non_contradiction -
truth_eval_implies_totality -
TruthEvaluableComparison -
identity -
of -
of -
of -
identity
used by
formal source
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