IndisputableMonolith.Foundation.LedgerCompositionToJCost

   1import IndisputableMonolith.Cost.FunctionalEquation
   2import IndisputableMonolith.Cost.AczelProof
   3import IndisputableMonolith.Foundation.LedgerToFactorization
   4
   5/-!
   6# Ledger composition forces the recognition cost `J` (Phase 3 endpoint)
   7
   8The Phase 3 checklist item "Apply `law_of_logic_forces_jcost`" was flagged
   9because `law_of_logic_forces_jcost` exists but its `SatisfiesCompositionLaw F`
  10hypothesis was *assumed*, not derived from the recognition ledger.
  11
  12This module closes that gap structurally.  The composition law
  13
  14  `F (x·y) + F (x/y) = 2 F x F y + 2 F x + 2 F y`
  15
  16is, term for term, the statement that the cost's own two-point combiner
  17`(x, y) ↦ F (x·y) + F (x/y)` equals the RCL combiner `rclCombiner` evaluated at
  18the costs `(F x, F y)` (`rclCombiner u v = 2uv + 2u + 2v`).  So the composition
  19law is *not* an independent analytic input: it is exactly
  20
  21  "the recognition cost composes through the RCL combiner".
  22
  23Phase 3's directional ledger theorem
  24(`LedgerToFactorization.primitiveLedgerPosting_directional_forces_rcl`) already
  25forces *any* primitive ledger-posting combiner with per-slice directional
  26regularity to equal `rclCombiner`.  Composing the two:
  27
  28* if `F` composes through *some* combiner `P` (the factorization/composability
  29  input), and
  30* `P` satisfies primitive ledger posting with directional regularity,
  31
  32then `P = rclCombiner`, hence `SatisfiesCompositionLaw F`, hence — feeding the
  33remaining reciprocal/normalized/calibrated/continuous hypotheses into
  34`law_of_logic_forces_jcost` — `F = J`.
  35
  36The `SatisfiesCompositionLaw` hypothesis of `law_of_logic_forces_jcost` is thus
  37replaced by a ledger-side statement: the cost composes through a ledger-posting
  38combiner.  The residual that remains is the bare *composability* of the cost
  39(`CostComposesThrough F P` for some `P`), isolated cleanly here; the "combiner
  40is RCL" half is now a theorem of the ledger, not a hypothesis.
  41
  42`Cost.Jcost` itself composes through `rclCombiner`
  43(`jcost_composesThrough_rclCombiner`), so the construction is non-vacuous: `J`
  44is a genuine fixed point of the entire ledger-composition setup.
  45
  46Status: 0 sorry, 0 new axiom.  Uses the proved `AczelSmoothnessPackage`
  47instance (`Cost/AczelProof.lean`), so the conclusion is unconditional.
  48-/
  49
  50namespace IndisputableMonolith
  51namespace Foundation
  52namespace LedgerCompositionToJCost
  53
  54open Cost.FunctionalEquation
  55open DAlembert.FactorizationForcing
  56open LedgerToFactorization
  57
  58/-! ## The composition law is "the cost composes through the RCL combiner" -/
  59
  60/-- **The composition law is the RCL combiner law on costs.**  `F` satisfies the
  61recognition composition law iff its symmetric two-point combination
  62`F (x·y) + F (x/y)` equals `rclCombiner (F x) (F y)`.  This is a pure
  63rearrangement: `rclCombiner u v = 2uv + 2u + 2v` is the composition-law RHS with
  64`u = F x`, `v = F y`. -/
  65theorem satisfiesCompositionLaw_iff_rclCombiner (F : ℝ → ℝ) :
  66    SatisfiesCompositionLaw F ↔
  67      ∀ x y : ℝ, 0 < x → 0 < y →
  68        F (x * y) + F (x / y) = rclCombiner (F x) (F y) := by
  69  unfold SatisfiesCompositionLaw rclCombiner
  70  constructor
  71  · intro h x y hx hy; rw [h x y hx hy]
  72  · intro h x y hx hy; rw [h x y hx hy]
  73
  74/-- **The cost composes through a combiner `P`** if its symmetric two-point
  75combination is `P` evaluated at the costs.  This is the factorization /
  76composability input: `F (x·y) + F (x/y)` is governed by a binary law of the two
  77single-point costs. -/
  78def CostComposesThrough (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ) : Prop :=
  79  ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)
  80
  81/-- If the cost composes through the RCL combiner, it satisfies the composition
  82law. -/
  83theorem satisfiesCompositionLaw_of_composesThrough_rcl (F : ℝ → ℝ)
  84    (h : CostComposesThrough F rclCombiner) :
  85    SatisfiesCompositionLaw F :=
  86  (satisfiesCompositionLaw_iff_rclCombiner F).mpr h
  87
  88/-- **Ledger posting + directional regularity force the cost's composition
  89law.**  If `F` composes through a combiner `P`, and `P` is a primitive
  90ledger-posting combiner with per-slice directional regularity, then `P` is
  91forced to be `rclCombiner` (Phase 3), so `F` satisfies the recognition
  92composition law. -/
  93theorem satisfiesCompositionLaw_of_ledgerComposes (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
  94    (hP : PrimitiveLedgerPostingSemantics P)
  95    (hdir : ∀ u, Monotone (fun v => P u v) ∨ Antitone (fun v => P u v))
  96    (hCompose : CostComposesThrough F P) :
  97    SatisfiesCompositionLaw F := by
  98  have hPrcl : ∀ u v, P u v = rclCombiner u v :=
  99    primitiveLedgerPosting_directional_forces_rcl P hP hdir
 100  apply satisfiesCompositionLaw_of_composesThrough_rcl
 101  intro x y hx hy
 102  rw [hCompose x y hx hy, hPrcl]
 103
 104/-! ## Phase 3 endpoint: ledger composition forces `J` -/
 105
 106/-- **Ledger composition forces `J`.**  If the recognition cost `F` is
 107reciprocal, normalized, calibrated, and continuous on the positive ray, and it
 108composes through a combiner `P` that satisfies primitive ledger posting with
 109per-slice directional regularity, then `F = J` on positives.
 110
 111This is the genuine discharge of the Phase 3 "Apply `law_of_logic_forces_jcost`"
 112item: the previously-assumed `SatisfiesCompositionLaw F` hypothesis is replaced
 113by the ledger-side pair (cost composes through `P`) ∧ (`P` is a ledger-posting
 114combiner), and the "combiner = RCL" half is a theorem, not an assumption. -/
 115theorem ledgerComposition_forces_jcost
 116    (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
 117    (hRecip : IsReciprocalCost F)
 118    (hNorm : IsNormalized F)
 119    (hCalib : IsCalibrated F)
 120    (hCont : ContinuousOn F (Set.Ioi 0))
 121    (hP : PrimitiveLedgerPostingSemantics P)
 122    (hdir : ∀ u, Monotone (fun v => P u v) ∨ Antitone (fun v => P u v))
 123    (hCompose : CostComposesThrough F P) :
 124    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
 125  have hComp : SatisfiesCompositionLaw F :=
 126    satisfiesCompositionLaw_of_ledgerComposes F P hP hdir hCompose
 127  exact law_of_logic_forces_jcost F hRecip hNorm hComp hCalib hCont
 128
 129/-! ## Non-vacuity: `J` composes through the RCL combiner -/
 130
 131/-- **`J` composes through the RCL combiner.**  The recognition cost
 132`J(x) = ½(x + x⁻¹) − 1` satisfies `J (x·y) + J (x/y) = rclCombiner (J x) (J y)`
 133for positive `x, y`.  This shows the ledger-composition setup is non-vacuous:
 134`J` is a fixed point of the composition law it forces. -/
 135theorem jcost_composesThrough_rclCombiner :
 136    CostComposesThrough Cost.Jcost rclCombiner := by
 137  intro x y hx hy
 138  have hx0 : x ≠ 0 := ne_of_gt hx
 139  have hy0 : y ≠ 0 := ne_of_gt hy
 140  unfold Cost.Jcost rclCombiner
 141  field_simp
 142  ring
 143
 144/-- Consequently `J` itself satisfies the recognition composition law. -/
 145theorem jcost_satisfiesCompositionLaw : SatisfiesCompositionLaw Cost.Jcost :=
 146  satisfiesCompositionLaw_of_composesThrough_rcl Cost.Jcost
 147    jcost_composesThrough_rclCombiner
 148
 149/-! ## Certificate -/
 150
 151/-- The Phase 3 ledger-composition closure certificate: every field is a proved
 152theorem of this module.  It records that the composition-law hypothesis of
 153`law_of_logic_forces_jcost` is reducible to a ledger-posting combiner plus bare
 154composability, that this forces `J`, and that `J` is a consistent fixed point. -/
 155structure LedgerCompositionCertificate : Prop where
 156  /-- The composition law is exactly "the cost composes through the RCL
 157  combiner". -/
 158  composition_law_is_rcl :
 159    ∀ F : ℝ → ℝ, SatisfiesCompositionLaw F ↔
 160      ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = rclCombiner (F x) (F y)
 161  /-- A cost composing through a ledger-posting + directional combiner satisfies
 162  the composition law. -/
 163  ledger_composes_forces_composition_law :
 164    ∀ (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ),
 165      PrimitiveLedgerPostingSemantics P →
 166      (∀ u, Monotone (fun v => P u v) ∨ Antitone (fun v => P u v)) →
 167      CostComposesThrough F P →
 168      SatisfiesCompositionLaw F
 169  /-- Ledger composition (plus reciprocal/normalized/calibrated/continuous)
 170  forces `F = J`. -/
 171  ledger_composition_forces_jcost :
 172    ∀ (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ),
 173      IsReciprocalCost F → IsNormalized F → IsCalibrated F →
 174      ContinuousOn F (Set.Ioi 0) →
 175      PrimitiveLedgerPostingSemantics P →
 176      (∀ u, Monotone (fun v => P u v) ∨ Antitone (fun v => P u v)) →
 177      CostComposesThrough F P →
 178      ∀ x : ℝ, 0 < x → F x = Cost.Jcost x
 179  /-- `J` composes through the RCL combiner (non-vacuity). -/
 180  jcost_composes : CostComposesThrough Cost.Jcost rclCombiner
 181
 182/-- The ledger-composition certificate holds. -/
 183theorem ledgerCompositionCertificate : LedgerCompositionCertificate where
 184  composition_law_is_rcl := satisfiesCompositionLaw_iff_rclCombiner
 185  ledger_composes_forces_composition_law :=
 186    satisfiesCompositionLaw_of_ledgerComposes
 187  ledger_composition_forces_jcost := ledgerComposition_forces_jcost
 188  jcost_composes := jcost_composesThrough_rclCombiner
 189
 190end LedgerCompositionToJCost
 191end Foundation
 192end IndisputableMonolith
 193