IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCalibrationIndependence

   1/-
   2  PrimitiveRecognitionCalculus/PRCCalibrationIndependence.lean
   3
   4  Item 2, the negative direction, proved (not just asserted in prose).
   5
   6  `PRCCalibrationTarget.lean` established the POSITIVE structure of the residual
   7  calibration freedom: the δ-forced cost form is a faithful one-parameter family,
   8  its only invariant is the log-curvature `c²` at the unit, and "curvature = 1"
   9  picks out `J`. From that it CLAIMED, in prose, that the unit `c` is a gauge --
  10  "not a δ-forced constant" -- because curvature is a continuum-side
  11  second-derivative datum the discrete carrier does not supply.
  12
  13  That claim was never a theorem. This module proves it, as the exact analogue of
  14  `PRCCompletenessIndependence.completeness_not_forced_by_genuine_cost_laws`:
  15
  16  The multiplicative gauge family
  17
  18      costLambda c x = ½(x^c + x^{−c}) − 1      (real exponent, x > 0)
  19
  20  satisfies, for EVERY positive `c`, the genuine recognition cost laws recorded in
  21  `Cost.CostRequirements` (reciprocal symmetry `F x = F x⁻¹` and the unit law
  22  `F 1 = 0`), and each member is moreover continuous on `(0,∞)`. The family is
  23  faithful (`costLambda_inj`): distinct positive `c` give genuinely distinct cost
  24  functions. The `c = 1` member is exactly `Cost.Jcost`.
  25
  26  Consequence (`calibration_unit_not_forced_by_cost_laws`): two distinct functions
  27  (`costLambda 1 = J` and `costLambda 2`) both satisfy `Cost.CostRequirements`, so
  28  those laws do NOT entail `c = 1`. The unit of scale is logically independent of
  29  the cost laws; it is fixed only by the extra calibration hypothesis (leading
  30  log-curvature normalized to 1) carried by the upstream uniqueness theorem
  31  `Cost.FunctionalEquation.law_of_logic_forces_jcost`. Drop that one hypothesis and
  32  the whole family is admissible. So "δ forces the cost FORM" does not upgrade to
  33  "δ forces J": the unit is the one irreducible gauge choice.
  34
  35  This is the credibility-gating form. A skeptic cannot say the independence rests
  36  on a weak premise: every member is a bona fide recognition cost (symmetric, unit
  37  law, continuous), differing only in the unforced unit.
  38
  39  No project-local axioms. No sorry.
  40-/
  41
  42import Mathlib
  43import IndisputableMonolith.Cost
  44import IndisputableMonolith.Cost.FunctionalEquation
  45import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCalibrationTarget
  46
  47namespace IndisputableMonolith
  48namespace Foundation
  49namespace PrimitiveRecognitionCalculus
  50namespace Calibration
  51
  52/-- The δ-forced cost gauge family in multiplicative coordinates:
  53`costLambda c x = ½(x^c + x^{−c}) − 1`, with the real exponent taken via
  54`Real.rpow`. The `c = 1` member is `J`. -/
  55noncomputable def costLambda (c x : ℝ) : ℝ := (x ^ c + x ^ (-c)) / 2 - 1
  56
  57/-- On the positive reals the multiplicative form coincides with the additive
  58(log-coordinate) form `cosh(c·log x) − 1` used in `PRCCalibrationTarget`. -/
  59theorem costLambda_eq_cosh (c : ℝ) {x : ℝ} (hx : 0 < x) :
  60    costLambda c x = Real.cosh (c * Real.log x) - 1 := by
  61  have h1 : x ^ c = Real.exp (c * Real.log x) := by
  62    rw [Real.rpow_def_of_pos hx c, mul_comm]
  63  have h2 : x ^ (-c) = Real.exp (-(c * Real.log x)) := by
  64    rw [Real.rpow_def_of_pos hx (-c)]
  65    congr 1
  66    ring
  67  unfold costLambda
  68  rw [h1, h2, Real.cosh_eq]
  69
  70/-- The unit law `F(1) = 0` holds for every member. -/
  71theorem costLambda_unit0 (c : ℝ) : costLambda c 1 = 0 := by
  72  rw [costLambda_eq_cosh c one_pos, Real.log_one, mul_zero, Real.cosh_zero]
  73  norm_num
  74
  75/-- Reciprocal symmetry `F x = F x⁻¹` holds for every member on the positives. -/
  76theorem costLambda_symm (c : ℝ) {x : ℝ} (hx : 0 < x) :
  77    costLambda c x = costLambda c x⁻¹ := by
  78  have hxinv : 0 < x⁻¹ := inv_pos.mpr hx
  79  rw [costLambda_eq_cosh c hx, costLambda_eq_cosh c hxinv, Real.log_inv, mul_neg,
  80    Real.cosh_neg]
  81
  82/-- **Every gauge member is a bona fide recognition cost.** For every positive
  83`c`, `costLambda c` satisfies `Cost.CostRequirements` (the same structure
  84`PRCCompletenessIndependence.jcost_isCostRequirements` verifies for `J`). -/
  85theorem costLambda_isCostRequirements (c : ℝ) :
  86    Cost.CostRequirements (fun x => costLambda c x) where
  87  symmetric := fun {_} hx => costLambda_symm c hx
  88  unit0 := costLambda_unit0 c
  89
  90/-- Each member is continuous on `(0,∞)`, so continuity (a hypothesis of the
  91upstream uniqueness theorem) does not discriminate within the family either. -/
  92theorem costLambda_continuousOn (c : ℝ) :
  93    ContinuousOn (fun x => costLambda c x) (Set.Ioi 0) := by
  94  have hlog : ContinuousOn Real.log (Set.Ioi 0) :=
  95    Real.continuousOn_log.mono (fun x hx => ne_of_gt hx)
  96  have hmul : ContinuousOn (fun x => c * Real.log x) (Set.Ioi 0) :=
  97    continuousOn_const.mul hlog
  98  have hcosh : ContinuousOn (fun x => Real.cosh (c * Real.log x) - 1) (Set.Ioi 0) := by
  99    apply ContinuousOn.sub _ continuousOn_const
 100    exact Real.continuous_cosh.comp_continuousOn hmul
 101  exact hcosh.congr (fun x hx => costLambda_eq_cosh c hx)
 102
 103/-- The `c = 1` member is exactly `Cost.Jcost` on the positives. -/
 104theorem costLambda_one_eq_Jcost {x : ℝ} (hx : 0 < x) :
 105    costLambda 1 x = Cost.Jcost x := by
 106  rw [costLambda_eq_cosh 1 hx, one_mul]
 107  show Real.cosh (Real.log x) - 1 = (x + x⁻¹) / 2 - 1
 108  exact costLambda_one_eq_J x hx
 109
 110/-- **The family is faithful.** Distinct positive curvature parameters give
 111genuinely distinct cost functions. Proved by transporting the equality along
 112`x = exp t` to the log-coordinate family and invoking `clog_inj`. -/
 113theorem costLambda_inj {c d : ℝ} (hc : 0 < c) (hd : 0 < d)
 114    (h : (fun x => costLambda c x) = (fun x => costLambda d x)) : c = d := by
 115  apply clog_inj hc hd
 116  funext t
 117  have hexp : (0 : ℝ) < Real.exp t := Real.exp_pos t
 118  have hval := congrFun h (Real.exp t)
 119  simp only at hval
 120  rw [costLambda_eq_cosh c hexp, costLambda_eq_cosh d hexp, Real.log_exp] at hval
 121  exact hval
 122
 123/-- **Item 2, the negative direction.** The recognition cost laws
 124(`Cost.CostRequirements`) do not force the unit of scale.
 125
 126The conjunction records: every member of the gauge family is a bona fide cost
 127(symmetric + unit law); the family is faithful (so the residual freedom is exactly
 128one real); the `c = 1` member is `J`; and there exist two genuinely distinct
 129members (`costLambda 1 = J` and `costLambda 2`) both satisfying the cost laws.
 130The last clause is the independence: the laws are satisfied by more than one
 131function, hence cannot single out `J`. The unit is fixed only by the extra
 132calibration hypothesis of the upstream uniqueness theorem, and is therefore the
 133one irreducible gauge choice. -/
 134theorem calibration_unit_not_forced_by_cost_laws :
 135    (∀ c : ℝ, Cost.CostRequirements (fun x => costLambda c x))
 136      ∧ (∀ c d : ℝ, 0 < c → 0 < d →
 137          (fun x => costLambda c x) = (fun x => costLambda d x) → c = d)
 138      ∧ (∀ x : ℝ, 0 < x → costLambda 1 x = Cost.Jcost x)
 139      ∧ (∃ c d : ℝ, 0 < c ∧ 0 < d ∧ c ≠ d
 140            ∧ Cost.CostRequirements (fun x => costLambda c x)
 141            ∧ Cost.CostRequirements (fun x => costLambda d x)
 142            ∧ (fun x => costLambda c x) ≠ (fun x => costLambda d x)) := by
 143  refine ⟨fun c => costLambda_isCostRequirements c,
 144          fun c d hc hd h => costLambda_inj hc hd h,
 145          fun x hx => costLambda_one_eq_Jcost hx,
 146          ⟨1, 2, one_pos, two_pos, by norm_num,
 147           costLambda_isCostRequirements 1, costLambda_isCostRequirements 2, ?_⟩⟩
 148  intro h
 149  have h12 : (1 : ℝ) = 2 := costLambda_inj one_pos two_pos h
 150  norm_num at h12
 151
 152/-! ## Independence against the FULL law set (RCL included)
 153
 154The result above used only `Cost.CostRequirements = {symmetry, unit law}`. A skeptic
 155could object that those are weak, and that adding the reciprocal cost law (RCL, the
 156d'Alembert composition identity that actually drives the upstream classification) pins
 157the unit after all. It does not. The section below proves the gauge family satisfies
 158the EXACT non-calibration hypothesis set of
 159`Cost.FunctionalEquation.law_of_logic_forces_jcost`
 160(`IsReciprocalCost`, `IsNormalized`, `SatisfiesCompositionLaw`, `ContinuousOn (Ioi 0)`)
 161for every positive `c`, and that the remaining hypothesis `IsCalibrated` holds iff
 162`c = 1`. So calibration is the single hypothesis that pins `J`; everything else is
 163satisfied by the whole family. -/
 164
 165/-- In log coordinates the gauge member reads off as `G(costLambda c) t = cosh(c·t) − 1`,
 166matching the `cosh(c·)` family that drives the upstream functional-equation classification. -/
 167theorem G_costLambda (c t : ℝ) :
 168    Cost.FunctionalEquation.G (fun x => costLambda c x) t = Real.cosh (c * t) - 1 := by
 169  show costLambda c (Real.exp t) = Real.cosh (c * t) - 1
 170  rw [costLambda_eq_cosh c (Real.exp_pos t), Real.log_exp]
 171
 172/-- **Every gauge member satisfies the RCL** (the cosh-add / d'Alembert identity). Both
 173sides reduce to `2·cosh(ct)cosh(cu) − 2` via `cosh_add`/`cosh_sub`. -/
 174theorem costLambda_coshAddIdentity (c : ℝ) :
 175    Cost.FunctionalEquation.CoshAddIdentity (fun x => costLambda c x) := by
 176  intro t u
 177  simp only [G_costLambda]
 178  have e1 : c * (t + u) = c * t + c * u := by ring
 179  have e2 : c * (t - u) = c * t - c * u := by ring
 180  rw [e1, e2, Real.cosh_add, Real.cosh_sub]
 181  ring
 182
 183theorem costLambda_isReciprocalCost (c : ℝ) :
 184    Cost.FunctionalEquation.IsReciprocalCost (fun x => costLambda c x) :=
 185  fun _ hx => costLambda_symm c hx
 186
 187theorem costLambda_isNormalized (c : ℝ) :
 188    Cost.FunctionalEquation.IsNormalized (fun x => costLambda c x) :=
 189  costLambda_unit0 c
 190
 191theorem costLambda_satisfiesCompositionLaw (c : ℝ) :
 192    Cost.FunctionalEquation.SatisfiesCompositionLaw (fun x => costLambda c x) :=
 193  (Cost.FunctionalEquation.composition_law_equiv_coshAdd _).mpr (costLambda_coshAddIdentity c)
 194
 195/-- The remaining hypothesis, calibration (`G''(0) = 1`), holds iff `c = 1`, because
 196`G(costLambda c)'' (0) = c²`. -/
 197theorem costLambda_isCalibrated_iff {c : ℝ} (hc : 0 < c) :
 198    Cost.FunctionalEquation.IsCalibrated (fun x => costLambda c x) ↔ c = 1 := by
 199  have hG : Cost.FunctionalEquation.G (fun x => costLambda c x)
 200      = fun t => Real.cosh (c * t) - 1 := by
 201    funext t; exact G_costLambda c t
 202  unfold Cost.FunctionalEquation.IsCalibrated
 203  rw [hG]
 204  exact curvature_one_iff_J hc
 205
 206/-- **Item 2, airtight: calibration is the ONLY hypothesis of the uniqueness theorem
 207that pins `J`.** Every gauge member satisfies the full non-calibration hypothesis set of
 208`law_of_logic_forces_jcost` (reciprocity, normalization, the RCL composition law, and
 209continuity on the positives); calibration holds iff `c = 1`; and the family contains
 210genuinely distinct members. Hence the four non-calibration hypotheses are satisfied by
 211more than one function and cannot determine `J`: the unit of scale is logically
 212independent of the entire law set except for the calibration choice. -/
 213theorem calibration_is_the_only_hypothesis_pinning_J :
 214    (∀ c : ℝ,
 215        Cost.FunctionalEquation.IsReciprocalCost (fun x => costLambda c x)
 216          ∧ Cost.FunctionalEquation.IsNormalized (fun x => costLambda c x)
 217          ∧ Cost.FunctionalEquation.SatisfiesCompositionLaw (fun x => costLambda c x)
 218          ∧ ContinuousOn (fun x => costLambda c x) (Set.Ioi 0))
 219      ∧ (∀ c : ℝ, 0 < c →
 220          (Cost.FunctionalEquation.IsCalibrated (fun x => costLambda c x) ↔ c = 1))
 221      ∧ (∃ c d : ℝ, 0 < c ∧ 0 < d ∧ c ≠ d
 222            ∧ (fun x => costLambda c x) ≠ (fun x => costLambda d x)) := by
 223  refine ⟨fun c => ⟨costLambda_isReciprocalCost c, costLambda_isNormalized c,
 224            costLambda_satisfiesCompositionLaw c, costLambda_continuousOn c⟩,
 225          fun c hc => costLambda_isCalibrated_iff hc, ?_⟩
 226  refine ⟨1, 2, one_pos, two_pos, by norm_num, ?_⟩
 227  intro h
 228  have h12 : (1 : ℝ) = 2 := costLambda_inj one_pos two_pos h
 229  norm_num at h12
 230
 231end Calibration
 232end PrimitiveRecognitionCalculus
 233end Foundation
 234end IndisputableMonolith
 235