`FiniteLogicalComparison`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.LogicAsFunctionalEquation.FiniteLogicalComparison
domain: Foundation
line: 25 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.FiniteLogicalComparison on GitHub at line 25.

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

  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

papers checked against this theorem

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