IndisputableMonolith.Foundation.LedgerComparisonToComposition

   1import IndisputableMonolith.Cost.FunctionalEquation
   2import IndisputableMonolith.Foundation.ClosedObservableFramework
   3import IndisputableMonolith.Foundation.LedgerCompositionToJCost
   4import IndisputableMonolith.Foundation.DAlembert.Ultimate
   5
   6/-!
   7# Positive-ratio comparison and factorization existence from the ledger (Phase 3)
   8
   9Two Phase 3 checklist items remained after `LedgerCompositionToJCost` discharged
  10the "apply `law_of_logic_forces_jcost`" step:
  11
  12* **Derive positive-ratio comparison from ledger**: the object the recognition
  13  cost `J` is applied to (the comparison between two observable states) is a
  14  *positive ratio*, with reciprocal symmetry under state swap.
  15* **Derive factorization/composition from ledger**: the existence of a binary
  16  combiner `P` with `F(x·y) + F(x/y) = P(F x, F y)` (the d'Alembert factorization
  17  input, `HasMultiplicativeConsistency`) was *assumed*, not derived.
  18
  19This module closes both honestly.
  20
  21## Positive-ratio comparison
  22
  23A `ClosedObservableFramework` carries a strictly positive observable `r : S → ℝ`.
  24The comparison between two states is the ratio `r s₁ / r s₂`, which is
  25
  26* strictly positive (`compRatio_pos`), so the *domain* of `J` is exactly the
  27  positive ray, not assumed but read off `r_pos`;
  28* inverted by the state swap (`compRatio_swap`), so a reciprocal-symmetric cost
  29  is swap-invariant (`comparison_cost_swap_invariant`): this is `IsReciprocalCost`
  30  realized on the ledger;
  31* unital at self-comparison (`compRatio_self`), so a normalized cost vanishes on
  32  self-comparison (`comparison_cost_self_zero`): this is `IsNormalized`.
  33
  34## Factorization existence is a well-definedness condition
  35
  36`HasMultiplicativeConsistency F` is, by definition, `∃ P, CostComposesThrough F P`.
  37We prove it is *equivalent* to the combination being **cost-determined**: the value
  38`F(x·y) + F(x/y)` depends only on the pair of single-point costs `(F x, F y)`
  39(`hasMultiplicativeConsistency_iff_costDetermined`).  So the factorization combiner
  40is not an arbitrary analytic input; it exists exactly when the symmetric
  41combination is a function of the costs alone, which is the ledger-native
  42well-definedness condition already appearing as the `hJ_suff` field of
  43`ClosedFramework.ledger_reconstruction`.  Combined with
  44`LedgerCompositionToJCost`, a comparison cost whose combination is cost-determined
  45*through a ledger-posting combiner* is forced to be `J`.
  46
  47Non-vacuity: `J`'s own combination is cost-determined
  48(`jcost_combinationCostDetermined`), since `J` composes through `rclCombiner`.
  49
  50Status: 0 sorry, 0 new axiom.
  51-/
  52
  53namespace IndisputableMonolith
  54namespace Foundation
  55namespace LedgerComparisonToComposition
  56
  57open ClosedFramework
  58open Cost.FunctionalEquation
  59open DAlembert.FactorizationForcing
  60open LedgerCompositionToJCost
  61
  62/-! ## Positive-ratio comparison from the ledger -/
  63
  64/-- The comparison ratio between two observable states of a closed framework. -/
  65noncomputable def compRatio (F : ClosedObservableFramework) (s₁ s₂ : F.S) : ℝ :=
  66  F.r s₁ / F.r s₂
  67
  68/-- **The comparison object is a positive ratio.**  Read off the framework's
  69strictly positive observable `r`: the domain of the recognition cost is the
  70positive ray, derived rather than assumed. -/
  71theorem compRatio_pos (F : ClosedObservableFramework) (s₁ s₂ : F.S) :
  72    0 < compRatio F s₁ s₂ :=
  73  div_pos (F.r_pos s₁) (F.r_pos s₂)
  74
  75/-- **State swap inverts the comparison ratio.**  Swapping the two states sends the
  76ratio to its reciprocal, the geometric origin of reciprocal symmetry. -/
  77theorem compRatio_swap (F : ClosedObservableFramework) (s₁ s₂ : F.S) :
  78    compRatio F s₂ s₁ = (compRatio F s₁ s₂)⁻¹ := by
  79  unfold compRatio
  80  rw [inv_div]
  81
  82/-- **Self-comparison is the unit ratio.** -/
  83theorem compRatio_self (F : ClosedObservableFramework) (s : F.S) :
  84    compRatio F s s = 1 :=
  85  div_self (ne_of_gt (F.r_pos s))
  86
  87/-- **Reciprocal symmetry realized on the ledger.**  A reciprocal-symmetric cost
  88assigns equal cost to a comparison and its state-swap, because the swap inverts the
  89positive ratio. -/
  90theorem comparison_cost_swap_invariant (F : ClosedObservableFramework)
  91    (J : ℝ → ℝ) (hJ : IsReciprocalCost J) (s₁ s₂ : F.S) :
  92    J (compRatio F s₁ s₂) = J (compRatio F s₂ s₁) := by
  93  rw [compRatio_swap F s₁ s₂]
  94  exact hJ (compRatio F s₁ s₂) (compRatio_pos F s₁ s₂)
  95
  96/-- **Normalization realized on the ledger.**  A normalized cost vanishes on
  97self-comparison, since self-comparison is the unit ratio. -/
  98theorem comparison_cost_self_zero (F : ClosedObservableFramework)
  99    (J : ℝ → ℝ) (hJ : IsNormalized J) (s : F.S) :
 100    J (compRatio F s s) = 0 := by
 101  rw [compRatio_self]
 102  exact hJ
 103
 104/-! ## Factorization existence is the cost-determined-combination condition -/
 105
 106/-- The symmetric combination of a cost `F` is **cost-determined** if its value
 107`F(x·y) + F(x/y)` depends only on the pair of single-point costs `(F x, F y)`.
 108This is the ledger-native well-definedness condition (the `hJ_suff` field of
 109`ledger_reconstruction`, in its joint form). -/
 110def CombinationCostDetermined (F : ℝ → ℝ) : Prop :=
 111  ∀ x₁ y₁ x₂ y₂ : ℝ, 0 < x₁ → 0 < y₁ → 0 < x₂ → 0 < y₂ →
 112    F x₁ = F x₂ → F y₁ = F y₂ →
 113    F (x₁ * y₁) + F (x₁ / y₁) = F (x₂ * y₂) + F (x₂ / y₂)
 114
 115/-- **Factorization existence ⇔ cost-determined combination.**  A comparison cost
 116admits a binary combiner `P` with `F(x·y) + F(x/y) = P(F x, F y)` (the d'Alembert
 117`HasMultiplicativeConsistency` factorization input) **iff** its symmetric
 118combination is cost-determined.  So the combiner is not an arbitrary analytic
 119assumption: it exists exactly when the combination is a function of the costs
 120alone.  The reverse direction builds `P` by choosing, for each cost pair in the
 121image, a witnessing ratio pair; cost-determinedness makes the choice irrelevant. -/
 122theorem hasMultiplicativeConsistency_iff_costDetermined (F : ℝ → ℝ) :
 123    DAlembert.Ultimate.HasMultiplicativeConsistency F ↔ CombinationCostDetermined F := by
 124  constructor
 125  · rintro ⟨P, hP⟩ x₁ y₁ x₂ y₂ hx₁ hy₁ hx₂ hy₂ hFx hFy
 126    rw [hP x₁ y₁ hx₁ hy₁, hP x₂ y₂ hx₂ hy₂, hFx, hFy]
 127  · intro hdet
 128    classical
 129    refine ⟨fun u v =>
 130      if h : ∃ p : ℝ × ℝ, 0 < p.1 ∧ 0 < p.2 ∧ F p.1 = u ∧ F p.2 = v
 131      then F (h.choose.1 * h.choose.2) + F (h.choose.1 / h.choose.2)
 132      else 0, ?_⟩
 133    intro x y hx hy
 134    have hex : ∃ p : ℝ × ℝ, 0 < p.1 ∧ 0 < p.2 ∧ F p.1 = F x ∧ F p.2 = F y :=
 135      ⟨(x, y), hx, hy, rfl, rfl⟩
 136    show F (x * y) + F (x / y) =
 137      (if h : ∃ p : ℝ × ℝ, 0 < p.1 ∧ 0 < p.2 ∧ F p.1 = F x ∧ F p.2 = F y
 138        then F (h.choose.1 * h.choose.2) + F (h.choose.1 / h.choose.2)
 139        else 0)
 140    rw [dif_pos hex]
 141    obtain ⟨hp1, hp2, hpx, hpy⟩ := hex.choose_spec
 142    exact (hdet hex.choose.1 hex.choose.2 x y hp1 hp2 hx hy hpx hpy).symm
 143
 144/-- `HasMultiplicativeConsistency F` is definitionally `∃ P, CostComposesThrough F P`:
 145the factorization input is exactly "the cost composes through some combiner". -/
 146theorem hasMultiplicativeConsistency_iff_exists_composesThrough (F : ℝ → ℝ) :
 147    DAlembert.Ultimate.HasMultiplicativeConsistency F ↔
 148      ∃ P : ℝ → ℝ → ℝ, CostComposesThrough F P :=
 149  Iff.rfl
 150
 151/-! ## Non-vacuity: `J`'s combination is cost-determined -/
 152
 153/-- **`J`'s combination is cost-determined.**  Since `J` composes through
 154`rclCombiner`, its symmetric combination is a function of the single-point costs,
 155so the factorization-existence condition is non-vacuous. -/
 156theorem jcost_combinationCostDetermined :
 157    CombinationCostDetermined Cost.Jcost :=
 158  (hasMultiplicativeConsistency_iff_costDetermined Cost.Jcost).mp
 159    ⟨rclCombiner, jcost_composesThrough_rclCombiner⟩
 160
 161/-! ## Phase 3 composite: cost-determined through a ledger combiner forces `J` -/
 162
 163/-- **Phase 3 composite.**  A comparison cost that is reciprocal, normalized,
 164calibrated, and continuous, whose symmetric combination is realized through a
 165primitive ledger-posting combiner with per-slice directional regularity, is forced
 166to be `J`.  The factorization combiner is supplied through the ledger (so it is
 167forced to `rclCombiner`), the composition law follows, and
 168`law_of_logic_forces_jcost` finishes, with no analytic composition-law hypothesis
 169assumed. -/
 170theorem ledgerComparison_forces_jcost
 171    (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
 172    (hRecip : IsReciprocalCost F) (hNorm : IsNormalized F)
 173    (hCalib : IsCalibrated F) (hCont : ContinuousOn F (Set.Ioi 0))
 174    (hP : LedgerToFactorization.PrimitiveLedgerPostingSemantics P)
 175    (hdir : ∀ u, Monotone (fun v => P u v) ∨ Antitone (fun v => P u v))
 176    (hCompose : CostComposesThrough F P) :
 177    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x :=
 178  ledgerComposition_forces_jcost F P hRecip hNorm hCalib hCont hP hdir hCompose
 179
 180/-! ## Certificate -/
 181
 182/-- The Phase 3 comparison/factorization closure certificate. -/
 183structure LedgerComparisonCertificate : Prop where
 184  /-- The comparison object is a strictly positive ratio of observables. -/
 185  comparison_is_positive_ratio :
 186    ∀ (F : ClosedObservableFramework) (s₁ s₂ : F.S), 0 < compRatio F s₁ s₂
 187  /-- State swap inverts the comparison ratio (reciprocal symmetry origin). -/
 188  comparison_swap_inverts :
 189    ∀ (F : ClosedObservableFramework) (s₁ s₂ : F.S),
 190      compRatio F s₂ s₁ = (compRatio F s₁ s₂)⁻¹
 191  /-- Self-comparison is the unit ratio (normalization origin). -/
 192  comparison_self_unit :
 193    ∀ (F : ClosedObservableFramework) (s : F.S), compRatio F s s = 1
 194  /-- Factorization existence is equivalent to the combination being
 195  cost-determined. -/
 196  factorization_iff_cost_determined :
 197    ∀ F : ℝ → ℝ,
 198      DAlembert.Ultimate.HasMultiplicativeConsistency F ↔ CombinationCostDetermined F
 199  /-- `J`'s combination is cost-determined (non-vacuity). -/
 200  jcost_cost_determined : CombinationCostDetermined Cost.Jcost
 201
 202/-- The Phase 3 comparison/factorization certificate holds. -/
 203theorem ledgerComparisonCertificate : LedgerComparisonCertificate where
 204  comparison_is_positive_ratio := compRatio_pos
 205  comparison_swap_inverts := compRatio_swap
 206  comparison_self_unit := compRatio_self
 207  factorization_iff_cost_determined := hasMultiplicativeConsistency_iff_costDetermined
 208  jcost_cost_determined := jcost_combinationCostDetermined
 209
 210end LedgerComparisonToComposition
 211end Foundation
 212end IndisputableMonolith
 213