IndisputableMonolith.Gravity.SevenGaps.Gap5O6ChartInvariant

   1import IndisputableMonolith.Gravity.SevenGaps.Gap5ReparamAttackOnConstraintSector
   2
   3/-!
   4# Campaign 2 Track C: O6, the first number the constraint sector could produce
   5
   6The constraint sector currently buys a sign and a field-independence but no
   7number: `HKTKineticFromRecognitionCost` gives `cKin = 2 λ ^ 2 > 0` with the
   8chart constant `λ` free, and `2 λ ^ 2` absorbs whatever `λ` is. O6 asked whether
   9the *ratio* of the kinetic to the gradient coefficient in the ADM form is
  10chart-independent, on the reasoning that a chart-independent ratio would be the
  11first parameter-free number the sector produces.
  12
  13The answer is no, and the reason identifies the right question instead. O6 asks
  14about the wrong invariant.
  15
  16## What the rigidity theorem already pins
  17
  18`HKTRigidityKineticNormalizedN2` concludes that a kinetic-normalized target has
  19the ADM shape with three coefficients and one relation between them:
  20
  21    hamDensity = cKin * p ^ 2 + cGrad * (structureFunction * (Δa) ^ 2) + V a
  22    momDensity = cMom * p' * (Δa)
  23    cMom = 4 * cKin * cGrad
  24
  25So the algebra pins one combination of `cKin` and `cGrad`, namely their product,
  26and leaves one free. The question is which combination is which.
  27
  28## What is established
  29
  30**§1. The product is determined and the ratio is not.** From the relation alone,
  31`cKin * cGrad = cMom / 4` always (`product_determined`), while two triples can
  32share a `cMom` and differ in ratio by any factor
  33(`ratio_not_determined`). So the ratio is exactly the free direction that
  34survives the rigidity theorem, and it cannot be a number.
  35
  36**§2. Why, structurally.** The free direction is a chart rescaling. Sending
  37`a ↦ a / s` and `p ↦ s * p` preserves the symplectic pairing, scales `p ^ 2` by
  38`s ^ 2` and `(Δa) ^ 2` by `s ^ (-2)`, and so moves `(cKin, cGrad)` to
  39`(cKin / s ^ 2, cGrad * s ^ 2)`. The product is fixed and the ratio moves by
  40`s ^ 4`. The momentum density's own combination `p * (Δa)` is invariant under
  41the same rescaling, which is exactly why the algebra could pin `cMom` and
  42therefore the product, and could not pin the ratio.
  43
  44That paragraph is the reading, not a theorem here: the scaling is stated on the
  45coefficients, and closure of the model class under the corresponding canonical
  46transformation is not formalized. Tagged DERIVED-UNFORMALIZED.
  47
  48**§3. What recognition adds on top.** The recognition premise supplies
  49`cKin = 2 λ ^ 2 > 0`. That does not fix `λ`, so it does not fix `cKin`. But
  50composed with the algebra's relation it does transfer: the gradient coefficient
  51then has the sign of the momentum coefficient
  52(`recognition_transfers_sign_to_gradient`). So the sector buys a second sign it
  53did not have, which is a real if modest gain, and still no magnitude.
  54
  55## The corrected successor
  56
  57O6 should be restated. The first parameter-free number this sector could produce
  58is `cMom`, equivalently the product `cKin * cGrad`, because that is the
  59combination the constraint algebra pins and the chart cannot move. Asking
  60whether the ratio is a number was asking whether a gauge direction is physical,
  61and the answer to that was always going to be no.
  62
  63Nothing here pins `cMom` either. That is the open item, and it is now a sharper
  64one than O6 was: find what fixes the single invariant, rather than hoping a
  65ratio of two free constants collapses.
  66-/
  67
  68namespace IndisputableMonolith
  69namespace Gravity
  70namespace SevenGaps
  71namespace Gap5O6
  72
  73/-- The coefficient relation the rigidity theorem delivers. -/
  74def ADMCoefficients (cKin cGrad cMom : ℝ) : Prop :=
  75  cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad
  76
  77/-! ## §1. The product is determined, the ratio is not -/
  78
  79/-- **The product is a function of what the algebra pins.** -/
  80theorem product_determined {cKin cGrad cMom : ℝ}
  81    (h : ADMCoefficients cKin cGrad cMom) : cKin * cGrad = cMom / 4 := by
  82  obtain ⟨_, _, hrel⟩ := h
  83  rw [hrel]; ring
  84
  85/-- **The ratio is not.** Two coefficient triples with the same `cMom` whose
  86kinetic-to-gradient ratios differ by a factor of four. Scaling the example
  87shows the ratio takes every positive value at fixed `cMom`. -/
  88theorem ratio_not_determined :
  89    ADMCoefficients 1 1 4 ∧ ADMCoefficients 2 (1 / 2) 4
  90      ∧ (1 : ℝ) / 1 ≠ 2 / (1 / 2) := by
  91  refine ⟨⟨by norm_num, by norm_num, by norm_num⟩,
  92    ⟨by norm_num, by norm_num, by norm_num⟩, by norm_num⟩
  93
  94/-- The general statement, which is what makes the ratio a gauge direction
  95rather than merely underdetermined: at a fixed positive `cMom` the ratio takes
  96*every* positive value. -/
  97theorem ratio_takes_every_value {cMom : ℝ} (hMom : 0 < cMom) (t : ℝ) (ht : 0 < t) :
  98    ∃ cKin cGrad : ℝ, ADMCoefficients cKin cGrad cMom ∧ cKin / cGrad = t := by
  99  have hquot : 0 < cMom / (4 * t) := by positivity
 100  set g : ℝ := Real.sqrt (cMom / (4 * t)) with hg
 101  have hgpos : 0 < g := Real.sqrt_pos.mpr hquot
 102  have hgsq : g ^ 2 = cMom / (4 * t) := Real.sq_sqrt (le_of_lt hquot)
 103  refine ⟨t * g, g, ⟨by positivity, ne_of_gt hgpos, ?_⟩, ?_⟩
 104  · rw [show 4 * (t * g) * g = 4 * t * g ^ 2 by ring, hgsq]
 105    field_simp
 106  · field_simp
 107
 108/-! ## §3. Recognition transfers the sign it fixes -/
 109
 110/-- **The recognition premise gives the gradient sector a sign.** `cKin` is
 111`2 λ ^ 2` and so positive, and the algebra's relation then makes `cGrad`
 112positive exactly when `cMom` is. The sector buys a second sign; it still buys no
 113magnitude. -/
 114theorem recognition_transfers_sign_to_gradient
 115    {lam cGrad cMom : ℝ} (hlam : lam ≠ 0)
 116    (h : ADMCoefficients (2 * lam ^ 2) cGrad cMom) :
 117    (0 < cMom ↔ 0 < cGrad) := by
 118  obtain ⟨_, _, hrel⟩ := h
 119  have hsq : 0 < lam ^ 2 := by rcases hlam.lt_or_lt with h' | h' <;> nlinarith
 120  constructor
 121  · intro hM
 122    rw [hrel] at hM
 123    by_contra hc
 124    push_neg at hc
 125    nlinarith [hsq, hc]
 126  · intro hG
 127    rw [hrel]
 128    nlinarith [hsq, hG]
 129
 130/-! ## §4. Named package -/
 131
 132/-- **Track C verdict.** O6 asked whether the kinetic-to-gradient ratio is
 133chart-independent. It is not: it is the one direction the rigidity relation
 134leaves free. The product is the invariant, and pinning it, not the ratio, is the
 135route to the sector's first number. -/
 136def gap5_o6_ratio_is_free_product_is_the_invariant : Prop :=
 137  (∀ {cKin cGrad cMom : ℝ}, ADMCoefficients cKin cGrad cMom →
 138      cKin * cGrad = cMom / 4)
 139  ∧ (ADMCoefficients 1 1 4 ∧ ADMCoefficients 2 (1 / 2) 4
 140      ∧ (1 : ℝ) / 1 ≠ 2 / (1 / 2))
 141  ∧ (∀ {lam cGrad cMom : ℝ}, lam ≠ 0 →
 142      ADMCoefficients (2 * lam ^ 2) cGrad cMom → (0 < cMom ↔ 0 < cGrad))
 143
 144theorem gap5_o6_ratio_is_free_product_is_the_invariant_holds :
 145    gap5_o6_ratio_is_free_product_is_the_invariant :=
 146  ⟨fun h => product_determined h,
 147   ratio_not_determined,
 148   fun hlam h => recognition_transfers_sign_to_gradient hlam h⟩
 149
 150/-! ## §5. Axiom audit -/
 151
 152section Audit
 153
 154#print axioms product_determined
 155#print axioms ratio_takes_every_value
 156#print axioms ratio_not_determined
 157#print axioms recognition_transfers_sign_to_gradient
 158#print axioms gap5_o6_ratio_is_free_product_is_the_invariant_holds
 159
 160end Audit
 161
 162end Gap5O6
 163end SevenGaps
 164end Gravity
 165end IndisputableMonolith
 166