IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum.CharacterRigidityForcing

   1/-
   2  PrimitiveRecognitionCalculus/Continuum/CharacterRigidityForcing.lean
   3
   4  Lane: CONSTRUCTIVE CONTINUUM R_δ — calibrated character-rigidity.
   5
   6  This additive module attacks the rigidity gap that
   7  `PRCNativeCostUniqueness` leaves OPEN: after setting `g = F + 1` the RCL
   8  has the d'Alembert form `g(xy) + g(x/y) = 2 g(x) g(y)`, and one-point
   9  calibration at `2` does not by itself control all prime directions.
  10
  11  We decompose the missing **calibrated character-rigidity** target into
  12  small named helper lemmas (each independently true and choice-free) and
  13  prove the headline single-prime / two-generator rigidity FROM them:
  14  the set of calibration points of a `PRCRatioCharacter` is closed under
  15  product, reciprocal and the unit, hence calibration in one prime
  16  direction rigidifies the whole cyclic subgroup it generates, and the
  17  generated cost is forced to the canonical PRC J-cost there.
  18
  19  The genuinely open all-primes statement (one-point calibration at `2`
  20  forcing global identity) is named honestly as `def target_*`, NOT faked.
  21
  22  This file cites the committed `PRCJCost` / `PRCNativeCostUniqueness`
  23  names verbatim (`PRCRatioCharacter`, `costFromCharacter`,
  24  `doubledTraceValue`, `doubledTraceValue_congr`, `onRatioOrbit`, `two`,
  25  `RatioOrbit.crossEq`, ...).
  26-/
  27
  28import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness
  29
  30namespace IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum
  31
  32open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  33open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCost
  34
  35/-! ## Calibration predicate -/
  36
  37/-- A character `χ` is *calibrated at* `q` when its value at `q` is
  38cross-equivalent to `q` itself, i.e. `χ` acts as the identity character on
  39the orbit direction `q`.  Calibration at `two` is the single-point datum the
  40PRC cost hypotheses actually carry. -/
  41def CharacterCalibratedAt (χ : RatioOrbit → RatioOrbit) (q : RatioOrbit) : Prop :=
  42  RatioOrbit.crossEq (χ q) q
  43
  44/-! ## Helper lemmas: rational displays of a ratio character -/
  45
  46/-- Multiplicativity of a `PRCRatioCharacter` on the verifier rational display. -/
  47theorem character_mul_toRat {χ : RatioOrbit → RatioOrbit}
  48    (hχ : PRCRatioCharacter χ) (x y : RatioOrbit) :
  49    (χ (RatioOrbit.mul x y)).toRat = (χ x).toRat * (χ y).toRat := by
  50  have h := hχ.multiplicative x y
  51  rw [RatioOrbit.crossEq_iff_toRat_eq] at h
  52  rw [h, RatioOrbit.mul_toRat]
  53
  54/-- The unit normalization of a `PRCRatioCharacter` on the rational display. -/
  55theorem character_one_toRat {χ : RatioOrbit → RatioOrbit}
  56    (hχ : PRCRatioCharacter χ) :
  57    (χ RatioOrbit.one).toRat = 1 := by
  58  have h := hχ.unit
  59  rw [RatioOrbit.crossEq_iff_toRat_eq] at h
  60  rw [h, RatioOrbit.one_toRat]
  61
  62/-- Reciprocal symmetry of a `PRCRatioCharacter` on the rational display. -/
  63theorem character_recip_toRat {χ : RatioOrbit → RatioOrbit}
  64    (hχ : PRCRatioCharacter χ) (x : RatioOrbit) :
  65    (χ (RatioOrbit.recip x)).toRat = (χ x).toRat⁻¹ := by
  66  have h := hχ.reciprocal x
  67  rw [RatioOrbit.crossEq_iff_toRat_eq] at h
  68  rw [h, RatioOrbit.recip_toRat]
  69
  70/-! ## Helper lemmas: the calibration set is a subgroup -/
  71
  72/-- The unit orbit is always a calibration point of a `PRCRatioCharacter`. -/
  73theorem calibrated_one {χ : RatioOrbit → RatioOrbit}
  74    (hχ : PRCRatioCharacter χ) :
  75    CharacterCalibratedAt χ RatioOrbit.one :=
  76  hχ.unit
  77
  78/-- Calibration is closed under products: if `χ` is the identity on `x` and
  79on `y`, multiplicativity forces it to be the identity on `x·y`. -/
  80theorem calibrated_mul {χ : RatioOrbit → RatioOrbit}
  81    (hχ : PRCRatioCharacter χ) {x y : RatioOrbit}
  82    (hx : CharacterCalibratedAt χ x) (hy : CharacterCalibratedAt χ y) :
  83    CharacterCalibratedAt χ (RatioOrbit.mul x y) := by
  84  unfold CharacterCalibratedAt at hx hy ⊢
  85  rw [RatioOrbit.crossEq_iff_toRat_eq] at hx hy ⊢
  86  rw [character_mul_toRat hχ, RatioOrbit.mul_toRat, hx, hy]
  87
  88/-- Calibration is closed under reciprocals. -/
  89theorem calibrated_recip {χ : RatioOrbit → RatioOrbit}
  90    (hχ : PRCRatioCharacter χ) {x : RatioOrbit}
  91    (hx : CharacterCalibratedAt χ x) :
  92    CharacterCalibratedAt χ (RatioOrbit.recip x) := by
  93  unfold CharacterCalibratedAt at hx ⊢
  94  rw [RatioOrbit.crossEq_iff_toRat_eq] at hx ⊢
  95  rw [character_recip_toRat hχ, RatioOrbit.recip_toRat, hx]
  96
  97/-- Two-generator / square case: calibration at `p` propagates to `p·p`. -/
  98theorem calibrated_square {χ : RatioOrbit → RatioOrbit}
  99    (hχ : PRCRatioCharacter χ) {p : RatioOrbit}
 100    (hp : CharacterCalibratedAt χ p) :
 101    CharacterCalibratedAt χ (RatioOrbit.mul p p) :=
 102  calibrated_mul hχ hp hp
 103
 104/-! ## Helper lemmas: cost / trace rigidity from calibration -/
 105
 106/-- The canonical PRC cost respects cross-equivalence of inputs. -/
 107theorem onRatioOrbit_crossEq {a b : RatioOrbit}
 108    (h : RatioOrbit.crossEq a b) :
 109    RatioOrbit.crossEq (onRatioOrbit a) (onRatioOrbit b) := by
 110  rw [RatioOrbit.crossEq_iff_toRat_eq] at h ⊢
 111  rw [onRatioOrbit_toRat, onRatioOrbit_toRat, h]
 112
 113/-- The d'Alembert trace `χ(p) + χ(p)⁻¹` of a calibrated character collapses
 114to the identity trace `p + p⁻¹` on a calibration point. -/
 115theorem character_trace_rigid {χ : RatioOrbit → RatioOrbit}
 116    (hχ : PRCRatioCharacter χ) {p : RatioOrbit}
 117    (hp : CharacterCalibratedAt χ p) :
 118    RatioOrbit.crossEq
 119      (RatioOrbit.add (χ p) (RatioOrbit.recip (χ p)))
 120      (RatioOrbit.add p (RatioOrbit.recip p)) := by
 121  unfold CharacterCalibratedAt at hp
 122  rw [RatioOrbit.crossEq_iff_toRat_eq] at hp ⊢
 123  rw [RatioOrbit.add_toRat, RatioOrbit.add_toRat, RatioOrbit.recip_toRat,
 124    RatioOrbit.recip_toRat, hp]
 125
 126/-- The cost generated by a calibrated character equals the canonical PRC
 127J-cost on a calibration point: `costFromCharacter χ p ≈ onRatioOrbit p`. -/
 128theorem costFromCharacter_rigid {χ : RatioOrbit → RatioOrbit}
 129    (hχ : PRCRatioCharacter χ) {p : RatioOrbit}
 130    (hp : CharacterCalibratedAt χ p) :
 131    RatioOrbit.crossEq (costFromCharacter χ p) (onRatioOrbit p) :=
 132  onRatioOrbit_crossEq hp
 133
 134/-- The doubled d'Alembert trace `2(F+1)` of the generated cost is rigidified
 135to the canonical doubled trace on a calibration point. -/
 136theorem doubledTrace_character_rigid {χ : RatioOrbit → RatioOrbit}
 137    (hχ : PRCRatioCharacter χ) {p : RatioOrbit}
 138    (hp : CharacterCalibratedAt χ p) :
 139    RatioOrbit.crossEq
 140      (doubledTraceValue (costFromCharacter χ p))
 141      (doubledTraceValue (onRatioOrbit p)) :=
 142  doubledTraceValue_congr (costFromCharacter_rigid hχ hp)
 143
 144/-! ## Headline: single-prime / two-generator calibrated rigidity -/
 145
 146/-- **Calibrated character-rigidity (single prime direction).**
 147
 148A `PRCRatioCharacter χ` that is calibrated at a prime direction `p`
 149(`χ p ≈ p`) is rigidified there: it is forced to remain the identity
 150character on `p·p` and on `p⁻¹` (so on the whole cyclic subgroup `p`
 151generates), and the cost it generates is forced to the canonical PRC
 152J-cost `onRatioOrbit p`.  This is exactly the rigidity that calibrated
 153multiplicativity supplies; the global all-primes step requires the
 154separate `target_*` below. -/
 155theorem prime_calibration_forces_identity_on_direction
 156    {χ : RatioOrbit → RatioOrbit} (hχ : PRCRatioCharacter χ)
 157    {p : RatioOrbit} (hcalib : CharacterCalibratedAt χ p) :
 158    CharacterCalibratedAt χ (RatioOrbit.mul p p)
 159      ∧ CharacterCalibratedAt χ (RatioOrbit.recip p)
 160      ∧ RatioOrbit.crossEq (costFromCharacter χ p) (onRatioOrbit p) :=
 161  ⟨calibrated_mul hχ hcalib hcalib,
 162   calibrated_recip hχ hcalib,
 163   costFromCharacter_rigid hχ hcalib⟩
 164
 165/-! ## The genuinely open all-primes target (named, not faked) -/
 166
 167/-- **Open target.**  One-point calibration at `two` forces global identity:
 168every `PRCRatioCharacter` that is calibrated only at the distinguished axis
 169`two` is in fact calibrated (cross-equivalent to the identity character) at
 170every nonzero ratio orbit.  This is the all-prime-directions statement that
 171`PRCNativeCostUniqueness` leaves OPEN; the single-prime lemma above provides
 172the per-direction rigidity, but propagating one-point calibration across
 173independent prime directions is the remaining content.  Stated honestly as a
 174`Prop`, not proved here. -/
 175def target_OnePointCalibrationForcesGlobalIdentity : Prop :=
 176  ∀ χ : RatioOrbit → RatioOrbit, PRCRatioCharacter χ →
 177    CharacterCalibratedAt χ two →
 178      ∀ q : RatioOrbit, q.toRat ≠ 0 → CharacterCalibratedAt χ q
 179
 180end IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum
 181