IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaRealCalibration

   1/-
   2  PrimitiveRecognitionCalculus/DeltaRealCalibration.lean
   3
   4  Phase 4 of the Delta-Native Analysis frontier: calibration from one act.
   5
   6  The δ-forced cost form is the faithful one-parameter gauge family (log
   7  coordinates) `cosh(c·t) − 1`, `c > 0`. The calibration question is whether δ
   8  forces `c = 1` (the canonical J), i.e. whether the unit of scale is derived
   9  rather than chosen.
  10
  11  The earlier modules resolved this NEGATIVELY at the discrete carrier:
  12  `PRCCalibrationTarget` and `PRCCalibrationIndependence` prove the family is a
  13  faithful torsor under positive rescaling, that the only invariant is the
  14  log-curvature `c²` at the unit, and that the discrete carrier ℚδ cannot fix it
  15  because curvature is a second-derivative (continuum) property.
  16
  17  This module records the honest reading the `ℝδ` interface forces. The one-act
  18  log-curvature is exactly a continuum-interface datum: it is read at the limit
  19  ratio `x → 1`, which lives in the protocol layer of `DeltaReal`, not in the
  20  discrete rational carrier. So:
  21
  22  * `unit_forced_by_one_act` : at the continuum interface, the single normalization
  23    "one-act curvature = 1" forces `c = 1`;
  24  * `discrete_does_not_force_unit` : the family is faithful and transitively
  25    rescaled, a one-real torsor, so without that one datum the unit is free;
  26  * `calibration_is_one_continuum_act` : the headline. `λ = 1` is forced by exactly
  27    one continuum-interface recognition act (the one-act curvature normalization),
  28    and by nothing in the discrete δ data. The residual gauge is one real, removed
  29    by one datum.
  30
  31  Second-pass closure:
  32
  33  * `NormalizedOneActInterface` packages the minimum extra interface datum needed
  34    to close calibration.
  35  * `normalized_interface_forces_J` proves that any such interface selects the
  36    canonical member.
  37  * `calibration_datum_necessary_and_sufficient` proves the datum is not an
  38    arbitrary patch: for positive units, it is exactly equivalent to `c = 1`.
  39
  40  No disguise: this is a CONDITIONAL derivation. The condition (one-act curvature
  41  normalization) is a continuum-side recognition datum, named explicitly. It is not
  42  smuggled, and it is not claimed to be discrete-δ-forced.
  43
  44  No project-local axioms. No sorry.
  45-/
  46
  47import Mathlib
  48import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCalibrationTarget
  49
  50namespace IndisputableMonolith
  51namespace Foundation
  52namespace PrimitiveRecognitionCalculus
  53namespace DeltaRealCalibration
  54
  55/-- The one-act log-curvature of the cost member with unit `c`: the second
  56derivative at the limit ratio `t = 0`. This is a continuum-interface quantity (it
  57is a second derivative), living in the `ℝδ` protocol layer, not in the discrete
  58rational carrier. -/
  59noncomputable def oneActCurvature (c : ℝ) : ℝ :=
  60  deriv (deriv (fun t => Real.cosh (c * t) - 1)) 0
  61
  62/-- The one-act curvature is `c²`: the residual gauge parameter read as a
  63second derivative. -/
  64theorem oneActCurvature_eq (c : ℝ) : oneActCurvature c = c ^ 2 :=
  65  Calibration.logCurvature c
  66
  67/-- **One continuum datum fixes the unit.** At the continuum interface, the single
  68normalization "one-act curvature equals 1" forces `c = 1`, i.e. selects the
  69canonical J. -/
  70theorem unit_forced_by_one_act {c : ℝ} (hc : 0 < c) :
  71    oneActCurvature c = 1 ↔ c = 1 := by
  72  unfold oneActCurvature
  73  exact Calibration.curvature_one_iff_J hc
  74
  75/-- **The discrete carrier does not force the unit.** The cost family is faithful
  76(distinct units give distinct costs) and transitively rescaled, so the residual
  77freedom is a one-real torsor. Without the one-act normalization datum the unit is
  78genuinely free. -/
  79theorem discrete_does_not_force_unit :
  80    (∀ c d : ℝ, 0 < c → 0 < d →
  81        (fun t => Real.cosh (c * t) - 1) = (fun t => Real.cosh (d * t) - 1) → c = d)
  82      ∧ (∀ c d : ℝ, 0 < c → 0 < d →
  83          ∃ μ : ℝ, 0 < μ ∧
  84            (fun t => Real.cosh (c * (μ * t)) - 1) = (fun t => Real.cosh (d * t) - 1)) :=
  85  Calibration.cost_freedom_is_one_real_torsor
  86
  87/-- **Phase 4 headline: calibration from one continuum act.** The unit `c` is a
  88faithful one-real torsor on the discrete carrier (no discrete δ datum fixes it),
  89while a single continuum-interface datum, the one-act curvature normalization,
  90forces `c = 1`. So `λ = 1` is derived from exactly one recognition act at the
  91`ℝδ` interface, with the residual gauge being one real removed by one datum.
  92This is the honest conditional: the calibration is not discrete-δ-forced, and the
  93one continuum datum is named rather than hidden. -/
  94theorem calibration_is_one_continuum_act :
  95    (∀ c : ℝ, oneActCurvature c = c ^ 2)
  96      ∧ (∀ c : ℝ, 0 < c → (oneActCurvature c = 1 ↔ c = 1))
  97      ∧ (∀ c d : ℝ, 0 < c → 0 < d →
  98          (fun t => Real.cosh (c * t) - 1) = (fun t => Real.cosh (d * t) - 1) → c = d) :=
  99  ⟨oneActCurvature_eq, fun _ hc => unit_forced_by_one_act hc,
 100    fun _ _ hc hd h => (Calibration.clog_inj hc hd h)⟩
 101
 102/-! ## Second-pass closure: the minimal normalized interface -/
 103
 104/-- The minimum continuum-side interface datum needed to close calibration. It is
 105not a full continuum and not a field completion. It is only: a positive cost unit
 106and the assertion that the primitive one-act chart has unit log-curvature. -/
 107structure NormalizedOneActInterface where
 108  unit : ℝ
 109  positive : 0 < unit
 110  curvature_unit : oneActCurvature unit = 1
 111
 112/-- Any normalized one-act interface forces the canonical cost unit. -/
 113theorem normalized_interface_forces_J (I : NormalizedOneActInterface) :
 114    I.unit = 1 :=
 115  (unit_forced_by_one_act I.positive).mp I.curvature_unit
 116
 117/-- For positive units, the one-act curvature datum is necessary and sufficient
 118for selecting the canonical member. This is the exact closure of the calibration
 119gap: one datum, no more and no less. -/
 120theorem calibration_datum_necessary_and_sufficient {c : ℝ} (hc : 0 < c) :
 121    c = 1 ↔ oneActCurvature c = 1 := by
 122  exact (unit_forced_by_one_act hc).symm
 123
 124/-- Existence of a normalized interface: the canonical member itself carries one. -/
 125def canonicalInterface : NormalizedOneActInterface where
 126  unit := 1
 127  positive := by norm_num
 128  curvature_unit := by
 129    rw [oneActCurvature_eq]
 130    norm_num
 131
 132/-- **Calibration closure theorem.** The discrete laws leave a faithful one-real
 133torsor (`discrete_does_not_force_unit`), while the normalized one-act interface is
 134both sufficient and necessary for `c = 1`. Thus the cost-unit issue is fully
 135classified: it is not discrete-forced; it is closed exactly by the minimal
 136second-order recognition interface. -/
 137theorem calibration_gap_closed_by_normalized_interface :
 138    (∀ I : NormalizedOneActInterface, I.unit = 1)
 139      ∧ (∀ c : ℝ, 0 < c → (c = 1 ↔ oneActCurvature c = 1))
 140      ∧ (∃ I : NormalizedOneActInterface, I.unit = 1)
 141      ∧ (∀ c d : ℝ, 0 < c → 0 < d →
 142          (fun t => Real.cosh (c * t) - 1) = (fun t => Real.cosh (d * t) - 1) → c = d) :=
 143  ⟨normalized_interface_forces_J, fun _ hc => calibration_datum_necessary_and_sufficient hc,
 144    ⟨canonicalInterface, rfl⟩, fun _ _ hc hd h => Calibration.clog_inj hc hd h⟩
 145
 146end DeltaRealCalibration
 147end PrimitiveRecognitionCalculus
 148end Foundation
 149end IndisputableMonolith
 150