IndisputableMonolith.Cost.RealCharacterFactorization
IndisputableMonolith/Cost/RealCharacterFactorization.lean · 990 lines · 73 declarations
show as:
view math explainer →
1/-
2# Real-valued character factorization for the anchor-free cost ledger
3
4The carrier-valued factorization target is the wrong type
5(`TraceRationalExponent.no_rational_character_at_trace_three`). What a cost
6exposes is the TRACE. This module records the corrected target and connects it
7to the algebraic core in `RealTraceRoot`.
8
9Imports are kept light (Uniqueness already has a local olean) so the module can
10build under laptop memory pressure. The SansAnchor pack is restated by fields;
11it matches `PRCStructuralNativeCostHypothesesSansAnchor` in the structural
12ledger when that module is available.
13-/
14
15import IndisputableMonolith.Cost.RealTraceRoot
16import IndisputableMonolith.Cost.TraceRationalExponent
17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness
18
19namespace IndisputableMonolith
20namespace Cost
21namespace RealCharacterFactorization
22
23open Foundation.PrimitiveRecognitionCalculus
24open Foundation.PrimitiveRecognitionCalculus.PRCJCost
25open RealTraceRoot
26open TraceRationalExponent
27
28export RealTraceRoot (realTraceRoot realTraceRoot_mul realTraceRoot_add_inv
29 realTraceRoot_ge_one larger_trace_of_diff_sq)
30
31/-! ## Doubled trace from RCL alone -/
32
33/-- The doubled-trace form of the composition law needs only the RCL. The anchor
34at two is not used. -/
35theorem doubledTrace_dAlembert_of_rcl
36 {F : RatioOrbit → RatioOrbit}
37 (hrcl : ∀ {x y : RatioOrbit}, x.toRat ≠ 0 → y.toRat ≠ 0 →
38 RatioOrbit.crossEq
39 (RatioOrbit.add (F (RatioOrbit.mul x y)) (F (div x y)))
40 (RatioOrbit.add
41 (RatioOrbit.add
42 (RatioOrbit.mul two (RatioOrbit.mul (F x) (F y)))
43 (RatioOrbit.mul two (F x)))
44 (RatioOrbit.mul two (F y))))
45 {x y : RatioOrbit} (hx : x.toRat ≠ 0) (hy : y.toRat ≠ 0) :
46 RatioOrbit.crossEq
47 (RatioOrbit.add (nativeCostDoubledTrace F (RatioOrbit.mul x y))
48 (nativeCostDoubledTrace F (div x y)))
49 (RatioOrbit.mul (nativeCostDoubledTrace F x) (nativeCostDoubledTrace F y)) := by
50 have h := hrcl hx hy
51 rw [RatioOrbit.crossEq_iff_toRat_eq] at h ⊢
52 simp only [nativeCostDoubledTrace, doubledTraceValue, RatioOrbit.mul_toRat,
53 RatioOrbit.add_toRat, two_toRat, RatioOrbit.one_toRat] at h ⊢
54 linarith
55
56/-- Same theorem specialized to the native cost pack, using only its RCL field. -/
57theorem doubledTrace_dAlembert_of_native
58 {F : RatioOrbit → RatioOrbit}
59 (hF : PRCNativeCostHypotheses F)
60 {x y : RatioOrbit} (hx : x.toRat ≠ 0) (hy : y.toRat ≠ 0) :
61 RatioOrbit.crossEq
62 (RatioOrbit.add (nativeCostDoubledTrace F (RatioOrbit.mul x y))
63 (nativeCostDoubledTrace F (div x y)))
64 (RatioOrbit.mul (nativeCostDoubledTrace F x) (nativeCostDoubledTrace F y)) :=
65 doubledTrace_dAlembert_of_rcl hF.canonical_rcl hx hy
66
67/-! ## Anchor-free hypotheses, restated lightly -/
68
69def IsPosIntOrbit (q : RatioOrbit) : Prop :=
70 ∃ n : ℕ, 1 ≤ n ∧ q.toRat = (n : ℚ)
71
72def natOrbit (n : ℕ) : RatioOrbit := ratioOrbitOfRat (n : ℚ)
73
74theorem natOrbit_toRat (n : ℕ) : (natOrbit n).toRat = (n : ℚ) :=
75 ratioOrbitOfRat_toRat _
76
77def PRCNativeCostSignReversing (F : RatioOrbit → RatioOrbit) : Prop :=
78 ∀ q r : RatioOrbit, r.toRat = -q.toRat →
79 (F r).toRat = -(F q).toRat - 2
80
81def PRCNativeCostMonotone (F : RatioOrbit → RatioOrbit) : Prop :=
82 ∀ a b : RatioOrbit, IsPosIntOrbit a → IsPosIntOrbit b →
83 a.toRat ≤ b.toRat → (F a).toRat ≤ (F b).toRat
84
85/-- Base sans the two-point anchor: the RCL pack without `two_calibrated`. -/
86structure BaseSansTwo (F : RatioOrbit → RatioOrbit) : Prop where
87 reciprocal :
88 ∀ q, RatioOrbit.crossEq (F q) (F (RatioOrbit.recip q))
89 normalized_invariant :
90 ∀ q, RatioOrbit.crossEq (F q) (F (DistinctionNat.normalizeRatio q))
91 canonical_rcl :
92 ∀ {x y : RatioOrbit}, x.toRat ≠ 0 → y.toRat ≠ 0 →
93 RatioOrbit.crossEq
94 (RatioOrbit.add (F (RatioOrbit.mul x y)) (F (div x y)))
95 (RatioOrbit.add
96 (RatioOrbit.add
97 (RatioOrbit.mul two (RatioOrbit.mul (F x) (F y)))
98 (RatioOrbit.mul two (F x)))
99 (RatioOrbit.mul two (F y)))
100 unit_zero :
101 F RatioOrbit.one = RatioOrbit.zero
102
103/-- Anchor-free pack matching `PRCStructuralNativeCostHypothesesSansAnchor`. -/
104structure SansAnchorHypotheses (F : RatioOrbit → RatioOrbit) : Prop where
105 base_sans_two : BaseSansTwo F
106 sign_reversing : PRCNativeCostSignReversing F
107 monotone : PRCNativeCostMonotone F
108 zero_calibrated : PRCDoubledTraceZeroCalibrated (nativeCostDoubledTrace F)
109
110theorem doubledTrace_dAlembert_of_sansAnchor
111 {F : RatioOrbit → RatioOrbit}
112 (hF : SansAnchorHypotheses F)
113 {x y : RatioOrbit} (hx : x.toRat ≠ 0) (hy : y.toRat ≠ 0) :
114 RatioOrbit.crossEq
115 (RatioOrbit.add (nativeCostDoubledTrace F (RatioOrbit.mul x y))
116 (nativeCostDoubledTrace F (div x y)))
117 (RatioOrbit.mul (nativeCostDoubledTrace F x) (nativeCostDoubledTrace F y)) :=
118 doubledTrace_dAlembert_of_rcl hF.base_sans_two.canonical_rcl hx hy
119
120/-! ## The corrected factorization target -/
121
122structure PRCRealRatioCharacter (χ : RatioOrbit → ℝ) : Prop where
123 unit : χ RatioOrbit.one = 1
124 multiplicative :
125 ∀ x y : RatioOrbit,
126 x.toRat ≠ 0 → y.toRat ≠ 0 →
127 χ (RatioOrbit.mul x y) = χ x * χ y
128 reciprocal :
129 ∀ x : RatioOrbit, x.toRat ≠ 0 → χ (RatioOrbit.recip x) = (χ x)⁻¹
130 nonzero :
131 ∀ x : RatioOrbit, x.toRat ≠ 0 → χ x ≠ 0
132 principal_on_pos_int :
133 ∀ n : ℕ, 1 ≤ n → 1 ≤ χ (natOrbit n)
134
135noncomputable def costFromRealCharacter (χ : RatioOrbit → ℝ) (q : RatioOrbit) : ℝ :=
136 (χ q + (χ q)⁻¹) / 2 - 1
137
138noncomputable def exponentOfCharacter (χ : RatioOrbit → ℝ) : ℝ :=
139 Real.log (χ (natOrbit 2)) / Real.log 2
140
141/-- **The corrected factorization target.** Every inhabitant of the anchor-free
142ledger factors through a real-valued character whose traces at the small bases
143are rational (so the exponent step can fire). -/
144def SansAnchorRealCharacterFactorizationTarget : Prop :=
145 ∀ F : RatioOrbit → RatioOrbit,
146 SansAnchorHypotheses F →
147 ∃ χ : RatioOrbit → ℝ,
148 PRCRealRatioCharacter χ ∧
149 (∀ q : RatioOrbit, 0 < q.toRat →
150 ((F q).toRat : ℝ) = costFromRealCharacter χ q) ∧
151 (∀ n : ℕ, 2 ≤ n → n ≤ 5 →
152 ∃ t : ℚ, χ (natOrbit n) + (χ (natOrbit n))⁻¹ = (t : ℝ))
153
154abbrev SansAnchorRealCharacterFactorizationInput : Prop :=
155 SansAnchorRealCharacterFactorizationTarget
156
157/-! ## Real display and quotient-independent rational trace -/
158
159/-- The real display of the carrier-valued doubled trace. -/
160noncomputable def traceDisplay
161 (F : RatioOrbit → RatioOrbit) (q : RatioOrbit) : ℝ :=
162 ((nativeCostDoubledTrace F q).toRat : ℝ)
163
164theorem traceDisplay_one
165 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F) :
166 traceDisplay F RatioOrbit.one = 2 := by
167 simp only [traceDisplay, nativeCostDoubledTrace, doubledTraceValue,
168 hF.base_sans_two.unit_zero, RatioOrbit.mul_toRat, RatioOrbit.add_toRat,
169 RatioOrbit.zero_toRat, RatioOrbit.one_toRat, two_toRat]
170 norm_num
171
172theorem traceDisplay_recip
173 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
174 (q : RatioOrbit) :
175 traceDisplay F (RatioOrbit.recip q) = traceDisplay F q := by
176 have h := doubledTraceValue_congr (hF.base_sans_two.reciprocal q)
177 rw [RatioOrbit.crossEq_iff_toRat_eq] at h
178 simp only [traceDisplay, nativeCostDoubledTrace]
179 exact_mod_cast h.symm
180
181theorem traceDisplay_dAlembert
182 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
183 {x y : RatioOrbit} (hx : x.toRat ≠ 0) (hy : y.toRat ≠ 0) :
184 traceDisplay F (RatioOrbit.mul x y) + traceDisplay F (div x y) =
185 traceDisplay F x * traceDisplay F y := by
186 have h := doubledTrace_dAlembert_of_sansAnchor hF hx hy
187 rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.add_toRat,
188 RatioOrbit.mul_toRat] at h
189 simp only [traceDisplay]
190 exact_mod_cast h
191
192theorem traceDisplay_posInt_ge_two
193 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
194 {q : RatioOrbit} (hq : IsPosIntOrbit q) :
195 2 ≤ traceDisplay F q := by
196 have hone : IsPosIntOrbit RatioOrbit.one :=
197 ⟨1, by norm_num, by rw [RatioOrbit.one_toRat]; norm_num⟩
198 obtain ⟨n, hn, hqn⟩ := hq
199 have hqone : RatioOrbit.one.toRat ≤ q.toRat := by
200 rw [RatioOrbit.one_toRat, hqn]
201 exact_mod_cast hn
202 have hm := hF.monotone RatioOrbit.one q hone ⟨n, hn, hqn⟩ hqone
203 rw [hF.base_sans_two.unit_zero, RatioOrbit.zero_toRat] at hm
204 simp only [traceDisplay, nativeCostDoubledTrace, doubledTraceValue,
205 RatioOrbit.mul_toRat, RatioOrbit.add_toRat, two_toRat,
206 RatioOrbit.one_toRat]
207 norm_num at hm ⊢
208 exact_mod_cast (show (0 : ℚ) ≤ (F q).toRat from hm)
209
210theorem traceDisplay_two_ge_two
211 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F) :
212 2 ≤ traceDisplay F two :=
213 traceDisplay_posInt_ge_two hF ⟨2, by norm_num, two_toRat⟩
214
215theorem traceDisplay_eq_of_crossEq
216 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
217 {q r : RatioOrbit} (hqr : RatioOrbit.crossEq q r) :
218 traceDisplay F q = traceDisplay F r := by
219 have hq := doubledTraceValue_congr (hF.base_sans_two.normalized_invariant q)
220 have hr := doubledTraceValue_congr (hF.base_sans_two.normalized_invariant r)
221 have hnorm :
222 DistinctionNat.normalizeRatio q = DistinctionNat.normalizeRatio r :=
223 PRCNormalizeRatioCanonicalTarget_proved q r hqr
224 rw [hnorm] at hq
225 have htrace := RatioOrbit.crossEq_trans hq (RatioOrbit.crossEq_symm hr)
226 rw [RatioOrbit.crossEq_iff_toRat_eq] at htrace
227 simp only [traceDisplay, nativeCostDoubledTrace]
228 exact_mod_cast htrace
229
230/-- The doubled trace as an honest function on rational displays. -/
231noncomputable def rationalTrace
232 (F : RatioOrbit → RatioOrbit) (x : ℚ) : ℝ :=
233 traceDisplay F (ratioOrbitOfRat x)
234
235theorem rationalTrace_eq_traceDisplay
236 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
237 (q : RatioOrbit) :
238 rationalTrace F q.toRat = traceDisplay F q := by
239 apply traceDisplay_eq_of_crossEq hF
240 rw [RatioOrbit.crossEq_iff_toRat_eq, ratioOrbitOfRat_toRat]
241
242theorem rationalTrace_one
243 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F) :
244 rationalTrace F 1 = 2 := by
245 calc
246 rationalTrace F 1 = traceDisplay F RatioOrbit.one := by
247 rw [rationalTrace]
248 apply traceDisplay_eq_of_crossEq hF
249 rw [RatioOrbit.crossEq_iff_toRat_eq, ratioOrbitOfRat_toRat,
250 RatioOrbit.one_toRat]
251 _ = 2 := traceDisplay_one hF
252
253theorem rationalTrace_recip
254 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
255 (x : ℚ) :
256 rationalTrace F x⁻¹ = rationalTrace F x := by
257 rw [rationalTrace, rationalTrace]
258 calc
259 traceDisplay F (ratioOrbitOfRat x⁻¹) =
260 traceDisplay F (RatioOrbit.recip (ratioOrbitOfRat x)) := by
261 apply traceDisplay_eq_of_crossEq hF
262 rw [RatioOrbit.crossEq_iff_toRat_eq, ratioOrbitOfRat_toRat,
263 RatioOrbit.recip_toRat, ratioOrbitOfRat_toRat]
264 _ = traceDisplay F (ratioOrbitOfRat x) := traceDisplay_recip hF _
265
266theorem rationalTrace_dAlembert
267 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
268 {x y : ℚ} (hx : x ≠ 0) (hy : y ≠ 0) :
269 rationalTrace F (x * y) + rationalTrace F (x / y) =
270 rationalTrace F x * rationalTrace F y := by
271 let ox := ratioOrbitOfRat x
272 let oy := ratioOrbitOfRat y
273 have hox : ox.toRat ≠ 0 := by
274 change (ratioOrbitOfRat x).toRat ≠ 0
275 rw [ratioOrbitOfRat_toRat]
276 exact hx
277 have hoy : oy.toRat ≠ 0 := by
278 change (ratioOrbitOfRat y).toRat ≠ 0
279 rw [ratioOrbitOfRat_toRat]
280 exact hy
281 have hd := traceDisplay_dAlembert hF hox hoy
282 have hmul :
283 traceDisplay F (RatioOrbit.mul ox oy) = rationalTrace F (x * y) := by
284 symm
285 apply traceDisplay_eq_of_crossEq hF
286 rw [RatioOrbit.crossEq_iff_toRat_eq, ratioOrbitOfRat_toRat,
287 RatioOrbit.mul_toRat]
288 change x * y = (ratioOrbitOfRat x).toRat * (ratioOrbitOfRat y).toRat
289 rw [ratioOrbitOfRat_toRat, ratioOrbitOfRat_toRat]
290 have hdiv :
291 traceDisplay F (div ox oy) = rationalTrace F (x / y) := by
292 symm
293 apply traceDisplay_eq_of_crossEq hF
294 rw [RatioOrbit.crossEq_iff_toRat_eq, ratioOrbitOfRat_toRat, div_toRat]
295 change x / y = (ratioOrbitOfRat x).toRat / (ratioOrbitOfRat y).toRat
296 rw [ratioOrbitOfRat_toRat, ratioOrbitOfRat_toRat]
297 simpa [rationalTrace, ox, oy, hmul, hdiv] using hd
298
299theorem rationalTrace_neg
300 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
301 (x : ℚ) :
302 rationalTrace F (-x) = -rationalTrace F x := by
303 have hsign := hF.sign_reversing (ratioOrbitOfRat x) (ratioOrbitOfRat (-x))
304 (by simp only [ratioOrbitOfRat_toRat])
305 simp only [rationalTrace, traceDisplay, nativeCostDoubledTrace,
306 doubledTraceValue, RatioOrbit.mul_toRat, RatioOrbit.add_toRat,
307 ratioOrbitOfRat_toRat, two_toRat, RatioOrbit.one_toRat]
308 norm_cast
309 linarith
310
311theorem rationalTrace_nat_ge_two
312 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
313 {n : ℕ} (hn : 1 ≤ n) :
314 2 ≤ rationalTrace F n := by
315 change 2 ≤ traceDisplay F (ratioOrbitOfRat (n : ℚ))
316 exact traceDisplay_posInt_ge_two hF
317 ⟨n, hn, ratioOrbitOfRat_toRat (n : ℚ)⟩
318
319/-! ## Symbolic linear extraction -/
320
321/-- Linear extraction from a nondegenerate anchor whose chosen root is `r`. -/
322noncomputable def linearExtraction
323 (T : ℚ → ℝ) (r : ℝ) (x : ℚ) : ℝ :=
324 (r * T (2 * x) - T x) / (r ^ 2 - 1)
325
326private theorem linearExtraction_unit
327 {T : ℚ → ℝ} {r : ℝ}
328 (h1 : T 1 = 2) (hr0 : r ≠ 0) (hrden : r ^ 2 - 1 ≠ 0)
329 (hrtrace : r + r⁻¹ = T 2) :
330 linearExtraction T r 1 = 1 := by
331 have hA : T 2 = (r ^ 2 + 1) / r := by
332 rw [← hrtrace, eq_div_iff hr0]
333 field_simp [hr0]
334 rw [linearExtraction, show (2 : ℚ) * 1 = 2 by norm_num, h1, hA]
335 field_simp [hr0, hrden]
336 ring
337
338private theorem linearExtraction_multiplicative
339 {T : ℚ → ℝ} {r : ℝ}
340 (hrec : ∀ x : ℚ, T x⁻¹ = T x)
341 (hd : ∀ {x y : ℚ}, x ≠ 0 → y ≠ 0 →
342 T (x * y) + T (x / y) = T x * T y)
343 (hr0 : r ≠ 0) (hrden : r ^ 2 - 1 ≠ 0)
344 (hrtrace : r + r⁻¹ = T 2)
345 {x y : ℚ} (hx : x ≠ 0) (hy : y ≠ 0) :
346 linearExtraction T r (x * y) =
347 linearExtraction T r x * linearExtraction T r y := by
348 have htwo : (2 : ℚ) ≠ 0 := by norm_num
349 have hxy : x * y ≠ 0 := mul_ne_zero hx hy
350 have hxdy : x / y ≠ 0 := div_ne_zero hx hy
351 have h2x : (2 : ℚ) * x ≠ 0 := mul_ne_zero htwo hx
352 have h2y : (2 : ℚ) * y ≠ 0 := mul_ne_zero htwo hy
353 have h2xy : (2 : ℚ) * (x * y) ≠ 0 := mul_ne_zero htwo hxy
354 have hx2y : x / ((2 : ℚ) * y) ≠ 0 := div_ne_zero hx h2y
355 have hCC := hd hx hy
356 have hDDraw := hd h2x h2y
357 have hDDprod :
358 ((2 : ℚ) * x) * ((2 : ℚ) * y) = 2 * (2 * (x * y)) := by ring
359 have hDDquot :
360 ((2 : ℚ) * x) / ((2 : ℚ) * y) = x / y := by
361 field_simp [hy]
362 rw [hDDprod, hDDquot] at hDDraw
363 have hanchorRaw := hd htwo h2xy
364 have hanchorProd :
365 (2 : ℚ) * (2 * (x * y)) = 2 * (2 * (x * y)) := rfl
366 have hanchorQuot :
367 (2 : ℚ) / (2 * (x * y)) = (x * y)⁻¹ := by
368 field_simp [hx, hy]
369 rw [hanchorProd, hanchorQuot, hrec (x * y)] at hanchorRaw
370 have hDD :
371 T (2 * x) * T (2 * y) =
372 T 2 * T (2 * (x * y)) - T (x * y) + T (x / y) := by
373 linarith
374 have hDCraw := hd h2x hy
375 have hDCprod : ((2 : ℚ) * x) * y = 2 * (x * y) := by ring
376 have hDCquot : ((2 : ℚ) * x) / y = 2 * (x / y) := by
377 field_simp [hy]
378 rw [hDCprod, hDCquot] at hDCraw
379 have hCDraw := hd hx h2y
380 have hCDprod : x * ((2 : ℚ) * y) = 2 * (x * y) := by ring
381 rw [hCDprod] at hCDraw
382 have hcrossRaw := hd htwo hxdy
383 have hcrossProd : (2 : ℚ) * (x / y) = 2 * (x / y) := rfl
384 have hcrossQuot :
385 (2 : ℚ) / (x / y) = (x / ((2 : ℚ) * y))⁻¹ := by
386 field_simp [hx, hy]
387 rw [hcrossProd, hcrossQuot, hrec (x / ((2 : ℚ) * y))] at hcrossRaw
388 have hcross :
389 T (2 * x) * T y + T x * T (2 * y) =
390 2 * T (2 * (x * y)) + T 2 * T (x / y) := by
391 linarith
392 have hA : T 2 = (r ^ 2 + 1) / r := by
393 rw [← hrtrace, eq_div_iff hr0]
394 field_simp [hr0]
395 have hnum :
396 (r * T (2 * x) - T x) * (r * T (2 * y) - T y) =
397 (r ^ 2 - 1) * (r * T (2 * (x * y)) - T (x * y)) := by
398 calc
399 (r * T (2 * x) - T x) * (r * T (2 * y) - T y) =
400 r ^ 2 * (T (2 * x) * T (2 * y)) -
401 r * (T (2 * x) * T y + T x * T (2 * y)) +
402 T x * T y := by ring
403 _ = r ^ 2 *
404 (T 2 * T (2 * (x * y)) - T (x * y) + T (x / y)) -
405 r * (2 * T (2 * (x * y)) + T 2 * T (x / y)) +
406 (T (x * y) + T (x / y)) := by rw [hDD, hcross, ← hCC]
407 _ = (r ^ 2 - 1) * (r * T (2 * (x * y)) - T (x * y)) := by
408 rw [hA]
409 field_simp [hr0]
410 ring
411 rw [linearExtraction, linearExtraction, linearExtraction,
412 show (2 : ℚ) * (x * y) = 2 * (x * y) by rfl]
413 field_simp [hrden]
414 convert hnum.symm using 1 <;> ring
415
416private theorem linearExtraction_recip_sum
417 {T : ℚ → ℝ} {r : ℝ}
418 (hrec : ∀ x : ℚ, T x⁻¹ = T x)
419 (hd : ∀ {x y : ℚ}, x ≠ 0 → y ≠ 0 →
420 T (x * y) + T (x / y) = T x * T y)
421 (hr0 : r ≠ 0) (hrden : r ^ 2 - 1 ≠ 0)
422 (hrtrace : r + r⁻¹ = T 2)
423 {x : ℚ} (hx : x ≠ 0) :
424 linearExtraction T r x⁻¹ + linearExtraction T r x = T x := by
425 have htwo : (2 : ℚ) ≠ 0 := by norm_num
426 have hinvx : x⁻¹ ≠ 0 := inv_ne_zero hx
427 have hda := hd htwo hx
428 have hmul : (2 : ℚ) * x = 2 * x := rfl
429 have hquot : (2 : ℚ) / x = 2 * x⁻¹ := by
430 rw [div_eq_mul_inv]
431 rw [hmul, hquot] at hda
432 have hA : T 2 = (r ^ 2 + 1) / r := by
433 rw [← hrtrace, eq_div_iff hr0]
434 field_simp [hr0]
435 rw [hA] at hda
436 rw [linearExtraction, linearExtraction, hrec x]
437 have htworecip :
438 (2 : ℚ) * x⁻¹ = 2 * x⁻¹ := rfl
439 rw [htworecip]
440 have hnum :
441 r * T (2 * x⁻¹) - T x + (r * T (2 * x) - T x) =
442 (r ^ 2 - 1) * T x := by
443 calc
444 r * T (2 * x⁻¹) - T x + (r * T (2 * x) - T x) =
445 r * (T (2 * x) + T (2 * x⁻¹)) - 2 * T x := by ring
446 _ = r * (((r ^ 2 + 1) / r) * T x) - 2 * T x := by rw [hda]
447 _ = (r ^ 2 - 1) * T x := by
448 field_simp [hr0]
449 ring
450 field_simp [hr0, hrden]
451 convert hnum using 1 <;> ring
452
453/-- Principal root at the distinguished positive integer two. -/
454noncomputable def anchorRoot (F : RatioOrbit → RatioOrbit) : ℝ :=
455 realTraceRoot (rationalTrace F 2)
456
457/-- The nondegenerate symbolic extraction from the trace at two. -/
458noncomputable def nontrivialCharacterValue
459 (F : RatioOrbit → RatioOrbit) (x : ℚ) : ℝ :=
460 linearExtraction (rationalTrace F) (anchorRoot F) x
461
462theorem anchorRoot_ge_one
463 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F) :
464 1 ≤ anchorRoot F :=
465 realTraceRoot_ge_one (by
466 simpa [rationalTrace] using traceDisplay_two_ge_two hF)
467
468theorem anchorRoot_add_inv
469 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F) :
470 anchorRoot F + (anchorRoot F)⁻¹ = rationalTrace F 2 :=
471 realTraceRoot_add_inv (by
472 simpa [rationalTrace] using traceDisplay_two_ge_two hF)
473
474theorem anchorRoot_gt_one
475 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
476 (hnontrivial : rationalTrace F 2 ≠ 2) :
477 1 < anchorRoot F := by
478 refine lt_of_le_of_ne (anchorRoot_ge_one hF) ?_
479 intro h
480 have hr : anchorRoot F = 1 := h.symm
481 have ht := anchorRoot_add_inv hF
482 rw [hr] at ht
483 norm_num at ht
484 exact hnontrivial ht.symm
485
486theorem anchorRoot_ne_zero
487 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F) :
488 anchorRoot F ≠ 0 :=
489 ne_of_gt (lt_of_lt_of_le zero_lt_one (anchorRoot_ge_one hF))
490
491theorem anchorRoot_sq_sub_one_ne_zero
492 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
493 (hnontrivial : rationalTrace F 2 ≠ 2) :
494 anchorRoot F ^ 2 - 1 ≠ 0 := by
495 have hr := anchorRoot_gt_one hF hnontrivial
496 nlinarith
497
498theorem nontrivialCharacterValue_one
499 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
500 (hnontrivial : rationalTrace F 2 ≠ 2) :
501 nontrivialCharacterValue F 1 = 1 :=
502 linearExtraction_unit (rationalTrace_one hF) (anchorRoot_ne_zero hF)
503 (anchorRoot_sq_sub_one_ne_zero hF hnontrivial) (anchorRoot_add_inv hF)
504
505theorem nontrivialCharacterValue_mul
506 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
507 (hnontrivial : rationalTrace F 2 ≠ 2)
508 {x y : ℚ} (hx : x ≠ 0) (hy : y ≠ 0) :
509 nontrivialCharacterValue F (x * y) =
510 nontrivialCharacterValue F x * nontrivialCharacterValue F y :=
511 linearExtraction_multiplicative (rationalTrace_recip hF)
512 (@rationalTrace_dAlembert F hF) (anchorRoot_ne_zero hF)
513 (anchorRoot_sq_sub_one_ne_zero hF hnontrivial) (anchorRoot_add_inv hF) hx hy
514
515theorem nontrivialCharacterValue_recip_sum
516 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
517 (hnontrivial : rationalTrace F 2 ≠ 2)
518 {x : ℚ} (hx : x ≠ 0) :
519 nontrivialCharacterValue F x⁻¹ + nontrivialCharacterValue F x =
520 rationalTrace F x :=
521 linearExtraction_recip_sum (rationalTrace_recip hF)
522 (@rationalTrace_dAlembert F hF) (anchorRoot_ne_zero hF)
523 (anchorRoot_sq_sub_one_ne_zero hF hnontrivial) (anchorRoot_add_inv hF) hx
524
525/-! ## The degenerate anchor -/
526
527theorem rationalTrace_nat_mono
528 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
529 {m n : ℕ} (hm : 1 ≤ m) (hmn : m ≤ n) :
530 rationalTrace F m ≤ rationalTrace F n := by
531 have hn : 1 ≤ n := le_trans hm hmn
532 have hmono := hF.monotone (natOrbit m) (natOrbit n)
533 ⟨m, hm, natOrbit_toRat m⟩ ⟨n, hn, natOrbit_toRat n⟩
534 (by
535 rw [natOrbit_toRat, natOrbit_toRat]
536 exact_mod_cast hmn)
537 change
538 (F (ratioOrbitOfRat (m : ℚ))).toRat ≤
539 (F (ratioOrbitOfRat (n : ℚ))).toRat at hmono
540 have hmonoR :
541 ((F (ratioOrbitOfRat (m : ℚ))).toRat : ℝ) ≤
542 ((F (ratioOrbitOfRat (n : ℚ))).toRat : ℝ) := by
543 exact_mod_cast hmono
544 simp only [rationalTrace, natOrbit, traceDisplay, nativeCostDoubledTrace,
545 doubledTraceValue, RatioOrbit.mul_toRat, RatioOrbit.add_toRat,
546 two_toRat, RatioOrbit.one_toRat]
547 push_cast
548 linarith
549
550theorem rationalTrace_two_pow_eq_two
551 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
552 (htwo : rationalTrace F 2 = 2) :
553 ∀ k : ℕ, rationalTrace F ((2 : ℚ) ^ k) = 2 := by
554 intro k
555 induction k using Nat.twoStepInduction with
556 | zero =>
557 simpa using rationalTrace_one hF
558 | one =>
559 simpa using htwo
560 | more m ih0 ih1 =>
561 have hx : (2 : ℚ) ^ (m + 1) ≠ 0 := pow_ne_zero _ (by norm_num)
562 have hd := rationalTrace_dAlembert hF hx (by norm_num : (2 : ℚ) ≠ 0)
563 have hprod :
564 (2 : ℚ) ^ (m + 1) * 2 = (2 : ℚ) ^ (m + 2) := by
565 simp [pow_succ]
566 have hquot :
567 (2 : ℚ) ^ (m + 1) / 2 = (2 : ℚ) ^ m := by
568 rw [show m + 1 = m + 1 by rfl, pow_succ]
569 field_simp
570 rw [hprod, hquot, ih0, ih1, htwo] at hd
571 linarith
572
573theorem rationalTrace_nat_eq_two_of_two_eq_two
574 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
575 (htwo : rationalTrace F 2 = 2) :
576 ∀ n : ℕ, 1 ≤ n → rationalTrace F n = 2 := by
577 have hpow2 : ∀ n : ℕ, n ≤ 2 ^ n := by
578 intro n
579 induction n with
580 | zero => norm_num
581 | succ k ih =>
582 have h1 : 1 ≤ 2 ^ k := Nat.one_le_two_pow
583 have hp : 2 ^ (k + 1) = 2 ^ k * 2 := by rw [pow_succ]
584 omega
585 intro n hn
586 have hlow : 2 ≤ rationalTrace F n := rationalTrace_nat_ge_two hF hn
587 have hup := rationalTrace_nat_mono hF hn (hpow2 n)
588 have hcast :
589 (((2 ^ n : ℕ) : ℚ)) = (2 : ℚ) ^ n := by norm_num
590 rw [hcast, rationalTrace_two_pow_eq_two hF htwo n] at hup
591 linarith
592
593theorem rationalTrace_pos_eq_two_of_two_eq_two
594 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
595 (htwo : rationalTrace F 2 = 2)
596 {x : ℚ} (hx : 0 < x) :
597 rationalTrace F x = 2 := by
598 let a := x.num.toNat
599 let b := x.den
600 have hnumpos : 0 < x.num := Rat.num_pos.mpr hx
601 have hapos : 0 < a := by
602 change 0 < x.num.toNat
603 omega
604 have hbpos : 0 < b := by
605 change 0 < x.den
606 exact x.pos
607 have ha1 : 1 ≤ a := hapos
608 have hb1 : 1 ≤ b := hbpos
609 have haa : (a : ℚ) ≠ 0 := by exact_mod_cast hapos.ne'
610 have hbb : (b : ℚ) ≠ 0 := by exact_mod_cast hbpos.ne'
611 have hxrep : (a : ℚ) / (b : ℚ) = x := by
612 change ((x.num.toNat : ℕ) : ℚ) / (x.den : ℚ) = x
613 have hnum :
614 ((x.num.toNat : ℕ) : ℚ) = ((x.num : ℤ) : ℚ) := by
615 exact_mod_cast Int.toNat_of_nonneg (le_of_lt hnumpos)
616 rw [hnum]
617 exact Rat.num_div_den x
618 have hd := rationalTrace_dAlembert hF (x := (a : ℚ)) (y := (b : ℚ))
619 haa hbb
620 have hmulNat : (a : ℚ) * (b : ℚ) = ((a * b : ℕ) : ℚ) := by norm_num
621 rw [hmulNat, hxrep, rationalTrace_nat_eq_two_of_two_eq_two hF htwo a ha1,
622 rationalTrace_nat_eq_two_of_two_eq_two hF htwo b hb1,
623 rationalTrace_nat_eq_two_of_two_eq_two hF htwo (a * b)
624 (by exact Nat.mul_pos hapos hbpos)] at hd
625 linarith
626
627/-! ## The assembled real character -/
628
629/-- The real sign character, extended by zero at zero. -/
630def rationalSignCharacter (x : ℚ) : ℝ :=
631 if x = 0 then 0 else if 0 < x then 1 else -1
632
633theorem rationalSignCharacter_one : rationalSignCharacter 1 = 1 := by
634 simp [rationalSignCharacter]
635
636theorem rationalSignCharacter_mul (x y : ℚ) :
637 rationalSignCharacter (x * y) =
638 rationalSignCharacter x * rationalSignCharacter y := by
639 by_cases hx : x = 0
640 · subst x
641 simp [rationalSignCharacter]
642 by_cases hy : y = 0
643 · subst y
644 simp [rationalSignCharacter]
645 have hxy : x * y ≠ 0 := mul_ne_zero hx hy
646 rcases lt_or_gt_of_ne hx with hxneg | hxpos
647 · rcases lt_or_gt_of_ne hy with hyneg | hypos
648 · have hxypos : 0 < x * y := mul_pos_of_neg_of_neg hxneg hyneg
649 simp [rationalSignCharacter, hx, hy, hxy, hxneg.not_gt, hyneg.not_gt,
650 hxypos]
651 · have hxyneg : x * y < 0 := mul_neg_of_neg_of_pos hxneg hypos
652 simp [rationalSignCharacter, hx, hy, hxy, hxneg.not_gt, hypos,
653 hxyneg.not_gt]
654 · rcases lt_or_gt_of_ne hy with hyneg | hypos
655 · have hxyneg : x * y < 0 := mul_neg_of_pos_of_neg hxpos hyneg
656 simp [rationalSignCharacter, hx, hy, hxy, hxpos, hyneg.not_gt,
657 hxyneg.not_gt]
658 · have hxypos : 0 < x * y := mul_pos hxpos hypos
659 simp [rationalSignCharacter, hx, hy, hxy, hxpos, hypos, hxypos]
660
661theorem rationalSignCharacter_recip {x : ℚ} (hx : x ≠ 0) :
662 rationalSignCharacter x⁻¹ = (rationalSignCharacter x)⁻¹ := by
663 rcases lt_or_gt_of_ne hx with hxneg | hxpos
664 · have hinvneg : x⁻¹ < 0 := inv_lt_zero.mpr hxneg
665 simp [rationalSignCharacter, hx, inv_ne_zero hx, hxneg.not_gt,
666 hinvneg.not_gt]
667 · have hinvpos : 0 < x⁻¹ := inv_pos.mpr hxpos
668 simp [rationalSignCharacter, hx, inv_ne_zero hx, hxpos, hinvpos]
669
670theorem rationalSignCharacter_nonzero {x : ℚ} (hx : x ≠ 0) :
671 rationalSignCharacter x ≠ 0 := by
672 rcases lt_or_gt_of_ne hx with hxneg | hxpos
673 · simp [rationalSignCharacter, hx, hxneg.not_gt]
674 · simp [rationalSignCharacter, hx, hxpos]
675
676theorem rationalSignCharacter_of_pos {x : ℚ} (hx : 0 < x) :
677 rationalSignCharacter x = 1 := by
678 simp [rationalSignCharacter, ne_of_gt hx, hx]
679
680/-- The real character extracted from the doubled trace. The degenerate anchor
681is the sign character; otherwise the generalized linear extraction is used. -/
682noncomputable def realCharacterCandidate
683 (F : RatioOrbit → RatioOrbit) (q : RatioOrbit) : ℝ :=
684 if rationalTrace F 2 = 2 then
685 rationalSignCharacter q.toRat
686 else if q.toRat = 0 then
687 0
688 else
689 nontrivialCharacterValue F q.toRat
690
691theorem nontrivialCharacterValue_nonzero
692 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
693 (hnontrivial : rationalTrace F 2 ≠ 2)
694 {x : ℚ} (hx : x ≠ 0) :
695 nontrivialCharacterValue F x ≠ 0 := by
696 have hmul := nontrivialCharacterValue_mul hF hnontrivial hx (inv_ne_zero hx)
697 rw [mul_inv_cancel₀ hx, nontrivialCharacterValue_one hF hnontrivial] at hmul
698 intro hz
699 rw [hz, zero_mul] at hmul
700 norm_num at hmul
701
702theorem nontrivialCharacterValue_recip
703 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
704 (hnontrivial : rationalTrace F 2 ≠ 2)
705 {x : ℚ} (hx : x ≠ 0) :
706 nontrivialCharacterValue F x⁻¹ =
707 (nontrivialCharacterValue F x)⁻¹ := by
708 have hmul := nontrivialCharacterValue_mul hF hnontrivial hx (inv_ne_zero hx)
709 rw [mul_inv_cancel₀ hx, nontrivialCharacterValue_one hF hnontrivial] at hmul
710 exact eq_inv_of_mul_eq_one_right hmul.symm
711
712theorem nontrivialCharacterValue_trace
713 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
714 (hnontrivial : rationalTrace F 2 ≠ 2)
715 {x : ℚ} (hx : x ≠ 0) :
716 nontrivialCharacterValue F x +
717 (nontrivialCharacterValue F x)⁻¹ =
718 rationalTrace F x := by
719 have hsum := nontrivialCharacterValue_recip_sum hF hnontrivial hx
720 rw [nontrivialCharacterValue_recip hF hnontrivial hx] at hsum
721 linarith
722
723theorem nontrivialCharacterValue_two
724 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
725 (hnontrivial : rationalTrace F 2 ≠ 2) :
726 nontrivialCharacterValue F 2 = anchorRoot F := by
727 have htwo : (2 : ℚ) ≠ 0 := by norm_num
728 have hd := rationalTrace_dAlembert hF htwo htwo
729 have hprod : (2 : ℚ) * 2 = 4 := by norm_num
730 have hquot : (2 : ℚ) / 2 = 1 := by norm_num
731 rw [hprod, hquot, rationalTrace_one hF] at hd
732 have hfour :
733 rationalTrace F 4 = rationalTrace F 2 ^ 2 - 2 := by
734 nlinarith [hd]
735 have hr0 := anchorRoot_ne_zero hF
736 have hrden := anchorRoot_sq_sub_one_ne_zero hF hnontrivial
737 have hA : rationalTrace F 2 =
738 (anchorRoot F ^ 2 + 1) / anchorRoot F := by
739 rw [← anchorRoot_add_inv hF, eq_div_iff hr0]
740 field_simp [hr0]
741 rw [nontrivialCharacterValue, linearExtraction,
742 show (2 : ℚ) * 2 = 4 by norm_num, hfour, hA]
743 field_simp [hr0, hrden]
744 ring
745
746theorem nontrivialCharacterValue_pow
747 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
748 (hnontrivial : rationalTrace F 2 ≠ 2)
749 {x : ℚ} (hx : x ≠ 0) :
750 ∀ k : ℕ,
751 nontrivialCharacterValue F (x ^ k) =
752 nontrivialCharacterValue F x ^ k := by
753 intro k
754 induction k with
755 | zero =>
756 simpa using nontrivialCharacterValue_one hF hnontrivial
757 | succ k ih =>
758 rw [pow_succ, nontrivialCharacterValue_mul hF hnontrivial
759 (pow_ne_zero k hx) hx, ih, pow_succ]
760
761theorem nontrivialCharacterValue_pos_on_nat
762 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
763 (hnontrivial : rationalTrace F 2 ≠ 2)
764 {n : ℕ} (hn : 1 ≤ n) :
765 0 < nontrivialCharacterValue F n := by
766 have hnq : (n : ℚ) ≠ 0 := by exact_mod_cast (show n ≠ 0 by omega)
767 have hne := nontrivialCharacterValue_nonzero hF hnontrivial hnq
768 have htrace := nontrivialCharacterValue_trace hF hnontrivial hnq
769 have hge := rationalTrace_nat_ge_two hF hn
770 by_contra hpos
771 have hle : nontrivialCharacterValue F n ≤ 0 := le_of_not_gt hpos
772 have hneg : nontrivialCharacterValue F n < 0 :=
773 lt_of_le_of_ne hle hne
774 have hinvneg : (nontrivialCharacterValue F n)⁻¹ < 0 :=
775 inv_lt_zero.mpr hneg
776 linarith
777
778private theorem exists_pow_trace_decrease
779 {u r : ℝ} (hu : 0 < u) (hu1 : u < 1) (hr : 1 < r) :
780 ∃ k : ℕ,
781 r * u ^ k + (r * u ^ k)⁻¹ < u ^ k + (u ^ k)⁻¹ := by
782 have hu2pos : 0 < u ^ 2 := sq_pos_of_pos hu
783 have hu2lt : u ^ 2 < 1 := by nlinarith
784 have hrpos : 0 < r := lt_trans zero_lt_one hr
785 have heps : 0 < r⁻¹ := inv_pos.mpr hrpos
786 obtain ⟨k, hk⟩ := exists_pow_lt_of_lt_one heps hu2lt
787 refine ⟨k, ?_⟩
788 let v := u ^ k
789 have hv : 0 < v := pow_pos hu k
790 have hsmall : v ^ 2 < r⁻¹ := by
791 have hid : v ^ 2 = (u ^ 2) ^ k := by
792 simp only [v, ← pow_mul]
793 rw [Nat.mul_comm]
794 rw [hid]
795 exact hk
796 have hrvlt : r * v ^ 2 < 1 := by
797 have hm := mul_lt_mul_of_pos_left hsmall hrpos
798 rw [mul_inv_cancel₀ (ne_of_gt hrpos)] at hm
799 exact hm
800 have hid :
801 (r * v) * (r * v + (r * v)⁻¹ - (v + v⁻¹)) =
802 (r - 1) * (r * v ^ 2 - 1) := by
803 field_simp [ne_of_gt hrpos, ne_of_gt hv]
804 ring
805 have hneg :
806 (r - 1) * (r * v ^ 2 - 1) < 0 :=
807 mul_neg_of_pos_of_neg (by linarith) (by linarith)
808 have hdiff :
809 r * v + (r * v)⁻¹ - (v + v⁻¹) < 0 := by
810 have hrvpos : 0 < r * v := mul_pos hrpos hv
811 have hscaled :
812 (r * v) * (r * v + (r * v)⁻¹ - (v + v⁻¹)) < 0 := by
813 rw [hid]
814 exact hneg
815 nlinarith
816 change r * v + (r * v)⁻¹ < v + v⁻¹
817 linarith
818
819theorem nontrivialCharacterValue_nat_trace_mono
820 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
821 (hnontrivial : rationalTrace F 2 ≠ 2)
822 {m n : ℕ} (hm : 1 ≤ m) (hmn : m ≤ n) :
823 nontrivialCharacterValue F m +
824 (nontrivialCharacterValue F m)⁻¹ ≤
825 nontrivialCharacterValue F n +
826 (nontrivialCharacterValue F n)⁻¹ := by
827 have hmq : (m : ℚ) ≠ 0 := by exact_mod_cast (show m ≠ 0 by omega)
828 have hnq : (n : ℚ) ≠ 0 := by
829 exact_mod_cast (show n ≠ 0 by omega)
830 have hmtrace := nontrivialCharacterValue_trace hF hnontrivial hmq
831 have hntrace := nontrivialCharacterValue_trace hF hnontrivial hnq
832 have hmono := rationalTrace_nat_mono hF hm hmn
833 rw [← hmtrace, ← hntrace] at hmono
834 exact hmono
835
836theorem nontrivialCharacterValue_principal_on_nat
837 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
838 (hnontrivial : rationalTrace F 2 ≠ 2) :
839 ∀ n : ℕ, 1 ≤ n → 1 ≤ nontrivialCharacterValue F n := by
840 intro n hn
841 let u := nontrivialCharacterValue F n
842 let r := anchorRoot F
843 have hu : 0 < u := nontrivialCharacterValue_pos_on_nat hF hnontrivial hn
844 have hr : 1 < r := anchorRoot_gt_one hF hnontrivial
845 by_contra hprincipal
846 have hu1 : u < 1 := lt_of_not_ge hprincipal
847 obtain ⟨k, hdecrease⟩ := exists_pow_trace_decrease hu hu1 hr
848 have hnpowPos : 0 < n ^ k := pow_pos (by omega) k
849 have hnpowOne : 1 ≤ n ^ k := hnpowPos
850 have hnatMono :=
851 nontrivialCharacterValue_nat_trace_mono hF hnontrivial
852 hnpowOne (by omega : n ^ k ≤ 2 * n ^ k)
853 have hnq : (n : ℚ) ≠ 0 := by exact_mod_cast (show n ≠ 0 by omega)
854 have hpowq : (n : ℚ) ^ k ≠ 0 := pow_ne_zero k hnq
855 have hcharPow := nontrivialCharacterValue_pow hF hnontrivial hnq k
856 have hcharTwoPow :=
857 nontrivialCharacterValue_mul hF hnontrivial
858 (by norm_num : (2 : ℚ) ≠ 0) hpowq
859 have hcastPow : (((n ^ k : ℕ) : ℚ)) = (n : ℚ) ^ k := by norm_num
860 have hcastTwoPow :
861 (((2 * n ^ k : ℕ) : ℚ)) = (2 : ℚ) * (n : ℚ) ^ k := by norm_num
862 rw [hcastPow, hcastTwoPow, hcharPow, hcharTwoPow,
863 nontrivialCharacterValue_two hF hnontrivial, hcharPow] at hnatMono
864 change u ^ k + (u ^ k)⁻¹ ≤
865 r * u ^ k + (r * u ^ k)⁻¹ at hnatMono
866 exact (not_lt_of_ge hnatMono) hdecrease
867
868theorem realCharacterCandidate_unit
869 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F) :
870 realCharacterCandidate F RatioOrbit.one = 1 := by
871 by_cases ht : rationalTrace F 2 = 2
872 · simp [realCharacterCandidate, ht, RatioOrbit.one_toRat,
873 rationalSignCharacter_one]
874 · simp [realCharacterCandidate, ht, RatioOrbit.one_toRat,
875 nontrivialCharacterValue_one hF ht]
876
877theorem realCharacterCandidate_mul
878 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
879 {x y : RatioOrbit} (hx : x.toRat ≠ 0) (hy : y.toRat ≠ 0) :
880 realCharacterCandidate F (RatioOrbit.mul x y) =
881 realCharacterCandidate F x * realCharacterCandidate F y := by
882 have hxy : x.toRat * y.toRat ≠ 0 := mul_ne_zero hx hy
883 by_cases ht : rationalTrace F 2 = 2
884 · simp [realCharacterCandidate, ht, RatioOrbit.mul_toRat,
885 rationalSignCharacter_mul]
886 · simp only [realCharacterCandidate, ht, if_false,
887 RatioOrbit.mul_toRat, hx, hy, hxy]
888 exact nontrivialCharacterValue_mul hF ht hx hy
889
890theorem realCharacterCandidate_recip
891 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
892 {x : RatioOrbit} (hx : x.toRat ≠ 0) :
893 realCharacterCandidate F (RatioOrbit.recip x) =
894 (realCharacterCandidate F x)⁻¹ := by
895 have hinv : x.toRat⁻¹ ≠ 0 := inv_ne_zero hx
896 by_cases ht : rationalTrace F 2 = 2
897 · simp [realCharacterCandidate, ht, RatioOrbit.recip_toRat,
898 rationalSignCharacter_recip hx]
899 · simp only [realCharacterCandidate, ht, if_false,
900 RatioOrbit.recip_toRat, hx, hinv]
901 exact nontrivialCharacterValue_recip hF ht hx
902
903theorem realCharacterCandidate_nonzero
904 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
905 {x : RatioOrbit} (hx : x.toRat ≠ 0) :
906 realCharacterCandidate F x ≠ 0 := by
907 by_cases ht : rationalTrace F 2 = 2
908 · simp only [realCharacterCandidate, ht, if_true]
909 exact rationalSignCharacter_nonzero hx
910 · simp only [realCharacterCandidate, ht, if_false, hx]
911 exact nontrivialCharacterValue_nonzero hF ht hx
912
913theorem realCharacterCandidate_principal_on_pos_int
914 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F) :
915 ∀ n : ℕ, 1 ≤ n → 1 ≤ realCharacterCandidate F (natOrbit n) := by
916 intro n hn
917 have hnpos : (0 : ℚ) < n := by exact_mod_cast (show 0 < n by omega)
918 have hnne : (n : ℚ) ≠ 0 := ne_of_gt hnpos
919 by_cases ht : rationalTrace F 2 = 2
920 · rw [realCharacterCandidate, if_pos ht, natOrbit_toRat,
921 rationalSignCharacter_of_pos hnpos]
922 · rw [realCharacterCandidate, if_neg ht, natOrbit_toRat, if_neg hnne]
923 exact nontrivialCharacterValue_principal_on_nat hF ht n hn
924
925theorem realCharacterCandidate_is_character
926 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F) :
927 PRCRealRatioCharacter (realCharacterCandidate F) where
928 unit := realCharacterCandidate_unit hF
929 multiplicative := fun _ _ hx hy => realCharacterCandidate_mul hF hx hy
930 reciprocal := fun _ hx => realCharacterCandidate_recip hF hx
931 nonzero := fun _ hx => realCharacterCandidate_nonzero hF hx
932 principal_on_pos_int := realCharacterCandidate_principal_on_pos_int hF
933
934theorem realCharacterCandidate_trace_of_pos
935 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
936 {q : RatioOrbit} (hq : 0 < q.toRat) :
937 realCharacterCandidate F q + (realCharacterCandidate F q)⁻¹ =
938 traceDisplay F q := by
939 have hqne : q.toRat ≠ 0 := ne_of_gt hq
940 have hdisplay := rationalTrace_eq_traceDisplay hF q
941 by_cases ht : rationalTrace F 2 = 2
942 · have htrivial := rationalTrace_pos_eq_two_of_two_eq_two hF ht hq
943 rw [htrivial] at hdisplay
944 rw [realCharacterCandidate, if_pos ht,
945 rationalSignCharacter_of_pos hq, ← hdisplay]
946 norm_num
947 · have htrace := nontrivialCharacterValue_trace hF ht hqne
948 rw [realCharacterCandidate, if_neg ht, if_neg hqne, htrace, hdisplay]
949
950theorem realCharacterCandidate_cost_agrees
951 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
952 (q : RatioOrbit) (hq : 0 < q.toRat) :
953 ((F q).toRat : ℝ) =
954 costFromRealCharacter (realCharacterCandidate F) q := by
955 rw [costFromRealCharacter, realCharacterCandidate_trace_of_pos hF hq]
956 simp only [traceDisplay, nativeCostDoubledTrace, doubledTraceValue,
957 RatioOrbit.mul_toRat, RatioOrbit.add_toRat, two_toRat,
958 RatioOrbit.one_toRat]
959 push_cast
960 ring
961
962theorem realCharacterCandidate_small_traces_rational
963 {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F) :
964 ∀ n : ℕ, 2 ≤ n → n ≤ 5 →
965 ∃ t : ℚ,
966 realCharacterCandidate F (natOrbit n) +
967 (realCharacterCandidate F (natOrbit n))⁻¹ =
968 (t : ℝ) := by
969 intro n hn _
970 refine ⟨(nativeCostDoubledTrace F (natOrbit n)).toRat, ?_⟩
971 exact realCharacterCandidate_trace_of_pos hF
972 (by rw [natOrbit_toRat]; exact_mod_cast (show 0 < n by omega))
973
974/-- The anchor-free doubled trace always factors through a real-valued
975principal character. -/
976theorem SansAnchorRealCharacterFactorizationTarget_proved :
977 SansAnchorRealCharacterFactorizationTarget := by
978 intro F hF
979 exact ⟨realCharacterCandidate F, realCharacterCandidate_is_character hF,
980 realCharacterCandidate_cost_agrees hF,
981 realCharacterCandidate_small_traces_rational hF⟩
982
983#print axioms doubledTrace_dAlembert_of_rcl
984#print axioms doubledTrace_dAlembert_of_sansAnchor
985#print axioms SansAnchorRealCharacterFactorizationTarget_proved
986
987end RealCharacterFactorization
988end Cost
989end IndisputableMonolith
990