IndisputableMonolith.Foundation.LogicAsFunctionalEquation.NoHiddenState

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge
   3
   4/-!
   5# No-hidden-state comparison composition
   6
   7No-hidden-state composition means the composite cost is supplied by a
   8counted-once resource expression in the two constituent costs.  This is a
   9formal version of "no hidden route memory, no branch choice, no infinite
  10series, and no reuse of a constituent comparison."
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Foundation
  15namespace LogicAsFunctionalEquation
  16
  17/-- A no-hidden-state composition law for `C`: there is a counted-once resource
  18expression whose evaluation on the two constituent costs gives the composite
  19cost. -/
  20structure NoHiddenStateComposition (C : ComparisonOperator) where
  21  expr : CountedOnceResourceExpr
  22  symmetric_expr : ∀ u v, CountedOnceResourceExpr.eval expr u v =
  23    CountedOnceResourceExpr.eval expr v u
  24  composition : ∀ x y : ℝ, 0 < x → 0 < y →
  25    derivedCost C (x * y) + derivedCost C (x / y) =
  26      CountedOnceResourceExpr.eval expr (derivedCost C x) (derivedCost C y)
  27
  28/-- No-hidden-state composition implies counted-once composition. -/
  29theorem no_hidden_state_implies_counted_once
  30    (C : ComparisonOperator)
  31    (h : NoHiddenStateComposition C) :
  32    CountedOnceComposition C := by
  33  refine ⟨fun u v => CountedOnceResourceExpr.eval h.expr u v, ?_, ?_, ?_⟩
  34  · exact CountedOnceResourceExpr.expr_induces_counted_once_combiner h.expr
  35  · exact h.symmetric_expr
  36  · exact h.composition
  37
  38/-- A no-hidden-state operative comparison forces the RCL family. -/
  39theorem no_hidden_state_comparison_forces_rcl
  40    (C : ComparisonOperator)
  41    (hOp : OperativePositiveRatioComparison C)
  42    (h : NoHiddenStateComposition C) :
  43    RCLFamily (derivedCost C) :=
  44  counted_once_combiner_forces_rcl C hOp
  45    (no_hidden_state_implies_counted_once C h)
  46
  47end LogicAsFunctionalEquation
  48end Foundation
  49end IndisputableMonolith
  50