theorem
proved
truth_eval_implies_non_contradiction
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.LogicAsFunctionalEquation.RealityStructure on GitHub at line 41.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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