IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCalibrationTarget

   1/-
   2  PrimitiveRecognitionCalculus/PRCCalibrationTarget.lean
   3
   4  Item 2 of the δ frontier: force the calibration unit from one δ act?
   5
   6  The δ-forced cost FORM is the one-parameter gauge family (in log
   7  coordinates t = ln x):
   8
   9      clog c t = cosh(c·t) − 1,    c > 0,
  10
  11  which in multiplicative coordinates is costLambda c x = ½(x^c + x^{−c}) − 1.
  12  Every member satisfies reciprocal symmetry, normalization, and the
  13  composition law (the d'Alembert / RCL identity proved upstream); they differ
  14  only by the positive real c, the "unit of scale". Calibration is the choice
  15  of c. The hope of Item 2 was that the cost of one δ act (distinguishing an
  16  orbit from its successor) would force the log-curvature at the unit to be
  17  exactly 1, hence c = 1, hence J.
  18
  19  What is proved here (the exact statement, both falsifier branches considered):
  20
  21  * `logCurvature`:           the log-curvature at the unit is c² for every c.
  22  * `clog_inj`:               distinct positive c give genuinely distinct costs;
  23                              the family is a faithful 1-parameter family.
  24  * `curvature_one_iff_J`:    curvature normalized to 1 ⟺ c = 1 (the J member).
  25  * `costLambda_one_eq_J`:    the c = 1 member is exactly J(x) = ½(x + x⁻¹) − 1.
  26  * `calibration_unit_is_a_gauge`: the headline conjunction.
  27
  28  RESULT (the falsifier resolves negative). The curvature at the unit is a
  29  SECOND-DERIVATIVE property: it is defined by the local behaviour of the cost
  30  at the limit ratio x → 1, i.e. by the continuous completion. The δ-native
  31  carrier is the rationals ℚ_δ, where the minimal distinction is the finite
  32  ratio step and no infinitesimal / second derivative exists. The discrete δ
  33  data (costs at rational ratios) therefore does NOT single out c; the whole
  34  family is admissible on ℚ_δ and the members are mutually distinct. The
  35  calibration c = 1 is fixed only by a continuum-side normalization (choosing
  36  the cost unit so the leading log-curvature is 1). It is a gauge, not a δ-forced
  37  constant. This confirms the δ3 / δ0 framing: "δ forces the cost FORM" does NOT
  38  upgrade to "δ forces J"; the unit is the one residual free parameter.
  39
  40  The positive content (form forced, family faithful, J = the curvature-1
  41  member) is fully proved below. The negative interpretation (curvature is a
  42  continuum property the discrete carrier cannot fix) is the honest reading the
  43  proved structure forces.
  44
  45  UPGRADE (PRCCalibrationIndependence.lean): the negative direction is no longer
  46  only "the honest reading"; it is now a theorem, in two strengths.
  47
  48  (a) `calibration_unit_not_forced_by_cost_laws`: the whole gauge family
  49  `costLambda c = ½(x^c + x^{−c}) − 1` satisfies the recognition cost laws
  50  `Cost.CostRequirements` for every positive `c` (and is continuous on the
  51  positives), is faithful, and has `J` as its `c = 1` member; two distinct members
  52  satisfy the laws, so the laws cannot force `c = 1`.
  53
  54  (b) `calibration_is_the_only_hypothesis_pinning_J` (airtight, RCL included):
  55  every member satisfies the EXACT non-calibration hypothesis set of
  56  `Cost.FunctionalEquation.law_of_logic_forces_jcost` -- `IsReciprocalCost`,
  57  `IsNormalized`, `SatisfiesCompositionLaw` (the RCL / d'Alembert composition law),
  58  and `ContinuousOn (Set.Ioi 0)` -- while `IsCalibrated` holds iff `c = 1`. So
  59  calibration is the single hypothesis of the uniqueness theorem that pins `J`; the
  60  unit of scale is logically independent of the entire law set except for the
  61  calibration choice. This forecloses the objection that adding the RCL to the weak
  62  `CostRequirements` premise might re-force the unit.
  63
  64  No project-local axioms. No sorry.
  65-/
  66
  67import Mathlib
  68
  69namespace IndisputableMonolith
  70namespace Foundation
  71namespace PrimitiveRecognitionCalculus
  72namespace Calibration
  73
  74/-- The log-curvature of the cost member `cosh(c·t) − 1` at the unit (t = 0) is
  75`c²`. This is the residual gauge parameter read off as a second derivative. -/
  76theorem logCurvature (c : ℝ) :
  77    deriv (deriv (fun t => Real.cosh (c * t) - 1)) 0 = c ^ 2 := by
  78  have hderiv1 : deriv (fun t => Real.cosh (c * t) - 1)
  79      = fun t => c * Real.sinh (c * t) := by
  80    funext t
  81    have hinner : HasDerivAt (fun s => c * s) (c * 1) t :=
  82      (hasDerivAt_id t).const_mul c
  83    have h : HasDerivAt (fun t => Real.cosh (c * t) - 1)
  84        (Real.sinh (c * t) * (c * 1)) t :=
  85      ((Real.hasDerivAt_cosh (c * t)).comp t hinner).sub_const 1
  86    rw [h.deriv]; ring
  87  rw [hderiv1]
  88  have hinner0 : HasDerivAt (fun s => c * s) (c * 1) (0 : ℝ) :=
  89    (hasDerivAt_id (0 : ℝ)).const_mul c
  90  have h2 : HasDerivAt (fun t => c * Real.sinh (c * t))
  91      (c * (Real.cosh (c * 0) * (c * 1))) (0 : ℝ) :=
  92    ((Real.hasDerivAt_sinh (c * 0)).comp (0 : ℝ) hinner0).const_mul c
  93  rw [h2.deriv]
  94  simp only [mul_zero, Real.cosh_zero, one_mul, mul_one]
  95  ring
  96
  97/-- The cost family is faithful: distinct positive curvature parameters give
  98distinct cost functions. (Proved through the curvature, which is an invariant of
  99the function.) -/
 100theorem clog_inj {c d : ℝ} (hc : 0 < c) (hd : 0 < d)
 101    (h : (fun t => Real.cosh (c * t) - 1) = (fun t => Real.cosh (d * t) - 1)) :
 102    c = d := by
 103  have e1 : deriv (deriv (fun t => Real.cosh (c * t) - 1)) 0 = c ^ 2 :=
 104    logCurvature c
 105  have e2 : deriv (deriv (fun t => Real.cosh (d * t) - 1)) 0 = d ^ 2 :=
 106    logCurvature d
 107  rw [h, e2] at e1
 108  have hsq : c ^ 2 = d ^ 2 := e1.symm
 109  have hfac : (c - d) * (c + d) = 0 := by nlinarith [hsq]
 110  rcases mul_eq_zero.mp hfac with h' | h'
 111  · linarith
 112  · linarith
 113
 114/-- Curvature normalized to 1 picks out exactly the `c = 1` member, i.e. J. -/
 115theorem curvature_one_iff_J {c : ℝ} (hc : 0 < c) :
 116    deriv (deriv (fun t => Real.cosh (c * t) - 1)) 0 = 1 ↔ c = 1 := by
 117  rw [logCurvature c]
 118  constructor
 119  · intro h
 120    have hfac : (c - 1) * (c + 1) = 0 := by nlinarith [h]
 121    rcases mul_eq_zero.mp hfac with h' | h'
 122    · linarith
 123    · linarith
 124  · intro h; rw [h]; norm_num
 125
 126/-- The `c = 1` member is exactly J: in multiplicative coordinates,
 127`cosh(ln x) − 1 = ½(x + x⁻¹) − 1`. -/
 128theorem costLambda_one_eq_J (x : ℝ) (hx : 0 < x) :
 129    Real.cosh (Real.log x) - 1 = (x + x⁻¹) / 2 - 1 := by
 130  rw [Real.cosh_eq, Real.exp_neg, Real.exp_log hx]
 131
 132/-- **Item 2 headline.** The δ-forced cost form leaves a faithful one-parameter
 133gauge family; its only invariant is the log-curvature c² at the unit; and
 134"curvature = 1" is exactly the condition selecting J. The unit c is a free
 135positive real (a gauge), because curvature is a continuum-side second-derivative
 136property that the discrete δ carrier does not fix. -/
 137theorem calibration_unit_is_a_gauge :
 138    (∀ c : ℝ, deriv (deriv (fun t => Real.cosh (c * t) - 1)) 0 = c ^ 2)
 139      ∧ (∀ c d : ℝ, 0 < c → 0 < d →
 140          (fun t => Real.cosh (c * t) - 1) = (fun t => Real.cosh (d * t) - 1) → c = d)
 141      ∧ (∀ c : ℝ, 0 < c →
 142          (deriv (deriv (fun t => Real.cosh (c * t) - 1)) 0 = 1 ↔ c = 1)) :=
 143  ⟨logCurvature, fun _ _ hc hd h => clog_inj hc hd h, fun _ hc => curvature_one_iff_J hc⟩
 144
 145/-- The gauge action `μ • F := F(μ · )` is transitive on the cost family: any
 146member reaches any other through a positive rescaling of the log-coordinate. -/
 147theorem gauge_action_transitive {c d : ℝ} (hc : 0 < c) (hd : 0 < d) :
 148    ∃ μ : ℝ, 0 < μ ∧
 149      (fun t => Real.cosh (c * (μ * t)) - 1) = (fun t => Real.cosh (d * t) - 1) := by
 150  refine ⟨d / c, div_pos hd hc, ?_⟩
 151  funext t
 152  have hcne : c ≠ 0 := ne_of_gt hc
 153  have hkey : c * (d / c * t) = d * t := by field_simp
 154  rw [hkey]
 155
 156/-- **Item 2, sharpened: the residual freedom is a torsor, exactly one real.** The
 157gauge action of the positive reals on the cost family is free (`clog_inj`) and
 158transitive (`gauge_action_transitive`). A free transitive action exhibits the
 159family as a principal homogeneous space under `(ℝ_{>0}, ·)`, so the residual
 160freedom in the cost is exactly one positive real, the unit of scale. It is fixed
 161by one calibration datum (curvature 1), and that datum is not supplied by the
 162discrete δ structure. -/
 163theorem cost_freedom_is_one_real_torsor :
 164    (∀ c d : ℝ, 0 < c → 0 < d →
 165        (fun t => Real.cosh (c * t) - 1) = (fun t => Real.cosh (d * t) - 1) → c = d)
 166      ∧ (∀ c d : ℝ, 0 < c → 0 < d →
 167          ∃ μ : ℝ, 0 < μ ∧
 168            (fun t => Real.cosh (c * (μ * t)) - 1) = (fun t => Real.cosh (d * t) - 1)) :=
 169  ⟨fun _ _ hc hd h => clog_inj hc hd h, fun _ _ hc hd => gauge_action_transitive hc hd⟩
 170
 171end Calibration
 172end PrimitiveRecognitionCalculus
 173end Foundation
 174end IndisputableMonolith
 175