IndisputableMonolith.Cost.GaugeOrbitClassification

   1/-
   2# The anchor-free gauge classification, on one named import
   3
   4`GaugeOrbitIsSignedPowerFamily` said: every inhabitant of the anchor-free structural cost
   5ledger is either the sign cost or the sign-extended power cost of some nonnegative integer
   6exponent, and nothing else. It was OPEN, resting on two unformalized imports plus prose
   7glue. This module proves it, conditional on ONE hypothesis, the six exponentials input
   8already named in `Cost.TraceRationalExponent`.
   9
  10What changed is that the second import is gone. Erdős's theorem, that a monotone completely
  11multiplicative function on the positive integers is a power, is now proved from nothing in
  12`Cost.MonotoneMultiplicativePower` by Howe's argument, so it enters as a theorem and not as
  13a hypothesis.
  14
  15The chain, in the order the file builds it:
  16
  171. Above one the trace order and the value order agree (`le_of_trace_le`), so the ledger's
  18   monotonicity of costs on positive integer orbits becomes monotonicity of the extracted
  19   character. That plus complete multiplicativity is exactly Howe's hypothesis pack.
  202. Howe gives `χ(n) = n^c` for one real `c ≥ 0`, and the nondegenerate branch forces
  21   `c > 0` because `χ(2)` is the anchor root, which exceeds one.
  223. The traces of the cost are displays of carrier elements, hence rational, so the six
  23   exponentials input applies and `c` is a positive integer `k`
  24   (`exponent_is_positive_integer`).
  254. Multiplicativity carries `χ` from the integers to every positive rational, orientation
  26   reversal carries it across zero, and the cost is `J ∘ χ` throughout, which is the
  27   sign-extended power cost of exponent `k`.
  28
  29The degenerate branch, where the trace at two is exactly two, is the sign cost, and it is
  30handled first because the extraction that produces `χ` divides by `r² - 1`.
  31
  32Nothing here is conditional on the ledger being nonempty or on the exponent being odd. Both
  33parities occur; that was settled in `GaugeOrbitFromRealCharacter` by construction.
  34-/
  35
  36import IndisputableMonolith.Cost.GaugeOrbitFromRealCharacter
  37import IndisputableMonolith.Cost.MonotoneMultiplicativePower
  38
  39namespace IndisputableMonolith
  40namespace Foundation
  41namespace PrimitiveRecognitionCalculus
  42namespace PRCJCost
  43
  44open IndisputableMonolith.Cost.RealCharacterFactorization
  45  (SansAnchorHypotheses traceDisplay rationalTrace rationalTrace_eq_traceDisplay
  46    rationalTrace_pos_eq_two_of_two_eq_two nontrivialCharacterValue
  47    nontrivialCharacterValue_one nontrivialCharacterValue_mul
  48    nontrivialCharacterValue_recip nontrivialCharacterValue_trace
  49    nontrivialCharacterValue_two nontrivialCharacterValue_principal_on_nat
  50    nontrivialCharacterValue_nat_trace_mono anchorRoot anchorRoot_gt_one)
  51
  52open IndisputableMonolith.Cost.MonotonePower (MonotoneMultiplicative exists_exponent)
  53
  54open IndisputableMonolith.Cost.TraceRationalExponent
  55  (SixExponentialsTraceInput exponent_is_positive_integer)
  56
  57/-! ## The trace order is the value order, above one -/
  58
  59/-- `v ↦ v + v⁻¹` is strictly increasing on `[1,∞)`, so an inequality between traces of
  60principal values is an inequality between the values. This is what turns the ledger's
  61monotonicity condition, which constrains costs, into monotonicity of the character. -/
  62private theorem le_of_trace_le {a b : ℝ} (ha : 1 ≤ a) (hb : 1 ≤ b)
  63    (h : a + a⁻¹ ≤ b + b⁻¹) : a ≤ b := by
  64  by_contra hcon
  65  push_neg at hcon
  66  have ha0 : (0 : ℝ) < a := lt_of_lt_of_le zero_lt_one ha
  67  have hb0 : (0 : ℝ) < b := lt_of_lt_of_le zero_lt_one hb
  68  have hkey : (a + a⁻¹) - (b + b⁻¹) = (a - b) * (a * b - 1) / (a * b) := by
  69    field_simp
  70    ring
  71  have h1 : (0 : ℝ) < a - b := by linarith
  72  have h2 : (0 : ℝ) < a * b - 1 := by nlinarith [mul_le_mul_of_nonneg_left hb ha0.le]
  73  have hpos : 0 < (a - b) * (a * b - 1) / (a * b) :=
  74    div_pos (mul_pos h1 h2) (mul_pos ha0 hb0)
  75  rw [← hkey] at hpos
  76  linarith
  77
  78/-! ## Reading the cost off the trace -/
  79
  80variable {F : RatioOrbit → RatioOrbit}
  81
  82/-- The cost display is the trace display, halved and shifted. -/
  83private theorem cost_display (hS : SansAnchorHypotheses F) (q : RatioOrbit) :
  84    ((F q).toRat : ℝ) = rationalTrace F q.toRat / 2 - 1 := by
  85  rw [rationalTrace_eq_traceDisplay hS q]
  86  simp only [traceDisplay, nativeCostDoubledTrace, doubledTraceValue,
  87    RatioOrbit.mul_toRat, RatioOrbit.add_toRat, two_toRat, RatioOrbit.one_toRat]
  88  push_cast
  89  ring
  90
  91/-- At a zero display orientation reversal alone pins the cost, with no character and no
  92appeal to the zero calibration field. -/
  93private theorem cost_at_zero (hS : SansAnchorHypotheses F) {q : RatioOrbit}
  94    (hq : q.toRat = 0) : (F q).toRat = -1 := by
  95  have h := hS.sign_reversing q q (by rw [hq]; norm_num)
  96  linarith
  97
  98/-- Negative displays are determined by the positive ones. -/
  99private theorem cost_at_neg (hS : SansAnchorHypotheses F) (q : RatioOrbit) :
 100    (F q).toRat = -(F (ratioOrbitOfRat (-q.toRat))).toRat - 2 :=
 101  hS.sign_reversing (ratioOrbitOfRat (-q.toRat)) q
 102    (by rw [ratioOrbitOfRat_toRat]; ring)
 103
 104/-! ## The degenerate branch is the sign cost -/
 105
 106/-- **The degenerate anchor is exactly the sign cost.** If the trace at two is two then the
 107trace is two at every positive display, the cost vanishes there, and orientation reversal
 108fills in the rest. -/
 109theorem degenerate_is_signGauge (hS : SansAnchorHypotheses F)
 110    (htwo : rationalTrace F 2 = 2) (q : RatioOrbit) :
 111    RatioOrbit.crossEq (F q) (signGaugeNativeCost q) := by
 112  refine dispCross ?_
 113  rw [signGaugeNativeCost_toRat]
 114  rcases lt_trichotomy q.toRat 0 with hneg | hzero | hpos
 115  · have hpospart : (0 : ℚ) < -q.toRat := by linarith
 116    have hp : (F (ratioOrbitOfRat (-q.toRat))).toRat = 0 := by
 117      have h := cost_display hS (ratioOrbitOfRat (-q.toRat))
 118      rw [ratioOrbitOfRat_toRat,
 119        rationalTrace_pos_eq_two_of_two_eq_two hS htwo hpospart] at h
 120      norm_num at h
 121      exact_mod_cast h
 122    rw [cost_at_neg hS q, hp, signGaugeCostDisplay, if_neg (not_lt.mpr hneg.le),
 123      if_neg (ne_of_lt hneg)]
 124    norm_num
 125  · rw [cost_at_zero hS hzero, signGaugeCostDisplay,
 126      if_neg (by rw [hzero]; exact lt_irrefl 0), if_pos hzero]
 127  · have h := cost_display hS q
 128    rw [rationalTrace_pos_eq_two_of_two_eq_two hS htwo hpos] at h
 129    norm_num at h
 130    rw [signGaugeCostDisplay, if_pos hpos]
 131    exact_mod_cast h
 132
 133/-! ## The nondegenerate branch: Howe, then six exponentials -/
 134
 135/-- The extracted character, restricted to the positive integers, satisfies exactly the
 136hypotheses of Erdős's theorem. Complete multiplicativity is the extraction's own
 137multiplicativity; monotonicity is the ledger's, read through `le_of_trace_le`. -/
 138private theorem natChar_monotoneMultiplicative (hS : SansAnchorHypotheses F)
 139    (hnt : rationalTrace F 2 ≠ 2) :
 140    MonotoneMultiplicative (fun n : ℕ => nontrivialCharacterValue F (n : ℚ)) where
 141  unit := by simpa using nontrivialCharacterValue_one hS hnt
 142  mul := by
 143    intro m n hm hn
 144    have hmq : ((m : ℕ) : ℚ) ≠ 0 := by exact_mod_cast (show m ≠ 0 by omega)
 145    have hnq : ((n : ℕ) : ℚ) ≠ 0 := by exact_mod_cast (show n ≠ 0 by omega)
 146    simpa using nontrivialCharacterValue_mul hS hnt hmq hnq
 147  mono := by
 148    intro m n hm hmn
 149    exact le_of_trace_le (nontrivialCharacterValue_principal_on_nat hS hnt m hm)
 150      (nontrivialCharacterValue_principal_on_nat hS hnt n (le_trans hm hmn))
 151      (nontrivialCharacterValue_nat_trace_mono hS hnt hm hmn)
 152
 153/-- **The exponent is a positive integer.** Howe supplies the real exponent, the anchor root
 154makes it positive, and the six exponentials input makes it an integer. This is the only
 155place the import is used. -/
 156theorem exists_nat_exponent (hsix : SixExponentialsTraceInput)
 157    (hS : SansAnchorHypotheses F) (hnt : rationalTrace F 2 ≠ 2) :
 158    ∃ k : ℕ, 1 ≤ k ∧ ∀ n : ℕ, 1 ≤ n →
 159      nontrivialCharacterValue F (n : ℚ) = ((n : ℝ)) ^ k := by
 160  obtain ⟨c, _, hc⟩ := exists_exponent (natChar_monotoneMultiplicative hS hnt)
 161  have h2 : nontrivialCharacterValue F ((2 : ℕ) : ℚ) = anchorRoot F := by
 162    simpa using nontrivialCharacterValue_two hS hnt
 163  have hroot : 1 < anchorRoot F := anchorRoot_gt_one hS hnt
 164  have hc2 : (((2 : ℕ) : ℝ)) ^ c = anchorRoot F := by
 165    rw [← hc 2 (by norm_num), h2]
 166  have hcpos : 0 < c := by
 167    by_contra hle
 168    push_neg at hle
 169    have hmono : (((2 : ℕ) : ℝ)) ^ c ≤ (((2 : ℕ) : ℝ)) ^ (0 : ℝ) :=
 170      Real.rpow_le_rpow_of_exponent_le (by norm_num) hle
 171    rw [Real.rpow_zero, hc2] at hmono
 172    linarith
 173  have htrace : ∀ n : ℕ, 2 ≤ n → n ≤ 5 →
 174      ∃ t : ℚ, ((n : ℝ)) ^ c + (((n : ℝ)) ^ c)⁻¹ = (t : ℝ) := by
 175    intro n hn _
 176    have hnq : ((n : ℕ) : ℚ) ≠ 0 := by exact_mod_cast (show n ≠ 0 by omega)
 177    refine ⟨(nativeCostDoubledTrace F (ratioOrbitOfRat ((n : ℕ) : ℚ))).toRat, ?_⟩
 178    rw [← hc n (by omega), nontrivialCharacterValue_trace hS hnt hnq]
 179    rfl
 180  obtain ⟨k, hk1, hck⟩ := exponent_is_positive_integer hsix hcpos htrace
 181  refine ⟨k, hk1, fun n hn => ?_⟩
 182  rw [hc n hn, hck]
 183  exact Real.rpow_natCast _ _
 184
 185/-- Multiplicativity carries the power law from the integers to every positive rational. -/
 186theorem char_at_pos (hS : SansAnchorHypotheses F) (hnt : rationalTrace F 2 ≠ 2)
 187    {k : ℕ} (hk : ∀ n : ℕ, 1 ≤ n → nontrivialCharacterValue F (n : ℚ) = ((n : ℝ)) ^ k)
 188    {x : ℚ} (hx : 0 < x) :
 189    nontrivialCharacterValue F x = ((x ^ k : ℚ) : ℝ) := by
 190  have hnumpos : 0 < x.num := Rat.num_pos.mpr hx
 191  have hapos : 0 < x.num.toNat := by omega
 192  have hbpos : 0 < x.den := x.pos
 193  have haa : ((x.num.toNat : ℕ) : ℚ) ≠ 0 := by exact_mod_cast hapos.ne'
 194  have hbb : ((x.den : ℕ) : ℚ) ≠ 0 := by exact_mod_cast hbpos.ne'
 195  have hxrep : ((x.num.toNat : ℕ) : ℚ) / ((x.den : ℕ) : ℚ) = x := by
 196    have hnum : ((x.num.toNat : ℕ) : ℚ) = ((x.num : ℤ) : ℚ) := by
 197      exact_mod_cast Int.toNat_of_nonneg (le_of_lt hnumpos)
 198    rw [hnum]
 199    exact Rat.num_div_den x
 200  have hmul := nontrivialCharacterValue_mul hS hnt haa (inv_ne_zero hbb)
 201  rw [← div_eq_mul_inv, hxrep, nontrivialCharacterValue_recip hS hnt hbb,
 202    hk _ hapos, hk _ hbpos] at hmul
 203  have hqk : x ^ k = ((x.num.toNat : ℕ) : ℚ) ^ k / ((x.den : ℕ) : ℚ) ^ k := by
 204    conv_lhs => rw [← hxrep]
 205    rw [div_pow]
 206  rw [hmul, hqk]
 207  push_cast
 208  ring
 209
 210/-- On a positive display the cost is `J` of the `k`-th power. -/
 211theorem cost_at_pos (hS : SansAnchorHypotheses F) (hnt : rationalTrace F 2 ≠ 2)
 212    {k : ℕ} (hk : ∀ n : ℕ, 1 ≤ n → nontrivialCharacterValue F (n : ℚ) = ((n : ℝ)) ^ k)
 213    {q : RatioOrbit} (hq : 0 < q.toRat) :
 214    (F q).toRat = jq (q.toRat ^ k) := by
 215  have hv := char_at_pos hS hnt hk hq
 216  have hd := cost_display hS q
 217  have htr := nontrivialCharacterValue_trace hS hnt (ne_of_gt hq)
 218  have hcast : ((F q).toRat : ℝ) = ((jq (q.toRat ^ k) : ℚ) : ℝ) := by
 219    rw [hd, ← htr, hv]
 220    push_cast [jq]
 221    ring
 222  exact_mod_cast hcast
 223
 224/-- **The nondegenerate branch is a sign-extended power cost.** -/
 225theorem nontrivial_is_signedPower (hS : SansAnchorHypotheses F)
 226    (hnt : rationalTrace F 2 ≠ 2) {k : ℕ} (hk1 : 1 ≤ k)
 227    (hk : ∀ n : ℕ, 1 ≤ n → nontrivialCharacterValue F (n : ℚ) = ((n : ℝ)) ^ k) :
 228    ∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (signedPowerNativeCost (k - 1) q) := by
 229  obtain ⟨m, rfl⟩ : ∃ m : ℕ, k = m + 1 := ⟨k - 1, by omega⟩
 230  intro q
 231  refine dispCross ?_
 232  rw [signedPowerNativeCost_toRat]
 233  simp only [Nat.add_sub_cancel]
 234  rcases lt_trichotomy q.toRat 0 with hneg | hzero | hpos
 235  · have hpospart : (0 : ℚ) < -q.toRat := by linarith
 236    have hp : (F (ratioOrbitOfRat (-q.toRat))).toRat = jq ((-q.toRat) ^ (m + 1)) := by
 237      have h := cost_at_pos hS hnt hk (q := ratioOrbitOfRat (-q.toRat))
 238        (by rw [ratioOrbitOfRat_toRat]; exact hpospart)
 239      rwa [ratioOrbitOfRat_toRat] at h
 240    rw [cost_at_neg hS q, hp, signedPow, abs_of_neg hneg,
 241      show q.toRat * (-q.toRat) ^ m = -((-q.toRat) ^ (m + 1)) by ring, jq_neg]
 242  · rw [cost_at_zero hS hzero, hzero, signedPow_zero_arg]
 243    norm_num [jq]
 244  · rw [cost_at_pos hS hnt hk hpos, signedPow, abs_of_pos hpos]
 245    congr 1
 246    ring
 247
 248/-! ## Nondegeneracy is one equation at one point, and it is strictness
 249
 250The classification admits exponent zero, the sign cost, and that member charges nothing at
 251any positive ratio, so it undercuts `J` without competing with it
 252(`Cost.UnitFromMinimality.exponent_zero_undercuts_everything`). Selection therefore needs a
 253nondegeneracy hypothesis, and the fair objection is that this looks like a new dial: an extra
 254postulate with content of its own, added to rescue the answer.
 255
 256It is not. For an inhabitant of the anchor-free ledger, all of the following are the same
 257condition: it charges something at the single orbit two, it charges something somewhere on
 258the positive ratios, the ledger's monotonicity holds strictly at some pair, and it is not the
 259sign cost. So nondegeneracy adds no surface beyond the strict form of a hypothesis the ledger
 260already carries, and it is decided by one rational equation at one point.
 261
 262None of this needs the six exponentials input or Erdős's theorem. The entire dichotomy is the
 263degenerate branch of the trace at two, which `degenerate_is_signGauge` settled above, so
 264these results are unconditional where the classification is not.
 265
 266What the degenerate member is, stated precisely, because "charges nothing" is the wrong
 267description: `signGauge_sees_orientation_only` says it charges the full reversal penalty at
 268every negative ratio and nothing at every positive one. It is not a cost that is free. It is
 269a cost that records which way a comparison points and never how far apart its sides are. The
 270content of nondegeneracy is that cost sees magnitude. -/
 271
 272/-- Cost vanishes at orbit two exactly when the trace there takes the degenerate value. -/
 273theorem vanishes_at_two_iff_trace_two (hS : SansAnchorHypotheses F) :
 274    (F two).toRat = 0 ↔ rationalTrace F 2 = 2 := by
 275  have hd := cost_display hS two
 276  rw [two_toRat] at hd
 277  constructor
 278  · intro h
 279    rw [h] at hd
 280    push_cast at hd
 281    linarith
 282  · intro h
 283    rw [h] at hd
 284    have hz : ((F two).toRat : ℝ) = 0 := by rw [hd]; norm_num
 285    exact_mod_cast hz
 286
 287/-- **Charging nothing at one point is charging nothing anywhere.** An inhabitant that is
 288free at orbit two is free at every positive ratio, however far apart its sides are. -/
 289theorem vanishes_at_two_iff_flat (hS : SansAnchorHypotheses F) :
 290    (F two).toRat = 0 ↔ ∀ q : RatioOrbit, 0 < q.toRat → (F q).toRat = 0 := by
 291  constructor
 292  · intro h q hq
 293    have hd := cost_display hS q
 294    rw [rationalTrace_pos_eq_two_of_two_eq_two hS ((vanishes_at_two_iff_trace_two hS).mp h) hq]
 295      at hd
 296    have hz : ((F q).toRat : ℝ) = 0 := by rw [hd]; norm_num
 297    exact_mod_cast hz
 298  · intro h
 299    exact h two (by rw [two_toRat]; norm_num)
 300
 301/-- A nondegenerate inhabitant charges a strictly positive amount at orbit two, so the
 302condition may be read as an inequality rather than a disequality. -/
 303theorem charges_positively_at_two (hS : SansAnchorHypotheses F)
 304    (hne : (F two).toRat ≠ 0) : 0 < (F two).toRat := by
 305  have hge : (2 : ℝ) ≤ rationalTrace F 2 := by
 306    have h := IndisputableMonolith.Cost.RealCharacterFactorization.rationalTrace_nat_ge_two hS
 307      (n := 2) (by norm_num)
 308    simpa using h
 309  have hgt : (2 : ℝ) < rationalTrace F 2 :=
 310    lt_of_le_of_ne hge (Ne.symm fun h => hne ((vanishes_at_two_iff_trace_two hS).mpr h))
 311  have hd := cost_display hS two
 312  rw [two_toRat] at hd
 313  have hpos : (0 : ℝ) < ((F two).toRat : ℝ) := by rw [hd]; linarith
 314  exact_mod_cast hpos
 315
 316/-- **Nondegeneracy is the strict form of the ledger's monotonicity.** Charging anything at
 317orbit two is equivalent to the cost order being strict at some pair of positive ratios. The
 318ledger assumes monotonicity non-strictly (`PRCNativeCostMonotone` is `≤ → ≤`), and the only
 319inhabitant that keeps it flat is the sign cost. -/
 320theorem strict_somewhere_iff_charges_at_two (hS : SansAnchorHypotheses F) :
 321    (∃ a b : RatioOrbit, 0 < a.toRat ∧ 0 < b.toRat ∧ a.toRat ≤ b.toRat ∧
 322        (F a).toRat < (F b).toRat)
 323      ↔ (F two).toRat ≠ 0 := by
 324  constructor
 325  · rintro ⟨a, b, ha, hb, -, hlt⟩ hzero
 326    have hflat := (vanishes_at_two_iff_flat hS).mp hzero
 327    rw [hflat a ha, hflat b hb] at hlt
 328    exact absurd hlt (lt_irrefl 0)
 329  · intro hne
 330    refine ⟨RatioOrbit.one, two, ?_, ?_, ?_, ?_⟩
 331    · rw [RatioOrbit.one_toRat]; norm_num
 332    · rw [two_toRat]; norm_num
 333    · rw [RatioOrbit.one_toRat, two_toRat]; norm_num
 334    · rw [hS.base_sans_two.unit_zero, RatioOrbit.zero_toRat]
 335      exact charges_positively_at_two hS hne
 336
 337/-- **Nondegeneracy is exactly the exclusion of the sign cost**, with no reference to
 338exponents and no appeal to the classification. -/
 339theorem charges_at_two_iff_not_signGauge (hS : SansAnchorHypotheses F) :
 340    (F two).toRat ≠ 0 ↔
 341      ¬ ∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (signGaugeNativeCost q) := by
 342  constructor
 343  · intro hne hall
 344    have h := crossDisp (hall two)
 345    rw [signGaugeNativeCost_toRat, two_toRat, signGaugeCostDisplay,
 346      if_pos (by norm_num : (0 : ℚ) < 2)] at h
 347    exact hne h
 348  · intro hnot hzero
 349    exact hnot (degenerate_is_signGauge hS ((vanishes_at_two_iff_trace_two hS).mp hzero))
 350
 351/-- What the degenerate member actually is. It charges the full reversal penalty at every
 352negative ratio and nothing at every positive one: a cost that records orientation and never
 353magnitude. So the nondegeneracy hypothesis is not "assume cost is not free"; it is "assume
 354cost sees how far apart the two sides are". -/
 355theorem signGauge_sees_orientation_only (q : RatioOrbit) :
 356    (0 < q.toRat → (signGaugeNativeCost q).toRat = 0) ∧
 357      (q.toRat < 0 → (signGaugeNativeCost q).toRat = -2) := by
 358  refine ⟨fun hq => ?_, fun hq => ?_⟩
 359  · rw [signGaugeNativeCost_toRat, signGaugeCostDisplay, if_pos hq]
 360  · rw [signGaugeNativeCost_toRat, signGaugeCostDisplay, if_neg (not_lt.mpr hq.le),
 361      if_neg (ne_of_lt hq)]
 362
 363/-! ## The classification -/
 364
 365/-- **The anchor-free gauge classification, on one named import.** Every inhabitant of the
 366anchor-free structural cost ledger is the sign cost or the sign-extended power cost of a
 367nonnegative integer exponent. The only hypothesis is the six exponentials input; the Erdős
 368step is now the theorem `Cost.MonotonePower.exists_exponent`.
 369
 370Two things this does NOT say. It does not say the exponent is odd: both parities are
 371inhabited, by construction in `GaugeOrbitFromRealCharacter`. And it does not select `J`:
 372selection is leastness, which lives in `Cost.UnitFromMinimality`. -/
 373theorem GaugeOrbitIsSignedPowerFamily_of_sixExponentials
 374    (hsix : SixExponentialsTraceInput) : GaugeOrbitIsSignedPowerFamily := by
 375  intro G hG
 376  have hS := realCharacterFactorizationHypotheses_of_structural hG
 377  by_cases htwo : rationalTrace G 2 = 2
 378  · exact Or.inl (degenerate_is_signGauge hS htwo)
 379  · obtain ⟨k, hk1, hk⟩ := exists_nat_exponent hsix hS htwo
 380    exact Or.inr ⟨k - 1, nontrivial_is_signedPower hS htwo hk1 hk⟩
 381
 382/-! ### Axiom audit -/
 383
 384#print axioms degenerate_is_signGauge
 385#print axioms vanishes_at_two_iff_trace_two
 386#print axioms vanishes_at_two_iff_flat
 387#print axioms charges_positively_at_two
 388#print axioms strict_somewhere_iff_charges_at_two
 389#print axioms charges_at_two_iff_not_signGauge
 390#print axioms signGauge_sees_orientation_only
 391#print axioms exists_nat_exponent
 392#print axioms nontrivial_is_signedPower
 393#print axioms GaugeOrbitIsSignedPowerFamily_of_sixExponentials
 394
 395end PRCJCost
 396end PrimitiveRecognitionCalculus
 397end Foundation
 398end IndisputableMonolith
 399