`OperativeDomainStructure`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.LogicAsFunctionalEquation.OperativeDomain
domain: Foundation
line: 22 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.OperativeDomain on GitHub at line 22.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  19
  20/-- An operative-domain structure is finite logical comparison on the
  21continuous positive-ratio setting. -/
  22def OperativeDomainStructure (C : ComparisonOperator) : Prop :=
  23  FiniteLogicalComparison C
  24
  25/-- Operative-domain structures satisfy the encoded laws of logic. -/
  26theorem operative_domain_satisfies_logic
  27    (C : ComparisonOperator)
  28    (hO : OperativeDomainStructure C) :
  29    SatisfiesLawsOfLogic C :=
  30  finite_logical_satisfies_laws C hO
  31
  32/-- Operative-domain structures force the RCL family on the derived cost. -/
  33theorem operative_domain_identification
  34    (C : ComparisonOperator)
  35    (hO : OperativeDomainStructure C) :
  36    RCLFamily (derivedCost C) :=
  37  finite_logical_comparison_forces_rcl C hO
  38
  39/-- Headline corollary: on the operative domain, logical comparison and the
  40RCL family have the same forced algebraic form. -/
  41theorem rcl_logic_reality_chain
  42    (C : ComparisonOperator)
  43    (hO : OperativeDomainStructure C) :
  44    SatisfiesLawsOfLogic C ∧ RCLFamily (derivedCost C) := by
  45  exact ⟨operative_domain_satisfies_logic C hO,
  46    operative_domain_identification C hO⟩
  47
  48end LogicAsFunctionalEquation
  49end Foundation
  50end IndisputableMonolith

papers checked against this theorem

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