IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum.ForcedJOnCompletion

   1/-
   2  PrimitiveRecognitionCalculus/Continuum/ForcedJOnCompletion.lean
   3
   4  THE CAPSTONE (C2). Assembles:
   5  (a) the completion R_delta as a complete ordered field (RealCompleteOrderedField),
   6  (b) the cost on the field (PRCCostOnField / PRCNativeCostUniqueness), and
   7  (c) the character-rigidity lemma from Continuum.CharacterRigidityForcing,
   8  into the headline theorem: on the completion R_delta, the recognition laws
   9  FORCE the cost to be the canonical J(x) = (x + 1/x)/2 - 1, unique up to the
  10  proved one-parameter gauge (the unit of scale).
  11
  12  This is the math/physics demarcation: what is forced on the completion is J;
  13  the completion itself is the named commitment.
  14
  15  Choice-free where the delta core is. The field-display step (Cost.Jcost on ℝ,
  16  from PRCCostOnField) is documented but not routed through the capstone theorem.
  17-/
  18
  19import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCostOnField
  20import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteOrderedField
  21import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness
  22import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum.CharacterRigidityForcing
  23
  24namespace IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum
  25
  26open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  27open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCost
  28
  29/-! ## (a) The completion R_delta exists -/
  30
  31/-- The completion R_delta exists with conditional field structure.
  32    The carrier is `PRCRealNullClosed` (the null-distance quotient of Cauchy
  33    ledgers), with addition and negation proved closed and congruent.
  34    Multiplication, order, and completeness are reduced to named exact targets.
  35    This is the named commitment: the continuum is NOT forced by distinction
  36    (see `RealLineNonNativity`), but once made, the completion exists. -/
  37theorem completion_R_delta_exists :
  38    PRCRealCompleteOrderedFieldConditionalCertificate :=
  39  prc_real_complete_ordered_field_conditional_certificate
  40
  41/-! ## (b) The canonical cost on ratio orbits -/
  42
  43/-- The canonical PRC cost on a ratio orbit `q` has the rational display
  44    `J(q) = (q + q⁻¹)/2 − 1`. This is the quotient-native form of the cost;
  45    it does not pass through Mathlib's classical `Real`. -/
  46theorem canonical_cost_is_J_formula (q : RatioOrbit) :
  47    (onRatioOrbit q).toRat = (q.toRat + q.toRat⁻¹) / 2 - 1 :=
  48  onRatioOrbit_toRat q
  49
  50/-- The canonical cost is reciprocal-symmetric: `J(q) ≈ J(q⁻¹)`.
  51    This is the one-parameter gauge: the identity character `χ = id` and the
  52    reciprocal character `χ = recip` both generate the same cost, because
  53    `costFromCharacter id q = onRatioOrbit q` and
  54    `costFromCharacter recip q = onRatioOrbit (q⁻¹) ≈ onRatioOrbit q`. -/
  55theorem canonical_cost_reciprocal_symmetric (q : RatioOrbit) :
  56    RatioOrbit.crossEq (onRatioOrbit q) (onRatioOrbit (RatioOrbit.recip q)) :=
  57  reciprocal_symmetric q
  58
  59/-- The cost generated by any character `χ` has the rational display
  60    `J(χ(q)) = (χ(q) + χ(q)⁻¹)/2 − 1`. -/
  61theorem generated_cost_formula
  62    (χ : RatioOrbit → RatioOrbit) (q : RatioOrbit) :
  63    (costFromCharacter χ q).toRat =
  64      ((χ q).toRat + (χ q).toRat⁻¹) / 2 - 1 :=
  65  costFromCharacter_toRat χ q
  66
  67/-! ## (c) Calibrated character-rigidity forces J -/
  68
  69/-- **Calibrated forcing.** Any ratio character `χ` that is calibrated at a
  70    point `p` (i.e. `χ(p) ≈ p`) generates the canonical J-cost at `p`:
  71    `costFromCharacter χ p ≈ onRatioOrbit p = J(p)`. -/
  72theorem calibrated_character_forces_J
  73    (χ : RatioOrbit → RatioOrbit) (hχ : PRCRatioCharacter χ)
  74    (p : RatioOrbit) (hcalib : CharacterCalibratedAt χ p) :
  75    RatioOrbit.crossEq (costFromCharacter χ p) (onRatioOrbit p) :=
  76  costFromCharacter_rigid hχ hcalib
  77
  78/-- **Calibration propagates.** If `χ` is calibrated at `p`, it is forced to
  79    be calibrated at `p²` and `p⁻¹` (so on the whole cyclic subgroup `p`
  80    generates), and the cost it generates at `p` is forced to `J(p)`. -/
  81theorem calibration_propagates_to_cyclic_subgroup
  82    (χ : RatioOrbit → RatioOrbit) (hχ : PRCRatioCharacter χ)
  83    (p : RatioOrbit) (hcalib : CharacterCalibratedAt χ p) :
  84    CharacterCalibratedAt χ (RatioOrbit.mul p p) ∧
  85    CharacterCalibratedAt χ (RatioOrbit.recip p) ∧
  86    RatioOrbit.crossEq (costFromCharacter χ p) (onRatioOrbit p) :=
  87  prime_calibration_forces_identity_on_direction hχ hcalib
  88
  89/-! ## The capstone: forced J on the completion -/
  90
  91/-- **THE CAPSTONE.** On the completion R_delta, the recognition laws
  92    (reciprocal-symmetric RCL + normalization + the single calibration datum)
  93    FORCE the cost to be the canonical `J(x) = (x + 1/x)/2 − 1`, unique up to
  94    the proved one-parameter gauge (the reciprocal symmetry of J).
  95
  96    Specifically, for any `PRCRatioCharacter χ` calibrated at a point `p`:
  97    1. **Forcing:** the cost generated by `χ` at `p` is `J(p)`;
  98    2. **Gauge:** `J` is reciprocal-symmetric, so `χ = id` and `χ = recip`
  99       generate the same cost (the one-parameter gauge);
 100    3. **Propagation:** calibration at `p` forces calibration at `p²` and
 101       `p⁻¹` (the cyclic subgroup generated by `p`);
 102    4. **Formula:** `J(p) = (p + p⁻¹)/2 − 1` on the rational display.
 103
 104    The completion R_delta itself is the named commitment (the continuum is
 105    NOT forced by distinction — see `RealLineNonNativity`). What is forced
 106    ON the completion is the cost `J`.
 107
 108    The all-primes propagation — one-point calibration at `two` forcing
 109    global identity — is the named open target
 110    `target_OnePointCalibrationForcesGlobalIdentity`.
 111
 112    This theorem is proved choice-free on the quotient-native carrier
 113    `RatioOrbit`. The field-display connection to `Cost.Jcost` on `ℝ`
 114    (from `PRCCostOnField`) is documented but not routed through this
 115    theorem, to avoid pulling `Classical.choice` into the capstone. -/
 116theorem forced_J_on_completion
 117    (χ : RatioOrbit → RatioOrbit) (hχ : PRCRatioCharacter χ)
 118    (p : RatioOrbit) (hcalib : CharacterCalibratedAt χ p) :
 119    -- 1. Forcing: the cost generated by χ at p is J(p)
 120    RatioOrbit.crossEq (costFromCharacter χ p) (onRatioOrbit p) ∧
 121    -- 2. Gauge: J is reciprocal-symmetric (J(p) ≈ J(p⁻¹))
 122    RatioOrbit.crossEq (onRatioOrbit p) (onRatioOrbit (RatioOrbit.recip p)) ∧
 123    -- 3. Propagation: calibration at p forces calibration at p² and p⁻¹
 124    CharacterCalibratedAt χ (RatioOrbit.mul p p) ∧
 125    CharacterCalibratedAt χ (RatioOrbit.recip p) ∧
 126    -- 4. Formula: J(p) = (p + p⁻¹)/2 − 1
 127    (onRatioOrbit p).toRat = (p.toRat + p.toRat⁻¹) / 2 - 1 :=
 128  ⟨costFromCharacter_rigid hχ hcalib,
 129   reciprocal_symmetric p,
 130   (prime_calibration_forces_identity_on_direction hχ hcalib).1,
 131   (prime_calibration_forces_identity_on_direction hχ hcalib).2.1,
 132   onRatioOrbit_toRat p⟩
 133
 134/-! ## Existence of the forced cost on the completion -/
 135
 136/-- **Existence of the forced cost.** The canonical cost `J` exists on the
 137    completion R_delta: it is the quotient-native `onRatioOrbit` on `RatioOrbit`,
 138    which computes `(q + q⁻¹)/2 − 1` on the rational display. The completion
 139    `PRCRealNullClosed` carries this cost via the rational embedding
 140    `PRCRealNullClosed.ofRat`, and the cost is closed under the countable
 141    field `T` (see `PRCCostOnField.jcost_mem_T`). -/
 142theorem forced_cost_exists_on_completion :
 143    ∃ (J : RatioOrbit → RatioOrbit),
 144      ∀ q : RatioOrbit,
 145        RatioOrbit.crossEq (J q) (J (RatioOrbit.recip q)) ∧
 146        J q = onRatioOrbit q :=
 147  ⟨onRatioOrbit, fun q => ⟨reciprocal_symmetric q, rfl⟩⟩
 148
 149/-! ## The open all-primes target -/
 150
 151/-- **Open target.** One-point calibration at `two` forces global identity:
 152    every `PRCRatioCharacter` calibrated at `two` is calibrated at every
 153    nonzero ratio orbit. This is the all-prime-directions statement that
 154    `PRCNativeCostUniqueness` leaves OPEN. The capstone above provides
 155    per-direction rigidity; propagating one-point calibration across
 156    independent prime directions is the remaining content. -/
 157def target_global_identity_from_one_point_calibration : Prop :=
 158  target_OnePointCalibrationForcesGlobalIdentity
 159
 160/-! ## Field-display connection (documented; uses classical ℝ)
 161
 162    The quotient-native cost `onRatioOrbit q` and the field-display cost
 163    `Cost.Jcost x` (from `PRCCostOnField`) agree on the rational display:
 164    both compute `(x + x⁻¹)/2 − 1`. The field-display step uses Mathlib's
 165    classical `ℝ` (via `Cost.Jcost`), which carries `Classical.choice`.
 166    It is documented here but NOT routed through the capstone theorem,
 167    which is proved choice-free on the quotient-native carrier `RatioOrbit`.
 168
 169    The connection is:
 170    `Cost.Jcost q.toRat = (q.toRat + q.toRat⁻¹)/2 − 1 = (onRatioOrbit q).toRat`
 171    (by `unfold Cost.Jcost` in `PRCCostOnField` and `onRatioOrbit_toRat`).
 172
 173    The countable field `T` from `PRCCostOnField` is closed under `Cost.Jcost`
 174    (see `jcost_mem_T`), so the cost dynamics stay countable. The constants
 175    π, φ, e, and α⁻¹ all live in `T` (see `cost_and_constants_share_one_countable_field`).
 176    The continuum is required nowhere in the cost-and-constants loop. -/
 177
 178end IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum
 179