IndisputableMonolith.Foundation.LogicAsFunctionalEquation.OperativeDomain

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.FiniteLogicalComparison
   3
   4/-!
   5# Operative-domain identification
   6
   7This module packages the formal chain:
   8
   9finite logical comparison on positive ratios
  10  → encoded logical comparison
  11  → RCL family.
  12
  13This is the Lean counterpart of the paper's operative-domain corollary.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Foundation
  18namespace LogicAsFunctionalEquation
  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
  51