IndisputableMonolith.Cost.GaugeOrbitFromRealCharacter
IndisputableMonolith/Cost/GaugeOrbitFromRealCharacter.lean · 479 lines · 41 declarations
show as:
view math explainer →
1/-
2# Gauge orbit composition from real characters
3
4The proposed odd-power classification has a degenerate boundary member. The
5anchor-free structural ledger admits the sign character, whose value on every
6positive rational is one and whose exponent is zero. Its generated cost is zero
7on positive ratios, minus two on negative ratios, and minus one at zero.
8
9This module packages the structural-to-real-factorization bridge and proves
10that the sign member is a countermodel to `GaugeOrbitIsOddPowerFamily`.
11
12It then goes one step further, because the corrected target was wrong too. The second half
13of the file shows that the ledger admits an inhabitant of EVERY nonnegative integer
14exponent, via the sign-extended character `x ↦ x·|x|^m`, so
15`GaugeOrbitIsSignOrOddPowerFamily` is refuted as well and the live target is
16`GaugeOrbitIsSignedPowerFamily`. The even-power refutation that had been read as excluding
17even exponents excludes only the parameterization `q ↦ J(q^n)`, which forgets the sign.
18-/
19
20import IndisputableMonolith.Cost.RealCharacterFactorization
21import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostStructuralLedger
22
23namespace IndisputableMonolith
24namespace Foundation
25namespace PrimitiveRecognitionCalculus
26namespace PRCJCost
27
28/-- The structural ledger fields imply the light hypothesis pack used by the
29real-character factorization theorem. -/
30theorem realCharacterFactorizationHypotheses_of_structural
31 {F : RatioOrbit → RatioOrbit}
32 (hF : PRCStructuralNativeCostHypothesesSansAnchor F) :
33 IndisputableMonolith.Cost.RealCharacterFactorization.SansAnchorHypotheses F where
34 base_sans_two :=
35 { reciprocal := hF.base_sans_two.reciprocal
36 normalized_invariant := hF.base_sans_two.normalized_invariant
37 canonical_rcl := hF.base_sans_two.canonical_rcl
38 unit_zero := hF.base_sans_two.unit_zero }
39 sign_reversing := fun q r hr => hF.sign_reversing q r hr
40 monotone := by
41 intro a b ha hb hab
42 exact hF.monotone a b ha hb hab
43 zero_calibrated := hF.zero_calibrated
44
45/-- Every structural anchor-free cost has the real factorization proved in
46`RealCharacterFactorization`. -/
47theorem structural_sansAnchor_realCharacterFactorization
48 {F : RatioOrbit → RatioOrbit}
49 (hF : PRCStructuralNativeCostHypothesesSansAnchor F) :
50 ∃ χ : RatioOrbit → ℝ,
51 IndisputableMonolith.Cost.RealCharacterFactorization.PRCRealRatioCharacter χ ∧
52 (∀ q : RatioOrbit, 0 < q.toRat →
53 ((F q).toRat : ℝ) =
54 IndisputableMonolith.Cost.RealCharacterFactorization.costFromRealCharacter χ q) ∧
55 (∀ n : ℕ, 2 ≤ n → n ≤ 5 →
56 ∃ t : ℚ,
57 χ (IndisputableMonolith.Cost.RealCharacterFactorization.natOrbit n) +
58 (χ (IndisputableMonolith.Cost.RealCharacterFactorization.natOrbit n))⁻¹ =
59 (t : ℝ)) :=
60 IndisputableMonolith.Cost.RealCharacterFactorization.SansAnchorRealCharacterFactorizationTarget_proved F
61 (realCharacterFactorizationHypotheses_of_structural hF)
62
63/-- Display of the zero-exponent sign cost. -/
64def signGaugeCostDisplay (x : ℚ) : ℚ :=
65 if 0 < x then 0 else if x = 0 then -1 else -2
66
67/-- The cost generated by the sign character. -/
68def signGaugeNativeCost (q : RatioOrbit) : RatioOrbit :=
69 if 0 < q.toRat then RatioOrbit.zero
70 else if q.toRat = 0 then ratioOrbitOfRat (-1)
71 else ratioOrbitOfRat (-2)
72
73theorem signGaugeNativeCost_toRat (q : RatioOrbit) :
74 (signGaugeNativeCost q).toRat = signGaugeCostDisplay q.toRat := by
75 by_cases hp : 0 < q.toRat
76 · rw [signGaugeNativeCost, if_pos hp, RatioOrbit.zero_toRat,
77 signGaugeCostDisplay, if_pos hp]
78 · by_cases hz : q.toRat = 0
79 · rw [signGaugeNativeCost, if_neg hp, if_pos hz, ratioOrbitOfRat_toRat,
80 signGaugeCostDisplay, if_neg hp, if_pos hz]
81 · rw [signGaugeNativeCost, if_neg hp, if_neg hz, ratioOrbitOfRat_toRat,
82 signGaugeCostDisplay, if_neg hp, if_neg hz]
83
84theorem signGaugeNativeCost_base_sans_two :
85 PRCNativeCostHypothesesSansTwoCalibration signGaugeNativeCost where
86 reciprocal := by
87 intro q
88 rw [RatioOrbit.crossEq_iff_toRat_eq, signGaugeNativeCost_toRat,
89 signGaugeNativeCost_toRat, RatioOrbit.recip_toRat]
90 by_cases hz : q.toRat = 0
91 · simp [signGaugeCostDisplay, hz]
92 · rcases lt_or_gt_of_ne hz with hn | hp
93 · have hi : q.toRat⁻¹ < 0 := inv_lt_zero.mpr hn
94 simp [signGaugeCostDisplay, hz, hn.not_gt, inv_ne_zero hz, hi.not_gt]
95 · have hi : 0 < q.toRat⁻¹ := inv_pos.mpr hp
96 simp [signGaugeCostDisplay, hp, hi]
97 normalized_invariant := by
98 intro q
99 rw [RatioOrbit.crossEq_iff_toRat_eq, signGaugeNativeCost_toRat,
100 signGaugeNativeCost_toRat, DistinctionNat.normalizeRatio_toRat]
101 canonical_rcl := by
102 intro x y hx hy
103 rw [RatioOrbit.crossEq_iff_toRat_eq]
104 simp only [RatioOrbit.add_toRat, RatioOrbit.mul_toRat,
105 signGaugeNativeCost_toRat, div_toRat, two_toRat]
106 rcases lt_or_gt_of_ne hx with hxn | hxp
107 · rcases lt_or_gt_of_ne hy with hyn | hyp
108 · have hmul : 0 < x.toRat * y.toRat := mul_pos_of_neg_of_neg hxn hyn
109 have hdiv : 0 < x.toRat / y.toRat := div_pos_of_neg_of_neg hxn hyn
110 norm_num [signGaugeCostDisplay, hmul, hdiv, hxn.not_gt, hyn.not_gt,
111 ne_of_lt hxn, ne_of_lt hyn]
112 · have hmul : x.toRat * y.toRat < 0 := mul_neg_of_neg_of_pos hxn hyp
113 have hdiv : x.toRat / y.toRat < 0 := div_neg_of_neg_of_pos hxn hyp
114 norm_num [signGaugeCostDisplay, hmul.not_gt, hdiv.not_gt, hxn.not_gt,
115 hyp, ne_of_lt hmul, ne_of_lt hdiv, ne_of_lt hxn, ne_of_gt hyp]
116 · rcases lt_or_gt_of_ne hy with hyn | hyp
117 · have hmul : x.toRat * y.toRat < 0 := mul_neg_of_pos_of_neg hxp hyn
118 have hdiv : x.toRat / y.toRat < 0 := div_neg_of_pos_of_neg hxp hyn
119 norm_num [signGaugeCostDisplay, hmul.not_gt, hdiv.not_gt, hxp,
120 hyn.not_gt, ne_of_lt hmul, ne_of_lt hdiv, ne_of_gt hxp, ne_of_lt hyn]
121 · have hmul : 0 < x.toRat * y.toRat := mul_pos hxp hyp
122 have hdiv : 0 < x.toRat / y.toRat := div_pos hxp hyp
123 norm_num [signGaugeCostDisplay, hmul, hdiv, hxp, hyp,
124 ne_of_gt hxp, ne_of_gt hyp]
125 unit_zero := by
126 rw [signGaugeNativeCost, if_pos (by rw [RatioOrbit.one_toRat]; norm_num)]
127
128theorem signGaugeNativeCost_signReversing :
129 PRCNativeCostSignReversing signGaugeNativeCost := by
130 intro q r hr
131 rw [signGaugeNativeCost_toRat, signGaugeNativeCost_toRat, hr]
132 rcases lt_trichotomy q.toRat 0 with hn | hz | hp
133 · have hnegpos : 0 < -q.toRat := neg_pos.mpr hn
134 norm_num [signGaugeCostDisplay, hn.not_gt, ne_of_lt hn, hnegpos]
135 · rw [hz]
136 norm_num [signGaugeCostDisplay]
137 · have hnegneg : -q.toRat < 0 := neg_neg_of_pos hp
138 norm_num [signGaugeCostDisplay, hp, hnegneg.not_gt, ne_of_lt hnegneg]
139
140theorem signGaugeNativeCost_monotone :
141 PRCNativeCostMonotone signGaugeNativeCost := by
142 rintro a b ⟨m, hm, ha⟩ ⟨n, hn, hb⟩ _
143 rw [signGaugeNativeCost_toRat, signGaugeNativeCost_toRat]
144 have hapos : 0 < a.toRat := by
145 rw [ha]
146 exact_mod_cast (show 0 < m by omega)
147 have hbpos : 0 < b.toRat := by
148 rw [hb]
149 exact_mod_cast (show 0 < n by omega)
150 simp [signGaugeCostDisplay, hapos, hbpos]
151
152theorem signGaugeNativeCost_zero_calibrated :
153 PRCDoubledTraceZeroCalibrated
154 (nativeCostDoubledTrace signGaugeNativeCost) := by
155 rw [PRCDoubledTraceZeroCalibrated, RatioOrbit.crossEq_iff_toRat_eq]
156 simp only [nativeCostDoubledTrace, doubledTraceValue, RatioOrbit.mul_toRat,
157 RatioOrbit.add_toRat, two_toRat, RatioOrbit.one_toRat,
158 signGaugeNativeCost_toRat, RatioOrbit.zero_toRat]
159 norm_num [signGaugeCostDisplay]
160
161/-- The zero-exponent sign member satisfies every field of the anchor-free
162structural ledger. -/
163theorem signGaugeNativeCost_sansAnchor :
164 PRCStructuralNativeCostHypothesesSansAnchor signGaugeNativeCost where
165 base_sans_two := signGaugeNativeCost_base_sans_two
166 sign_reversing := signGaugeNativeCost_signReversing
167 monotone := signGaugeNativeCost_monotone
168 zero_calibrated := signGaugeNativeCost_zero_calibrated
169
170/-- The sign member takes the degenerate trace value two at the anchor. -/
171theorem signGaugeNativeCost_rationalTrace_two :
172 IndisputableMonolith.Cost.RealCharacterFactorization.rationalTrace
173 signGaugeNativeCost 2 = 2 := by
174 rw [IndisputableMonolith.Cost.RealCharacterFactorization.rationalTrace,
175 IndisputableMonolith.Cost.RealCharacterFactorization.traceDisplay,
176 nativeCostDoubledTrace, doubledTraceValue]
177 simp only [RatioOrbit.mul_toRat, RatioOrbit.add_toRat, two_toRat,
178 RatioOrbit.one_toRat, signGaugeNativeCost_toRat, ratioOrbitOfRat_toRat]
179 norm_num [signGaugeCostDisplay]
180
181/-- The factorization theorem extracts the sign character on this member. -/
182theorem signGaugeNativeCost_realCharacterCandidate (q : RatioOrbit) :
183 IndisputableMonolith.Cost.RealCharacterFactorization.realCharacterCandidate
184 signGaugeNativeCost q =
185 IndisputableMonolith.Cost.RealCharacterFactorization.rationalSignCharacter
186 q.toRat := by
187 rw [IndisputableMonolith.Cost.RealCharacterFactorization.realCharacterCandidate,
188 if_pos signGaugeNativeCost_rationalTrace_two]
189
190/-- The extracted character has exponent zero. -/
191theorem signGaugeNativeCost_characterExponent_zero :
192 IndisputableMonolith.Cost.RealCharacterFactorization.exponentOfCharacter
193 (IndisputableMonolith.Cost.RealCharacterFactorization.realCharacterCandidate
194 signGaugeNativeCost) = 0 := by
195 rw [IndisputableMonolith.Cost.RealCharacterFactorization.exponentOfCharacter,
196 signGaugeNativeCost_realCharacterCandidate,
197 IndisputableMonolith.Cost.RealCharacterFactorization.natOrbit_toRat]
198 have hsign :
199 IndisputableMonolith.Cost.RealCharacterFactorization.rationalSignCharacter
200 (((2 : ℕ) : ℚ)) = 1 := by
201 norm_num
202 [IndisputableMonolith.Cost.RealCharacterFactorization.rationalSignCharacter]
203 rw [hsign]
204 norm_num
205
206/-- The extracted sign character is not any positive odd-integer power,
207already at the anchor. -/
208theorem signGaugeNativeCost_character_not_oddPower (k : ℕ) :
209 IndisputableMonolith.Cost.RealCharacterFactorization.realCharacterCandidate
210 signGaugeNativeCost
211 (IndisputableMonolith.Cost.RealCharacterFactorization.natOrbit 2) ≠
212 (2 : ℝ) ^ (2 * k + 1) := by
213 rw [signGaugeNativeCost_realCharacterCandidate,
214 IndisputableMonolith.Cost.RealCharacterFactorization.natOrbit_toRat]
215 have hsign :
216 IndisputableMonolith.Cost.RealCharacterFactorization.rationalSignCharacter
217 (((2 : ℕ) : ℚ)) = 1 := by
218 norm_num
219 [IndisputableMonolith.Cost.RealCharacterFactorization.rationalSignCharacter]
220 rw [hsign]
221 exact ne_of_lt (one_lt_pow₀ (by norm_num) (by omega))
222
223/-- The sign member cannot equal any positive odd-power cost. -/
224theorem signGaugeNativeCost_not_oddPowerGeneratedNativeCost (k : ℕ) :
225 ¬ ∀ q : RatioOrbit,
226 RatioOrbit.crossEq (signGaugeNativeCost q)
227 (oddPowerGeneratedNativeCost k q) := by
228 intro h
229 have htwo := crossDisp (h two)
230 rw [signGaugeNativeCost_toRat, oddPowerGeneratedNativeCost_toRat,
231 two_toRat] at htwo
232 have hexp : 2 * k + 1 ≠ 0 := by omega
233 have hp : (1 : ℚ) < 2 ^ (2 * k + 1) :=
234 one_lt_pow₀ (by norm_num) hexp
235 have hzero : jq ((2 : ℚ) ^ (2 * k + 1)) = 0 := by
236 norm_num [signGaugeCostDisplay] at htwo
237 exact htwo.symm
238 have hone := jq_eq_zero (ne_of_gt (lt_trans zero_lt_one hp)) hzero
239 exact (ne_of_gt hp) hone
240
241/-- The proposed classification is false: it omits the zero-exponent sign
242member already allowed by the structural ledger. -/
243theorem GaugeOrbitIsOddPowerFamily_refuted :
244 ¬ GaugeOrbitIsOddPowerFamily := by
245 intro h
246 obtain ⟨k, hk⟩ := h signGaugeNativeCost signGaugeNativeCost_sansAnchor
247 exact signGaugeNativeCost_not_oddPowerGeneratedNativeCost k hk
248
249/-- **OPEN**, corrected classification. Every anchor-free structural inhabitant
250is either the zero-exponent sign cost or an odd-power generated cost. -/
251def GaugeOrbitIsSignOrOddPowerFamily : Prop :=
252 ∀ F : RatioOrbit → RatioOrbit, PRCStructuralNativeCostHypothesesSansAnchor F →
253 (∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (signGaugeNativeCost q)) ∨
254 ∃ k : ℕ, ∀ q : RatioOrbit,
255 RatioOrbit.crossEq (F q) (oddPowerGeneratedNativeCost k q)
256
257/-! ## The even exponents are inhabited too, so the corrected target also fails
258
259Orientation reversal constrains the character at `-1`. It does not constrain the parity of
260the exponent, and the two were being confused.
261
262What is true is that `powerGeneratedNativeCost (2k+2)`, the cost `q ↦ J(q^(2k+2))`, fails
263sign reversal (`powerGeneratedNativeCost_not_signReversing`): an even power forgets the sign
264of its argument, so the cost cannot reverse. That is a fact about the parameterization
265`q ↦ q^n`, and the ledger constrains costs rather than parameterizations.
266
267Take instead the character `χ(x) = x·|x|^m`, which is `sgn(x)·|x|^(m+1)`. It is completely
268multiplicative for every `m` with no case analysis, it sends `-1` to `-1`, so its generated
269cost reverses orientation while carrying the exponent `m+1`, whatever the parity. At even
270`m` it reproduces the odd powers exactly (`signedPowerNativeCost_even_eq_oddPower`). At odd
271`m` it is new. The member `m = 1` has exponent two, charges `J(4) = 9/8` at the anchor, and
272is therefore neither the sign cost nor any odd power, which refutes
273`GaugeOrbitIsSignOrOddPowerFamily`. Its doubled trace at two is `17/4`, whose principal root
274is `4 = 2^2`, so the extracted character really does have the even exponent.
275
276Net: the ledger contains an inhabitant of every nonnegative integer exponent, and the honest
277target is `GaugeOrbitIsSignedPowerFamily` below. This is the third correction to this
278classification in one day, and all three came from building the witness rather than
279reasoning about the family. -/
280
281/-- `signedPow m x = sgn(x)·|x|^(m+1)`, written as `x·|x|^m` so that multiplicativity is one
282`abs_mul` away and needs no sign case analysis. -/
283def signedPow (m : ℕ) (x : ℚ) : ℚ := x * |x| ^ m
284
285@[simp] theorem signedPow_zero_arg (m : ℕ) : signedPow m 0 = 0 := by
286 simp [signedPow]
287
288@[simp] theorem signedPow_one_arg (m : ℕ) : signedPow m 1 = 1 := by
289 simp [signedPow]
290
291theorem signedPow_mul (m : ℕ) (x y : ℚ) :
292 signedPow m (x * y) = signedPow m x * signedPow m y := by
293 simp only [signedPow, abs_mul, mul_pow]
294 ring
295
296theorem signedPow_inv (m : ℕ) (x : ℚ) :
297 signedPow m x⁻¹ = (signedPow m x)⁻¹ := by
298 rw [signedPow, signedPow, abs_inv, inv_pow, mul_inv]
299
300theorem signedPow_div (m : ℕ) (x y : ℚ) :
301 signedPow m (x / y) = signedPow m x / signedPow m y := by
302 rw [div_eq_mul_inv, signedPow_mul, signedPow_inv, div_eq_mul_inv]
303
304theorem signedPow_neg (m : ℕ) (x : ℚ) :
305 signedPow m (-x) = -signedPow m x := by
306 simp only [signedPow, abs_neg]
307 ring
308
309theorem signedPow_ne_zero {m : ℕ} {x : ℚ} (hx : x ≠ 0) : signedPow m x ≠ 0 :=
310 mul_ne_zero hx (pow_ne_zero m (abs_ne_zero.mpr hx))
311
312theorem signedPow_of_one_le {m : ℕ} {x : ℚ} (hx : 1 ≤ x) : 1 ≤ signedPow m x := by
313 have hx0 : (0 : ℚ) ≤ x := le_trans zero_le_one hx
314 have hpow : (1 : ℚ) ≤ x ^ m := one_le_pow₀ hx
315 rw [signedPow, abs_of_nonneg hx0]
316 nlinarith
317
318theorem signedPow_mono {m : ℕ} {a b : ℚ} (ha : 1 ≤ a) (hab : a ≤ b) :
319 signedPow m a ≤ signedPow m b := by
320 have ha0 : (0 : ℚ) ≤ a := le_trans zero_le_one ha
321 have hb0 : (0 : ℚ) ≤ b := le_trans ha0 hab
322 have hpow : a ^ m ≤ b ^ m := pow_le_pow_left₀ ha0 hab m
323 have h1 : (1 : ℚ) ≤ a ^ m := one_le_pow₀ ha
324 rw [signedPow, signedPow, abs_of_nonneg ha0, abs_of_nonneg hb0]
325 calc a * a ^ m ≤ b * a ^ m :=
326 mul_le_mul_of_nonneg_right hab (le_trans zero_le_one h1)
327 _ ≤ b * b ^ m := mul_le_mul_of_nonneg_left hpow hb0
328
329/-- At an even index the sign-extended power is the ordinary odd power. -/
330theorem signedPow_even (k : ℕ) (x : ℚ) : signedPow (2 * k) x = x ^ (2 * k + 1) := by
331 have habs : |x| ^ (2 * k) = x ^ (2 * k) := by
332 rw [pow_mul, sq_abs, ← pow_mul]
333 rw [signedPow, habs]
334 ring
335
336/-- The cost generated by the sign-extended power character `χ(x) = sgn(x)·|x|^(m+1)`. -/
337def signedPowerNativeCost (m : ℕ) (q : RatioOrbit) : RatioOrbit :=
338 if q.toRat = 1 then RatioOrbit.zero
339 else onRatioOrbit (ratioOrbitOfRat (signedPow m q.toRat))
340
341theorem signedPowerNativeCost_toRat (m : ℕ) (q : RatioOrbit) :
342 (signedPowerNativeCost m q).toRat = jq (signedPow m q.toRat) := by
343 rw [signedPowerNativeCost]
344 by_cases h : q.toRat = 1
345 · rw [if_pos h, RatioOrbit.zero_toRat, h, signedPow_one_arg]
346 norm_num [jq]
347 · rw [if_neg h, jq_onRatioOrbit, ratioOrbitOfRat_toRat]
348
349theorem signedPowerNativeCost_base (m : ℕ) :
350 PRCNativeCostHypothesesSansTwoCalibration (signedPowerNativeCost m) where
351 reciprocal := by
352 intro q
353 rw [RatioOrbit.crossEq_iff_toRat_eq, signedPowerNativeCost_toRat,
354 signedPowerNativeCost_toRat, RatioOrbit.recip_toRat, signedPow_inv, jq_inv]
355 normalized_invariant := by
356 intro q
357 rw [RatioOrbit.crossEq_iff_toRat_eq, signedPowerNativeCost_toRat,
358 signedPowerNativeCost_toRat, DistinctionNat.normalizeRatio_toRat]
359 canonical_rcl := by
360 intro x y hx hy
361 rw [RatioOrbit.crossEq_iff_toRat_eq]
362 simp only [RatioOrbit.add_toRat, RatioOrbit.mul_toRat,
363 signedPowerNativeCost_toRat, div_toRat, two_toRat]
364 rw [signedPow_mul, signedPow_div]
365 exact jq_rcl (signedPow_ne_zero hx) (signedPow_ne_zero hy)
366 unit_zero := by
367 rw [signedPowerNativeCost, if_pos RatioOrbit.one_toRat]
368
369theorem signedPowerNativeCost_signReversing (m : ℕ) :
370 PRCNativeCostSignReversing (signedPowerNativeCost m) := by
371 intro q r hr
372 rw [signedPowerNativeCost_toRat, signedPowerNativeCost_toRat, hr,
373 signedPow_neg, jq_neg]
374
375theorem signedPowerNativeCost_monotone (m : ℕ) :
376 PRCNativeCostMonotone (signedPowerNativeCost m) := by
377 rintro a b ⟨n, hn, han⟩ ⟨_, _, _⟩ hab
378 rw [signedPowerNativeCost_toRat, signedPowerNativeCost_toRat]
379 have ha1 : (1 : ℚ) ≤ a.toRat := by
380 rw [han]
381 exact_mod_cast hn
382 exact jq_mono (signedPow_of_one_le ha1) (signedPow_mono ha1 hab)
383
384theorem signedPowerNativeCost_zero_calibrated (m : ℕ) :
385 PRCDoubledTraceZeroCalibrated
386 (nativeCostDoubledTrace (signedPowerNativeCost m)) := by
387 rw [PRCDoubledTraceZeroCalibrated, RatioOrbit.crossEq_iff_toRat_eq]
388 simp only [nativeCostDoubledTrace, doubledTraceValue, RatioOrbit.mul_toRat,
389 RatioOrbit.add_toRat, two_toRat, RatioOrbit.one_toRat,
390 signedPowerNativeCost_toRat, RatioOrbit.zero_toRat, signedPow_zero_arg]
391 norm_num [jq]
392
393/-- **Every nonnegative integer exponent inhabits the anchor-free ledger.** The
394sign-extended power character satisfies every structural field, including orientation
395reversal, at every index and so at both parities of exponent. -/
396theorem signedPowerNativeCost_sansAnchor (m : ℕ) :
397 PRCStructuralNativeCostHypothesesSansAnchor (signedPowerNativeCost m) where
398 base_sans_two := signedPowerNativeCost_base m
399 sign_reversing := signedPowerNativeCost_signReversing m
400 monotone := signedPowerNativeCost_monotone m
401 zero_calibrated := signedPowerNativeCost_zero_calibrated m
402
403/-- The even indices recover the known odd-power family, so the new family contains it. -/
404theorem signedPowerNativeCost_even_eq_oddPower (k : ℕ) (q : RatioOrbit) :
405 (signedPowerNativeCost (2 * k) q).toRat =
406 (oddPowerGeneratedNativeCost k q).toRat := by
407 rw [signedPowerNativeCost_toRat, oddPowerGeneratedNativeCost_toRat, signedPow_even]
408
409/-- The exponent-two member charges `J(4)` at the anchor. -/
410theorem signedPowerNativeCost_one_two_toRat :
411 (signedPowerNativeCost 1 two).toRat = jq 4 := by
412 rw [signedPowerNativeCost_toRat, two_toRat]
413 norm_num [signedPow]
414
415theorem signedPowerNativeCost_one_not_oddPower (k : ℕ) :
416 ¬ ∀ q : RatioOrbit,
417 RatioOrbit.crossEq (signedPowerNativeCost 1 q)
418 (oddPowerGeneratedNativeCost k q) := by
419 intro h
420 have htwo := crossDisp (h two)
421 rw [signedPowerNativeCost_one_two_toRat, oddPowerGeneratedNativeCost_toRat,
422 two_toRat] at htwo
423 have hone : (1 : ℚ) ≤ (2 : ℚ) ^ (2 * k + 1) := one_le_pow₀ (by norm_num)
424 have heq : (4 : ℚ) = 2 ^ (2 * k + 1) :=
425 jq_inj_ge_one (by norm_num) hone htwo
426 rcases Nat.eq_zero_or_pos k with hk | hk
427 · subst hk
428 norm_num at heq
429 · have h8 : (8 : ℚ) ≤ 2 ^ (2 * k + 1) := by
430 calc (8 : ℚ) = 2 ^ 3 := by norm_num
431 _ ≤ 2 ^ (2 * k + 1) := pow_le_pow_right₀ (by norm_num) (by omega)
432 rw [← heq] at h8
433 norm_num at h8
434
435theorem signedPowerNativeCost_one_not_signGauge :
436 ¬ ∀ q : RatioOrbit,
437 RatioOrbit.crossEq (signedPowerNativeCost 1 q) (signGaugeNativeCost q) := by
438 intro h
439 have htwo := crossDisp (h two)
440 rw [signedPowerNativeCost_one_two_toRat, signGaugeNativeCost_toRat,
441 two_toRat] at htwo
442 norm_num [signGaugeCostDisplay, jq] at htwo
443
444/-- **The corrected classification is false too.** The exponent-two sign-extended member is
445neither the sign cost nor any odd power. -/
446theorem GaugeOrbitIsSignOrOddPowerFamily_refuted :
447 ¬ GaugeOrbitIsSignOrOddPowerFamily := by
448 intro h
449 rcases h (signedPowerNativeCost 1) (signedPowerNativeCost_sansAnchor 1) with
450 hsign | ⟨k, hk⟩
451 · exact signedPowerNativeCost_one_not_signGauge hsign
452 · exact signedPowerNativeCost_one_not_oddPower k hk
453
454/-- **PROVED**, on one named import, in `Cost.GaugeOrbitClassification`
455(`GaugeOrbitIsSignedPowerFamily_of_sixExponentials`). Corrected a third time before it
456closed: every anchor-free structural inhabitant is the sign cost (exponent zero) or a
457sign-extended power cost (exponent `m+1`), so the classification allows every nonnegative
458integer exponent and no more. The odd powers are the even indices by
459`signedPowerNativeCost_even_eq_oddPower`. The single hypothesis of the proof is
460`Cost.TraceRationalExponent.SixExponentialsTraceInput`. -/
461def GaugeOrbitIsSignedPowerFamily : Prop :=
462 ∀ F : RatioOrbit → RatioOrbit, PRCStructuralNativeCostHypothesesSansAnchor F →
463 (∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (signGaugeNativeCost q)) ∨
464 ∃ m : ℕ, ∀ q : RatioOrbit,
465 RatioOrbit.crossEq (F q) (signedPowerNativeCost m q)
466
467#print axioms structural_sansAnchor_realCharacterFactorization
468#print axioms signGaugeNativeCost_sansAnchor
469#print axioms signGaugeNativeCost_character_not_oddPower
470#print axioms GaugeOrbitIsOddPowerFamily_refuted
471#print axioms signedPowerNativeCost_sansAnchor
472#print axioms signedPowerNativeCost_even_eq_oddPower
473#print axioms GaugeOrbitIsSignOrOddPowerFamily_refuted
474
475end PRCJCost
476end PrimitiveRecognitionCalculus
477end Foundation
478end IndisputableMonolith
479