recognition / Foundation / Foundation.LogicAsFunctionalEquation.OperativeDomain / rcl_logic_reality_chain

theorem

`rcl_logic_reality_chain`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

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

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.

depends on

used by

operative_domain_rcl_logic_reality_chain IndisputableMonolith.Foundation.LogicAsFunctionalEquation.MainTheorem

formal source

  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.