IndisputableMonolith.Foundation.LogicAsFunctionalEquation.MainTheorem

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.PositiveRatioForcing
   3import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.NoHiddenState
   4import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.OperativeDomain
   5
   6/-!
   7# Main theorem package for logic as functional equation
   8
   9This module collects the formal chain closest to the paper's headline:
  10
  11* scale-free comparison factors through positive ratios;
  12* no-hidden-state finite comparison gives counted-once composition;
  13* counted-once finite logical comparison forces the RCL family.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Foundation
  18namespace LogicAsFunctionalEquation
  19
  20/-- No-hidden-state operative comparison forces the RCL family. -/
  21theorem no_hidden_state_logic_forces_rcl
  22    (C : ComparisonOperator)
  23    (hOp : OperativePositiveRatioComparison C)
  24    (hNoHidden : NoHiddenStateComposition C) :
  25    RCLFamily (derivedCost C) :=
  26  no_hidden_state_comparison_forces_rcl C hOp hNoHidden
  27
  28/-- Counted-once finite logical comparison on positive ratios is RCL algebra. -/
  29theorem rcl_is_counted_once_logic_on_positive_ratios
  30    (C : ComparisonOperator)
  31    (h : FiniteLogicalComparison C) :
  32    RCLFamily (derivedCost C) :=
  33  finite_logical_comparison_forces_rcl C h
  34
  35/-- The operative-domain chain: encoded logic plus RCL family. -/
  36theorem operative_domain_rcl_logic_reality_chain
  37    (C : ComparisonOperator)
  38    (h : OperativeDomainStructure C) :
  39    SatisfiesLawsOfLogic C ∧ RCLFamily (derivedCost C) :=
  40  rcl_logic_reality_chain C h
  41
  42/-- Scale-free counted-once logical comparison factors through ratios and
  43then forces RCL on the derived cost. -/
  44theorem scale_free_counted_once_logic_forces_ratio_rcl
  45    (C : ComparisonOperator)
  46    (h : FiniteLogicalComparison C) :
  47    (∃ F : ℝ → ℝ, ∀ x y : ℝ, 0 < x → 0 < y → C x y = F (x / y)) ∧
  48    RCLFamily (derivedCost C) := by
  49  exact ⟨scale_free_comparison_factors_through_ratio C h.scale_invariant,
  50    finite_logical_comparison_forces_rcl C h⟩
  51
  52/-- Final theorem-name alias: RCL is scale-free counted-once logic on positive
  53ratios. -/
  54theorem rcl_is_scale_free_counted_once_logic_on_positive_ratios
  55    (C : ComparisonOperator)
  56    (h : FiniteLogicalComparison C) :
  57    (∃ F : ℝ → ℝ, ∀ x y : ℝ, 0 < x → 0 < y → C x y = F (x / y)) ∧
  58    RCLFamily (derivedCost C) :=
  59  scale_free_counted_once_logic_forces_ratio_rcl C h
  60
  61end LogicAsFunctionalEquation
  62end Foundation
  63end IndisputableMonolith
  64