-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathRH.lean
More file actions
7885 lines (6935 loc) · 357 KB
/
Copy pathRH.lean
File metadata and controls
7885 lines (6935 loc) · 357 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
/-
A Geometric Proof of the Riemann Hypothesis
==========================
A Lean 4 / Mathlib formalization of the multiplicative framework:
unit-circle observation μ, source B, medium C, metallic ratios,
coherence ↔ sech, and the forced σ = 1/2.
Formal Reduction = ACHIEVED
Unconditional Closure = Pending
Build: lake env lean Framework.lean
Project: lakefile.lean depending on `mathlib`
Honest accounting at top:
* The geometric framework, canonical factorization, coherence identities,
prime-wise decomposition, finite-window refinement identities, and the
endpoint packaging theorem all have explicit proofs and no `sorry`.
* The RH closure is conditional on explicitly named analytic boundary
axioms (xi/log-derivative identities, convergence tails, and
Hurwitz-style window-zero transfer).
* The final RH-style step is isolated as a 2-D defect-to-rigidity
interface (`phase_lock_rigidity_from_2D_defect_boundary`), with theorem-level
routing through `phase_lock_defect_argument_2D`/`phase_lock_rigidity`.
The rest of the file is an explicit formal reduction to that interface plus
the stated analytic continuation/convergence axioms.
* The theorem `rh_endpoint_master` is the single packaged endpoint for
this file.
-/
import Mathlib.Analysis.SpecialFunctions.Complex.Log
import Mathlib.Analysis.SpecialFunctions.Complex.Arg
import Mathlib.Analysis.SpecialFunctions.Gamma.Basic
import Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.Complex.Norm
import Mathlib.Analysis.Complex.Trigonometric
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Real.Sqrt
import Mathlib.NumberTheory.LSeries.RiemannZeta
import Mathlib.NumberTheory.LSeries.HurwitzZetaValues
import Mathlib.NumberTheory.LSeries.Dirichlet
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
-- import Mathlib.Analysis.SpecialFunctions.Hyperbolic
import Mathlib.Tactic
import Mathlib.Analysis.Calculus.Deriv.Add
import Mathlib.Analysis.Calculus.Deriv.Mul
import Mathlib.Analysis.Calculus.Deriv.Comp
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
import Mathlib.Analysis.Calculus.LogDeriv
open Real Complex RingHom HurwitzZeta
open scoped ComplexOrder ComplexConjugate
open Classical
namespace Real
/-- Compatibility alias for older snippets: logarithm base `b`. -/
noncomputable def logb (b x : ℝ) : ℝ := Real.log x / Real.log b
/-- Compatibility helper: strict hyperbolic inequality away from `0`. -/
theorem one_lt_cosh {x : ℝ} (hx : x ≠ 0) : 1 < Real.cosh x :=
_root_.Real.one_lt_cosh.mpr hx
end Real
theorem one_div_lt_one {x : ℝ} (hx : 1 < x) : 1 / x < 1 := by
have hx0 : 0 < x := by linarith [zero_lt_one, hx]
rw [div_lt_iff₀ hx0, one_mul]
exact hx
/-! ### Complex modulus: Mathlib exposes `‖z‖`; keep `Complex.abs` as an alias for older snippets. -/
namespace Complex
noncomputable abbrev abs (z : ℂ) : ℝ := ‖z‖
@[simp]
theorem abs_def (z : ℂ) : abs z = Real.sqrt (normSq z) :=
norm_def z
@[simp]
theorem abs_mul (z w : ℂ) : abs (z * w) = abs z * abs w := by
simpa [abs] using norm_mul z w
@[simp]
theorem abs_exp (z : ℂ) : abs (exp z) = Real.exp z.re := by
simpa [abs] using (norm_exp z)
/-!
### Geometry in the Gaussian plane (ℝ²)
* **Reflection in the real axis** is exactly complex conjugation: `conj ⟨x, y⟩ = ⟨x, -y⟩`.
* **Rotation by \(π / 2\)** counterclockwise about `0` is multiplication by `I`.
* **Conjugation** is exactly that real-axis reflection; **multiplication by `I`** is the π/2 rotation,
so all point symmetries of the plane are repeatedly “reflection ∘ rotation ∘ …” bookkeeping.
The standard intertwining law is `conj (I * z) = -I * conj z`: reflect-then-rotate and
rotate-then-reflect differ by that sign (the same obstruction to complex-linearity: conjugation is
anti-linear for the complex vector space structure).
### “Solving for `conj`” (algebra)
`conj` denotes `starRingEnd ℂ`, a commutative `RingHom`. So peeling conjugation uses the same lemmas
as for any ring map (see **`Complex.Conj`** below): **`map_mul`**, **`map_add`**, **`map_sub`**, negatives,
powers, naturals/integers/rationals, and Mathlib’s **`conj_ofReal`**, **`conj_I`** (plus inversion via
Mathlib **`conj_inv`**).
For products involving **`I`**, compose with **`conj_mul_I`** and shuffle with **`mul_comm`** / **`ring`**.
**Tactics (defined after `Complex`):** `simp_conj`, `simp_conj!`, `simp_conj_plus`, `ring_conj`, `field_conj`,
`simp_log`, `simp_arg`, `push_div`, `simp_polar`, `grind_cplx`,
`cplx_ext`, `cplx_re_im`, `simp_abs`.
Baseline `simp_only` burst (for copy-paste / customization):
`simp only [map_mul, map_add, map_sub, map_neg, map_pow, map_one, map_zero, conj_ofReal, conj_I,
conj_natCast, conj_ofNat, div_eq_mul_inv, conj_inv]`.
-/
/-- Multiplying by `I` is the linear “90° CCW” map `(x, y) ↦ (-y, x)` on `(re, im)`. -/
lemma I_mul_rotate (z : ℂ) : (I * z).re = -z.im ∧ (I * z).im = z.re := by
simp [mul_re, mul_im, I_re, I_im]
/-- Conjugation is reflection in the real axis: imaginary part negated. -/
lemma conj_eq_reflect_real_axis (z : ℂ) : conj z = ⟨z.re, -z.im⟩ := by
refine Complex.ext ?_ ?_ <;> simp
/-- Conjugation sends `I` to `-I`, so `conj` anticommutes with rotation by `I`. -/
lemma conj_mul_I (z : ℂ) : conj (I * z) = -I * conj z := by
refine Complex.ext ?_ ?_
· simp [Complex.mul_re, Complex.mul_im, Complex.I_re, Complex.I_im]
· simp [Complex.mul_re, Complex.mul_im, Complex.I_re, Complex.I_im]
/-- Reflection in the **imaginary** axis is `z ↦ -conj z` (negate `re`, keep `im`). -/
lemma neg_conj_eq_reflect_imaginary_axis (z : ℂ) : -conj z = ⟨-z.re, z.im⟩ := by
refine Complex.ext ?_ ?_ <;> simp
/-! ### Structural lemmas for peeling `conj` (`starRingEnd ℂ`) -/
namespace Conj
variable {z w : ℂ}
theorem map_mul : conj (z * w) = conj z * conj w := RingHom.map_mul (starRingEnd ℂ) z w
theorem map_add : conj (z + w) = conj z + conj w := RingHom.map_add (starRingEnd ℂ) z w
theorem map_sub : conj (z - w) = conj z - conj w := RingHom.map_sub (starRingEnd ℂ) z w
theorem map_neg : conj (-z) = -conj z := RingHom.map_neg (starRingEnd ℂ) z
theorem map_one : conj (1 : ℂ) = 1 := RingHom.map_one (starRingEnd ℂ)
theorem map_zero : conj (0 : ℂ) = 0 := RingHom.map_zero (starRingEnd ℂ)
theorem map_pow (n : ℕ) : conj (z ^ n) = conj z ^ n := RingHom.map_pow (starRingEnd ℂ) z n
/-- Conjugation commutes with division (write `z / w` as `z * w⁻¹` and use `conj_inv`). -/
theorem map_div : conj (z / w) = conj z / conj w := by
simp_rw [div_eq_mul_inv, RingHom.map_mul (starRingEnd ℂ), conj_inv]
end Conj
end Complex
/-!
### Tactic macros (this file)
`conj` scope: `scoped[ComplexConjugate]` (opened above).
* `simp_conj` — peel `conj` via `starRingEnd` / `Complex.Conj`-style lemmas.
* `simp_conj!` — also `conj_mul_I` plus common `mul`/sign shuffles (`I`).
* `simp_conj_plus` — bounded nested `conj` cleanup.
* `ring_conj` — `simp_conj_plus` then `ring_nf`.
* `field_conj` — `field_simp`, then bounded `conj` peel / `ring_nf`.
* **`simp_log`** — `Complex.log` via `log_re` / `log_im` (+ `log 0`, `log 1`).
* **`simp_arg`** — common `Complex.arg` special values (`0`, `1`, `±1`, `±I`, naturals).
* **`push_div`** — `z / w` as `z * w⁻¹` (`div_eq_mul_inv`) for algebraic follow-up.
* **`simp_polar`** — polar identity `‖z‖ * exp(arg z · I) = z`.
* **`grind_cplx`** — cheap pipeline: norms/polar → Cartesian → divisions → logs/args → `conj` → `ring_nf` → `field_simp`.
* `cplx_ext` — split `ℂ` equality with `Complex.ext` then `simp`.
* `cplx_re_im` — expand `re`/`im` of `+`, `*`, reals, `I` (small cartesian bursts).
* `simp_abs` — rewrite `Complex.abs` to `‖·‖`/`norm`/sqrt form for `simp` closures.
-/
/-- Core `conj` peel (minimal; safe on most algebraic goals). -/
macro "simp_conj" : tactic =>
`(tactic|
simp only [map_mul, map_add, map_sub, map_neg, map_pow, map_one, map_zero,
conj_I, conj_ofReal, conj_natCast, conj_ofNat, div_eq_mul_inv, conj_inv])
/-- Like `simp_conj`, but also rotates `conj` across `I` and normalizes commutative products a bit. -/
macro "simp_conj!" : tactic =>
`(tactic|
simp only [map_mul, map_add, map_sub, map_neg, map_pow, map_one, map_zero,
conj_I, conj_ofReal, conj_natCast, conj_ofNat, div_eq_mul_inv, conj_inv,
conj_mul_I, mul_assoc, mul_comm, mul_left_comm, neg_mul, mul_neg])
/-- Nested `conj` bookkeeping: bounded iteration of `simp_conj`. -/
macro "simp_conj_plus" : tactic =>
`(tactic| simp_conj)
macro "ring_conj" : tactic =>
`(tactic| repeat' (first | simp_conj_plus | ring_nf))
macro "cplx_ext" : tactic =>
`(tactic| refine Complex.ext ?_ ?_ <;> simp)
macro "cplx_re_im" : tactic =>
`(tactic|
simp only [Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im, Complex.neg_re,
Complex.neg_im, Complex.sub_re, Complex.sub_im,
Complex.ofReal_re, Complex.ofReal_im, Complex.I_re, Complex.I_im,
mul_assoc, mul_comm, mul_left_comm])
macro "simp_abs" : tactic =>
`(tactic| simp only [Complex.abs_def, Complex.norm_def])
/-- `Complex.log` in terms of `‖·‖`, `arg`, and `Real.log` (often for `re`/`im` pushes). -/
macro "simp_log" : tactic =>
`(tactic|
simp only [Complex.log_re, Complex.log_im, Complex.log_zero, Complex.log_one])
/-- Select `Complex.arg` values (nonnegative reals cast to `ℂ`, `±1`, `±I`, etc.). -/
macro "simp_arg" : tactic =>
`(tactic|
simp only [Complex.arg_zero, Complex.arg_one, Complex.arg_neg_one, Complex.arg_I,
Complex.arg_neg_I, Complex.arg_div_self, Complex.natCast_arg, Complex.ofNat_arg])
/-- Prefer multiplicative form `z * w⁻¹` (then use `ring_nf` / `field_simp` as needed). -/
macro "push_div" : tactic =>
`(tactic| try simp_rw [div_eq_mul_inv])
/-- Polar glue: `‖z‖ * exp (arg z · I) = z` (Mathlib `Complex.norm_mul_exp_arg_mul_I`). -/
macro "simp_polar" : tactic =>
`(tactic| try simp only [Complex.norm_mul_exp_arg_mul_I])
/-- One-pass “complex grind”: light `simp` bursts and normal forms (all steps are `try`). -/
macro "grind_cplx" : tactic =>
`(tactic|
repeat' (first
| simp_abs
| simp_polar
| cplx_re_im
| push_div
| simp_log
| simp_arg
| simp_conj_plus
| ring_nf
| field_simp))
/-- `field_simp` then bounded `conj` peel / `ring_nf` (use when denominators muddy the goal). -/
macro "field_conj" : tactic =>
`(tactic| repeat' (first | field_simp | simp_conj_plus | ring_nf))
namespace FourAxioms
/-! ## The four axioms, as Lean definitions
We package the four-axiom premise as a structure. Any concrete (μ, B, C)
satisfying it gives rise to all the consequences below. -/
/-- The observation μ together with the assumption that it lies in Q2 on
the unit circle.
**Trivial “ζ” zeros vs this geometry:** the classical points `s = -2,-4,-6,…`
come from the **Γ-factor / completion** (pole-zero bookkeeping in the archimedean
Euler product), not from the **open Q2** locus `re_neg ∧ im_pos` used here. They
lie on the **negative real axis** and **never enter Q2**.
**Octagon / D8 crossing:** the unit-circle crossing locus at angles `π/4` and
`5π/4` (Q1 and Q3 on `S¹`) is packaged later via `Phase8` and `sourceOctagon`.
That locus is **disjoint** from the negative real axis where the trivial
completion points live. -/
structure Observation where
μ : ℂ
re_neg : μ.re < 0
im_pos : 0 < μ.im
unit_mod : Complex.abs μ = 1
/-- The factorization of the observation `μ` as `μ = B·C` with
`arg μ = arg B + arg C`.
**Source–medium–sink (same pattern as Ohm's law):** read `B` as the
source-like factor, `C` as the medium-like factor, and the product `B·C`
as the closed observable (sink-side accounting). The concrete circuit
identity `V = I·R` is the same multiplicative shape: injection × path/load
response yields what you measure across the channel. -/
structure Factorization (O : Observation) where
B : ℂ
C : ℂ
product : B * C = O.μ
arg_add : Complex.arg B + Complex.arg C = Complex.arg O.μ
-- non-degeneracy: B and C nonzero, so arg is well-defined
B_ne : B ≠ 0
C_ne : C ≠ 0
/-! ## §1. μ on the symmetric diagonal of Q2
The framework's coupling assumption (Re ⊥ Im, no preferred axis between them)
is captured here as: μ lies on the symmetric diagonal x = -y in Q2.
This is the natural fixed point of the Re↔Im symmetry; it isn't derived
from the bare axioms 1–2 (those alone leave the whole Q2 arc), but follows
once we add the symmetric-diagonal premise the notes record as
"Re ⊥ Im + coupling". We make that premise explicit as a hypothesis. -/
/-- The canonical observation μ = -1/√2 + i/√2. -/
noncomputable def μ_canonical : ℂ :=
⟨-(1 / Real.sqrt 2), 1 / Real.sqrt 2⟩
@[simp] lemma mu_canonical_re : μ_canonical.re = -(1 / Real.sqrt 2 : ℝ) := rfl
@[simp] lemma mu_canonical_im : μ_canonical.im = (1 / Real.sqrt 2 : ℝ) := rfl
/-- Unit-circle split for the canonical seed in component form. -/
lemma mu_canonical_re_sq_add_im_sq : μ_canonical.re ^ 2 + μ_canonical.im ^ 2 = 1 := by
have hsq : (Real.sqrt 2 : ℝ) ^ 2 = 2 := by
nlinarith [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
calc
μ_canonical.re ^ 2 + μ_canonical.im ^ 2
= (-(1 / Real.sqrt 2 : ℝ)) ^ 2 + (1 / Real.sqrt 2 : ℝ) ^ 2 := by
simp [mu_canonical_re, mu_canonical_im]
_ = (1 / 2 : ℝ) + (1 / 2 : ℝ) := by
field_simp [hsq]
_ = 1 := by norm_num
/-- Uniqueness of the canonical seed from geometry:
unit circle + Q2 sign conditions + diagonal symmetry (`Re = -Im`) force `μ = μ_canonical`. -/
theorem mu_forced_eq_mu_canonical_of_unit_q2_diagonal (μ : ℂ)
(hunit : μ.re ^ 2 + μ.im ^ 2 = 1)
(hre : μ.re < 0) (him : 0 < μ.im)
(hdiag : μ.re = -μ.im) :
μ = μ_canonical := by
have hre_sq : μ.re ^ 2 = μ.im ^ 2 := by nlinarith [hdiag]
have him_sq : μ.im ^ 2 = (1 / 2 : ℝ) := by nlinarith [hunit, hre_sq]
have hsqrt2 : (Real.sqrt 2) ^ 2 = (2 : ℝ) := by
nlinarith [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
have hhalf : (1 / Real.sqrt 2 : ℝ) ^ 2 = (1 / 2 : ℝ) := by
field_simp [hsqrt2]
have him_sq' : μ.im ^ 2 = (1 / Real.sqrt 2 : ℝ) ^ 2 := by
linarith [him_sq, hhalf]
rcases sq_eq_sq_iff_eq_or_eq_neg.mp him_sq' with him_pos | him_neg
· have hre' : μ.re = -(1 / Real.sqrt 2 : ℝ) := by
nlinarith [hdiag, him_pos]
apply Complex.ext <;> simp [μ_canonical, hre', him_pos]
· exfalso
have hpos : (0 : ℝ) < 1 / Real.sqrt 2 := by positivity
have him_lt : μ.im < 0 := by nlinarith [him_neg, hpos]
exact (not_lt_of_gt him) him_lt
lemma sqrt_two_div_two_eq_inv_sqrt_two : Real.sqrt 2 / 2 = 1 / Real.sqrt 2 := by
have hsp : (0 : ℝ) < Real.sqrt 2 := Real.sqrt_pos.mpr (show (0 : ℝ) < 2 by norm_num)
field_simp [hsp.ne']
lemma three_mul_pi_div_four_mem_Ioc_pi :
(3 * Real.pi / 4 : ℝ) ∈ Set.Ioc (-Real.pi) Real.pi := by
refine ⟨?_ , ?_⟩
· nlinarith [Real.pi_pos]
· linarith [Real.pi_pos]
lemma mu_canonical_eq_cos_sin_three_pi_div_four :
μ_canonical = Real.cos (3 * Real.pi / 4) + Real.sin (3 * Real.pi / 4) * Complex.I := by
have hcos :
Real.cos (3 * Real.pi / 4) = -(Real.sqrt 2 / 2) := calc
Real.cos (3 * Real.pi / 4) = Real.cos (Real.pi - Real.pi / 4) := by ring_nf
_ = -Real.cos (Real.pi / 4) := Real.cos_pi_sub _
_ = -(Real.sqrt 2 / 2) := by rw [Real.cos_pi_div_four]
have hsin :
Real.sin (3 * Real.pi / 4) = Real.sqrt 2 / 2 := calc
Real.sin (3 * Real.pi / 4) = Real.sin (Real.pi - Real.pi / 4) := by ring_nf
_ = Real.sin (Real.pi / 4) := Real.sin_pi_sub _
_ = Real.sqrt 2 / 2 := Real.sin_pi_div_four
refine Complex.ext ?_ ?_
· -- real part
simp [Complex.add_re, Complex.mul_re, hcos, sqrt_two_div_two_eq_inv_sqrt_two, μ_canonical_re]
ring
· -- imaginary part
simp [Complex.add_im, Complex.mul_im, hsin, sqrt_two_div_two_eq_inv_sqrt_two, μ_canonical_im]
ring
theorem μ_canonical_abs : Complex.abs μ_canonical = 1 := by
rw [Complex.abs_def]
simp only [Complex.normSq_apply, μ_canonical_re, μ_canonical_im]
rw [mu_canonical_re_sq_add_im_sq, Real.sqrt_one]
theorem μ_canonical_arg : Complex.arg μ_canonical = 3 * Real.pi / 4 := by
rw [← mu_canonical_eq_cos_sin_three_pi_div_four]
exact Complex.arg_cos_add_sin_mul_I three_mul_pi_div_four_mem_Ioc_pi
/-- Equal-energy split at the canonical angle (`arg μ = 3π/4`):
each squared component contributes `1/2`. -/
lemma mu_canonical_re_sq_eq_half : μ_canonical.re ^ 2 = (1 / 2 : ℝ) := by
have hsq : (Real.sqrt 2 : ℝ) ^ 2 = 2 := by
nlinarith [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
calc
μ_canonical.re ^ 2 = (-(1 / Real.sqrt 2 : ℝ)) ^ 2 := by simp [mu_canonical_re]
_ = (1 / 2 : ℝ) := by field_simp [hsq]
lemma mu_canonical_im_sq_eq_half : μ_canonical.im ^ 2 = (1 / 2 : ℝ) := by
have hsq : (Real.sqrt 2 : ℝ) ^ 2 = 2 := by
nlinarith [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
calc
μ_canonical.im ^ 2 = (1 / Real.sqrt 2 : ℝ) ^ 2 := by simp [mu_canonical_im]
_ = (1 / 2 : ℝ) := by field_simp [hsq]
/-! ## §2. B = 1+i and C = i/√2 are the canonical solution
These are forced once we add the "minimal integer-aligned source" criterion.
We write them as `def`s and prove they satisfy `Factorization`. -/
noncomputable def B_canonical : ℂ := ⟨1, 1⟩ -- 1 + i
noncomputable def C_canonical : ℂ := ⟨0, 1 / Real.sqrt 2⟩ -- i/√2
theorem B_abs : Complex.abs B_canonical = Real.sqrt 2 := by
unfold B_canonical
rw [Complex.abs_def]
simp [Complex.normSq]
norm_num
/-- Magnitude of the Gaussian dilation `(1+i)^k = B_canonical^k`: `|B|^k = (√2)^k`. -/
theorem B_canonical_pow_abs (k : ℕ) :
Complex.abs (B_canonical ^ k) = (Real.sqrt 2 : ℝ) ^ k := by
calc
Complex.abs (B_canonical ^ k) = Complex.abs B_canonical ^ k := by
simpa [Complex.abs] using (norm_pow B_canonical k)
_ = (Real.sqrt 2) ^ k := congrArg (fun x : ℝ => x ^ k) B_abs
/-- Notebook name for `B_canonical^k` as the `k`-fold `(1+i)` scaling step on `ℤ[i]` (embedded in `ℂ`).
**Discrete RG / octagon picture:** each multiplication by `1 + i` scales lengths by `√2`
(`B_abs` / `gaussian_scale_factor_abs`) and rotates by `π/4` (45°), so eight steps close an
octagon orbit (`B_canonical_pow_eight`, `gaussianScaleFactor_phase_cycle`). This is the usual
“renormalisation group” step on the Gaussian lattice: same generator at every scale.
**Area vs inverse-square:** in the plane, Euclidean “inverse-square” intensity is tied to area
scaling with radius — here each step doubles cell area since `|B|² = 2`; see `gaussianScaleFactor_area`. -/
noncomputable def gaussianScaleFactor (k : ℕ) : ℂ := B_canonical ^ k
@[simp]
theorem gaussianScaleFactor_eq (k : ℕ) : gaussianScaleFactor k = B_canonical ^ k := rfl
theorem gaussian_scale_factor_abs (k : ℕ) :
Complex.abs (gaussianScaleFactor k) = (Real.sqrt 2 : ℝ) ^ k := by
simpa [gaussianScaleFactor_eq] using B_canonical_pow_abs k
/-- Induction base for Gaussian scaling: at `k=0`, the scale factor is `1`. -/
@[simp] theorem gaussianScaleFactor_zero : gaussianScaleFactor 0 = (1 : ℂ) := by
simp [gaussianScaleFactor]
/-- Induction step for Gaussian scaling:
`(1+i)^(k+1) = (1+i) * (1+i)^k` in packaged `gaussianScaleFactor` form. -/
theorem gaussianScaleFactor_succ (k : ℕ) :
gaussianScaleFactor (k + 1) = B_canonical * gaussianScaleFactor k := by
simp [gaussianScaleFactor, pow_succ, mul_comm, mul_left_comm, mul_assoc]
/-- Bundled induction form for Gaussian scaling. -/
theorem gaussianScaleFactor_induction_form (k : ℕ) :
gaussianScaleFactor 0 = (1 : ℂ) ∧
gaussianScaleFactor (k + 1) = B_canonical * gaussianScaleFactor k := by
exact ⟨gaussianScaleFactor_zero, gaussianScaleFactor_succ k⟩
/-- Cell-area scaling law for the `k`-fold Gaussian dilation:
`|B^k|^2 = 2^k` for `B = 1 + i`.
Same doubling as one would expect from scaling lengths by `√2` in 2D (area ∝ length²); this is the
lattice analogue of inverse-square / spherical area scaling, restricted to the `(1+i)^k ℤ[i]` tower. -/
theorem gaussianScaleFactor_area (k : ℕ) :
(Complex.abs (gaussianScaleFactor k)) ^ 2 = (2 : ℝ) ^ k := by
rw [gaussian_scale_factor_abs]
calc
((Real.sqrt 2 : ℝ) ^ k) ^ 2 = (Real.sqrt 2 : ℝ) ^ (k * 2) := by
symm
rw [pow_mul]
_ = (Real.sqrt 2 : ℝ) ^ (2 * k) := by rw [Nat.mul_comm]
_ = ((Real.sqrt 2 : ℝ) ^ 2) ^ k := by rw [pow_mul]
have hsq : (Real.sqrt 2 : ℝ) ^ 2 = 2 := by
nlinarith [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
simpa [hsq]
/-- Base algebra for the phase channel: `(1+i)^2 = 2i`. -/
theorem B_canonical_sq : B_canonical ^ 2 = (2 : ℂ) * Complex.I := by
unfold B_canonical
norm_num [pow_two, Complex.ext_iff, Complex.mul_re, Complex.mul_im]
/-- Octagon-cycle closure: after 8 Gaussian steps, phase returns to the real axis. -/
theorem B_canonical_pow_eight : B_canonical ^ 8 = (16 : ℂ) := by
unfold B_canonical
norm_num [pow_succ, pow_two, Complex.ext_iff, Complex.mul_re, Complex.mul_im, Complex.I_sq]
/-- Phase-periodic scaling law: stepping by 8 multiplies only by the real factor `16`. -/
theorem gaussianScaleFactor_phase_cycle (k : ℕ) :
gaussianScaleFactor (k + 8) = (16 : ℂ) * gaussianScaleFactor k := by
unfold gaussianScaleFactor
calc
B_canonical ^ (k + 8) = B_canonical ^ 8 * B_canonical ^ k := by
simpa [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc] using (pow_add B_canonical 8 k)
_ = (16 : ℂ) * B_canonical ^ k := by rw [B_canonical_pow_eight]
_ = (16 : ℂ) * gaussianScaleFactor k := by rfl
/-- Branch-safe phase periodicity: adding 8 scale steps preserves `arg`. -/
theorem gaussianScaleFactor_arg_periodic_8 (k : ℕ) :
Complex.arg (gaussianScaleFactor (k + 8)) = Complex.arg (gaussianScaleFactor k) := by
rw [gaussianScaleFactor_phase_cycle]
have h16 : (0 : ℝ) < 16 := by norm_num
calc
Complex.arg ((16 : ℂ) * gaussianScaleFactor k)
= Complex.arg (((16 : ℝ) : ℂ) * gaussianScaleFactor k) := by norm_num
_ = Complex.arg (gaussianScaleFactor k) := by
simpa [mul_comm] using (Complex.arg_mul_real h16 (gaussianScaleFactor k))
/-- Exponential phase multiplication law from `exp` additivity. -/
lemma exp_mul_I_add (θ φ : ℝ) :
Complex.exp ((θ + φ) * Complex.I)
= Complex.exp (θ * Complex.I) * Complex.exp (φ * Complex.I) := by
calc
Complex.exp ((θ + φ) * Complex.I)
= Complex.exp (θ * Complex.I + φ * Complex.I) := by ring
_ = Complex.exp (θ * Complex.I) * Complex.exp (φ * Complex.I) := by
simpa using Complex.exp_add (θ * Complex.I) (φ * Complex.I)
/-- Polar form for the Gaussian generator: `1+i = √2 · exp(iπ/4)`. -/
theorem B_canonical_eq_sqrt2_mul_exp_pi_div_four :
B_canonical = ((Real.sqrt 2 : ℝ) : ℂ) * Complex.exp ((Real.pi / 4) * Complex.I) := by
conv_rhs => rw [← Complex.exp_ofReal_mul_I]
unfold B_canonical
refine Complex.ext ?_ ?_
· simp [Complex.mul_re, Complex.mul_im, Complex.add_re]
rw [Real.cos_pi_div_four, Real.sin_pi_div_four]
have hsq : (Real.sqrt (2 : ℝ)) ^ 2 = 2 := Real.sq_sqrt (show (0 : ℝ) ≤ 2 by positivity)
field_simp; ring_nf; rw [hsq]; ring
· simp [Complex.mul_re, Complex.mul_im, Complex.add_im]
rw [Real.cos_pi_div_four, Real.sin_pi_div_four]
have hsq : (Real.sqrt (2 : ℝ)) ^ 2 = 2 := Real.sq_sqrt (show (0 : ℝ) ≤ 2 by positivity)
field_simp; ring_nf; rw [hsq]; ring
lemma pi_div_four_mem_Ioc_pi : Real.pi / 4 ∈ Set.Ioc (-Real.pi) Real.pi := by
refine ⟨?_, ?_⟩
· nlinarith [Real.pi_pos, Real.pi_div_four_pos]
· nlinarith [Real.pi_pos]
theorem B_canonical_arg : Complex.arg B_canonical = Real.pi / 4 := by
have hsqrt2 : 0 < Real.sqrt (2 : ℝ) := Real.sqrt_pos.2 (show (0 : ℝ) < 2 by norm_num)
rw [B_canonical_eq_sqrt2_mul_exp_pi_div_four, Complex.exp_ofReal_mul_I]
simpa [Complex.ofReal_cos, Complex.ofReal_sin] using
Complex.arg_mul_cos_add_sin_mul_I (r := Real.sqrt (2 : ℝ))
(θ := Real.pi / 4) hsqrt2 pi_div_four_mem_Ioc_pi
/-- One-step reference angle: the Gaussian generator has argument `π/4`. -/
theorem gaussianScaleFactor_arg_one :
Complex.arg (gaussianScaleFactor 1) = Real.pi / 4 := by
rwa [gaussianScaleFactor_eq, pow_one]
/-- **Linear phase model:** `(1+i)^k = (√2)^k · exp(i k π/4)` (De Moivre on the Gaussian step). -/
theorem gaussianScaleFactor_linear_phase (k : ℕ) :
gaussianScaleFactor k
= ((Real.sqrt 2 : ℝ) ^ k : ℂ) * Complex.exp (((k : ℝ) * (Real.pi / 4)) * Complex.I) := by
induction k with
| zero =>
simp [gaussianScaleFactor_zero, pow_zero, Complex.exp_zero]
| succ k ih =>
calc
gaussianScaleFactor (Nat.succ k)
= B_canonical * gaussianScaleFactor k := gaussianScaleFactor_succ _
_ = ((((Real.sqrt 2 : ℝ) : ℂ)) * Complex.exp ((Real.pi / 4) * Complex.I))
* (((Real.sqrt 2 : ℝ) ^ k : ℂ)
* Complex.exp (((k : ℝ) * (Real.pi / 4)) * Complex.I)) := by
rw [B_canonical_eq_sqrt2_mul_exp_pi_div_four, ih]
_ = ((((Real.sqrt 2 : ℝ) : ℂ)) * (((Real.sqrt 2 : ℝ) ^ k : ℂ))) *
(Complex.exp ((Real.pi / 4) * Complex.I)
* Complex.exp (((k : ℝ) * (Real.pi / 4)) * Complex.I)) := by
simp [mul_assoc, mul_left_comm, mul_comm]
_ = (((Real.sqrt (2 : ℝ)) ^ (k + 1) : ℂ))
* Complex.exp ((((↑k + 1 : ℕ) : ℝ) * (Real.pi / 4)) * Complex.I) := by
simp [pow_succ, Complex.ofReal_mul, Complex.ofReal_pow, mul_assoc, mul_comm,
mul_left_comm]
congr 2
rw [← exp_mul_I_add ((Real.pi / 4)) ((k : ℝ) * (Real.pi / 4))]
congr 1 <;> ring_nf <;> push_cast <;> ring
/-- Consolidated geometric channels for Gaussian scaling at index `k`. -/
theorem gaussianScaleFactor_phase_magnitude_area (k : ℕ) :
Complex.abs (gaussianScaleFactor k) = (Real.sqrt 2 : ℝ) ^ k ∧
(Complex.abs (gaussianScaleFactor k)) ^ 2 = (2 : ℝ) ^ k ∧
gaussianScaleFactor k
= ((Real.sqrt 2 : ℝ) ^ k : ℂ) * Complex.exp (((k : ℝ) * (Real.pi / 4)) * Complex.I) := by
exact ⟨gaussian_scale_factor_abs k, gaussianScaleFactor_area k, gaussianScaleFactor_linear_phase k⟩
/-- Silver-ratio identity at the canonical source:
`Re(B) + |B| = 1 + √2` for `B = 1 + i`. -/
theorem silver_ratio_eq_re_B_add_abs_B :
B_canonical.re + Complex.abs B_canonical = 1 + Real.sqrt 2 := by
simpa [B_canonical] using congrArg (fun t : ℝ => (1 : ℝ) + t) B_abs
theorem C_abs : Complex.abs C_canonical = 1 / Real.sqrt 2 := by
unfold C_canonical
rw [Complex.abs_def]
simp [Complex.normSq]
/-- The unit-modulus balance |B|·|C| = 1. This is the r ↔ 1/r symmetry
in raw form, forced by axiom 2 + axiom 3. -/
theorem magnitude_balance :
Complex.abs B_canonical * Complex.abs C_canonical = 1 := by
rw [B_abs, C_abs]
have h2 : Real.sqrt 2 ≠ 0 := by positivity
field_simp
/-- Radius-channel reading of the medium: `|C| = 1 / |B|`.
This is the precise scalar sense in which the medium is reciprocal radius. -/
theorem medium_modulus_is_reciprocal_radius :
Complex.abs C_canonical = 1 / Complex.abs B_canonical := by
rw [B_abs, C_abs]
/-- The product B · C equals the canonical μ. -/
theorem B_mul_C_eq_μ : B_canonical * C_canonical = μ_canonical := by
unfold B_canonical C_canonical μ_canonical
refine Complex.ext ?_ ?_
· -- real parts: 1·0 - 1·(1/√2) = -1/√2 ✓
simp [Complex.mul_re]
· -- imag parts: 1·(1/√2) + 1·0 = 1/√2 ✓
simp [Complex.mul_im]
/-! ## §3. Complex log bridges Cartesian and polar
For any nonzero z, log z = log |z| + i·arg(z). This is `Complex.log_eq_…`
in Mathlib; we state the consequence we need: log distributes over our product. -/
/-- log(B·C) = log B + log C for our nonzero canonical values. -/
theorem log_distrib :
Complex.log (B_canonical * C_canonical) =
Complex.log B_canonical + Complex.log C_canonical := by
apply Complex.log_mul
· -- B ≠ 0
intro h
unfold B_canonical at h
have := congrArg Complex.re h
simp at this
· -- C ≠ 0
intro h
unfold C_canonical at h
have := congrArg Complex.im h
simp at this
/-- Real-part cancellation in log B + log C corresponds to |B|·|C| = 1. -/
theorem log_real_parts_cancel :
(Complex.log B_canonical).re + (Complex.log C_canonical).re = 0 := by
rw [Complex.log_re, Complex.log_re, B_abs, C_abs]
have hs0 : (Real.sqrt 2) ≠ 0 := by positivity
rw [one_div, Real.log_inv, Real.log_sqrt (by positivity : (0 : ℝ) ≤ 2)]
· ring
· exact hs0
/-! ## §4. Phase closure φ - θ = 0 is automatic
Define φ = arg(A) and θ = arg(B) + arg(C). The factorization axiom gives
arg_add directly: φ - θ = arg(A) - (arg(B) + arg(C)) = 0. -/
theorem phase_closure (O : Observation) (F : Factorization O) :
Complex.arg O.μ - (Complex.arg F.B + Complex.arg F.C) = 0 := by
rw [F.arg_add]; ring
/-! ## §4b. Cartesian channel decomposition for `A = B * C`
These identities keep the same factorization story in explicit Re/Im form.
They are the coordinate-channel counterpart of the phase relation above. -/
/-- Real-part channel of the factorization `A = B * C`. -/
lemma factorization_re_channel (O : Observation) (F : Factorization O) :
O.μ.re = F.B.re * F.C.re - F.B.im * F.C.im := by
simpa [Complex.mul_re] using (congrArg Complex.re F.product).symm
/-- Imaginary-part channel of the factorization `A = B * C`. -/
lemma factorization_im_channel (O : Observation) (F : Factorization O) :
O.μ.im = F.B.re * F.C.im + F.B.im * F.C.re := by
simpa [Complex.mul_im] using (congrArg Complex.im F.product).symm
/-- Bundled Re/Im channel decomposition for the observation `A`. -/
lemma factorization_reim_bundle (O : Observation) (F : Factorization O) :
O.μ.re = F.B.re * F.C.re - F.B.im * F.C.im
∧
O.μ.im = F.B.re * F.C.im + F.B.im * F.C.re := by
exact ⟨factorization_re_channel O F, factorization_im_channel O F⟩
/-! ## §4d. Unit-modulus consequences (`|μ| = 1`)
For any factorization `A = B * C` of an observation with `|A| = 1`,
the source/medium radii are multiplicative reciprocals. -/
/-- From `|μ|=1` and `μ=B*C`, the product modulus is exactly one. -/
lemma factorization_abs_product_eq_one (O : Observation) (F : Factorization O) :
Complex.abs (F.B * F.C) = 1 := by
simpa [F.product] using O.unit_mod
/-- Norm-channel product balance for a general factorization with `|μ|=1`. -/
lemma factorization_norm_balance (O : Observation) (F : Factorization O) :
‖F.B‖ * ‖F.C‖ = 1 := by
have hprod : ‖F.B * F.C‖ = 1 := by
simpa using factorization_abs_product_eq_one O F
simpa [norm_mul] using hprod
/-- Radius reciprocity for the medium channel in any unit-modulus factorization. -/
lemma factorization_medium_norm_is_reciprocal_source (O : Observation) (F : Factorization O) :
‖F.C‖ = 1 / ‖F.B‖ := by
have hbal := factorization_norm_balance O F
have hB : ‖F.B‖ ≠ 0 := by
exact norm_ne_zero_iff.mpr F.B_ne
apply (eq_div_iff hB).2
simpa [mul_comm] using hbal
/-- Abstract unit-modulus bridge for any factorization:
the observation has modulus one, the factor radii multiply to one, and the
medium radius is the reciprocal of the source radius. -/
theorem factorization_unit_modulus_bridge (O : Observation) (F : Factorization O) :
Complex.abs O.μ = 1 ∧ ‖F.B‖ * ‖F.C‖ = 1 ∧ ‖F.C‖ = 1 / ‖F.B‖ := by
exact ⟨O.unit_mod, factorization_norm_balance O F,
factorization_medium_norm_is_reciprocal_source O F⟩
/-! ## §4c. Explicit `x + iy` substitution
This is the fully coordinate-level form of complex multiplication, plus the
specialization to any factorization `A = B * C` in this file. -/
/-- Expanded coordinate formula for `(x + iy) * (u + iv)`. -/
lemma mul_xyuv_expand (x y u v : ℝ) :
(((x : ℂ) + y * Complex.I) * ((u : ℂ) + v * Complex.I))
= ((x * u - y * v : ℝ) : ℂ) + (x * v + y * u) * Complex.I := by
refine Complex.ext ?_ ?_
· simp [Complex.mul_re, Complex.mul_im, Complex.I_re, Complex.I_im]
ring
· simp [Complex.mul_re, Complex.mul_im, Complex.I_re, Complex.I_im]
ring
/-- Real channel for `(x + iy) * (u + iv)`. -/
lemma mul_xyuv_re (x y u v : ℝ) :
((((x : ℂ) + y * Complex.I) * ((u : ℂ) + v * Complex.I)).re)
= x * u - y * v := by
simpa [mul_xyuv_expand x y u v]
/-- Imaginary channel for `(x + iy) * (u + iv)`. -/
lemma mul_xyuv_im (x y u v : ℝ) :
((((x : ℂ) + y * Complex.I) * ((u : ℂ) + v * Complex.I)).im)
= x * v + y * u := by
simpa [mul_xyuv_expand x y u v]
/-- Substituting `B = x+iy`, `C = u+iv` into `A = B*C`: real channel. -/
lemma factorization_re_channel_xy (O : Observation) (F : Factorization O)
(x y u v : ℝ)
(hB : F.B = (x : ℂ) + y * Complex.I)
(hC : F.C = (u : ℂ) + v * Complex.I) :
O.μ.re = x * u - y * v := by
rw [factorization_re_channel O F, hB, hC]
simp
/-- Substituting `B = x+iy`, `C = u+iv` into `A = B*C`: imaginary channel. -/
lemma factorization_im_channel_xy (O : Observation) (F : Factorization O)
(x y u v : ℝ)
(hB : F.B = (x : ℂ) + y * Complex.I)
(hC : F.C = (u : ℂ) + v * Complex.I) :
O.μ.im = x * v + y * u := by
rw [factorization_im_channel O F, hB, hC]
simp [mul_comm, mul_left_comm, mul_assoc, add_comm, add_left_comm, add_assoc]
/-- Bundled coordinate substitution for `A = B*C` with `B = x+iy`, `C = u+iv`. -/
lemma factorization_reim_bundle_xy (O : Observation) (F : Factorization O)
(x y u v : ℝ)
(hB : F.B = (x : ℂ) + y * Complex.I)
(hC : F.C = (u : ℂ) + v * Complex.I) :
O.μ.re = x * u - y * v ∧ O.μ.im = x * v + y * u := by
exact ⟨factorization_re_channel_xy O F x y u v hB hC,
factorization_im_channel_xy O F x y u v hB hC⟩
/-! ## §5. Metallic ratios fall out
For B = n + i with n ≥ 0, the quantity Re(B) + |B| = n + √(n²+1)
is the n-th metallic mean. Silver = (n=1), Golden = (n=1/2). -/
/-- The n-th metallic mean as a real number. -/
noncomputable def metallic (n : ℝ) : ℝ := n + Real.sqrt (n^2 + 1)
/-- Parameterized source family for metallic geometry: `B_n = n + i`. -/
noncomputable def B_metallic (n : ℝ) : ℂ :=
(n : ℂ) + Complex.I
/-- The modulus of `B_n = n + i` is `√(n²+1)`. -/
theorem B_metallic_abs (n : ℝ) :
Complex.abs (B_metallic n) = Real.sqrt (n ^ 2 + 1) := by
unfold B_metallic
rw [Complex.abs_def]
congr_arg Real.sqrt
simp [Complex.normSq_apply, Complex.add_re, Complex.add_im, Complex.ofReal_re, Complex.ofReal_im,
Complex.I_re, Complex.I_im]
ring
/-- General metallic identity:
`metallic n = Re(B_n) + |B_n|` for `B_n = n + i`. -/
theorem metallic_eq_re_B_metallic_add_abs_B_metallic (n : ℝ) :
metallic n = (B_metallic n).re + Complex.abs (B_metallic n) := by
unfold metallic B_metallic
simp [B_metallic_abs]
/-- Equivalent orientation of the same identity (often convenient for rewriting). -/
theorem re_B_metallic_add_abs_B_metallic_eq_metallic (n : ℝ) :
(B_metallic n).re + Complex.abs (B_metallic n) = metallic n := by
simpa using (metallic_eq_re_B_metallic_add_abs_B_metallic n).symm
/-- Silver ratio: metallic 1 = 1 + √2. -/
theorem silver_eq : metallic 1 = 1 + Real.sqrt 2 := by
unfold metallic
congr 1
congr 1
ring
/-- Golden ratio: metallic (1/2) = (1 + √5)/2. -/
theorem golden_eq : metallic (1/2) = (1 + Real.sqrt 5) / 2 := by
unfold metallic
-- 1/2 + √(1/4 + 1) = 1/2 + √(5/4) = 1/2 + √5/2 = (1+√5)/2
have h : ((1:ℝ)/2)^2 + 1 = 5 / 4 := by ring
rw [h]
have h2 : Real.sqrt (5/4) = Real.sqrt 5 / 2 := by
calc
Real.sqrt (5 / 4) = Real.sqrt 5 / Real.sqrt 4 := by
rw [Real.sqrt_div (by positivity : (0:ℝ) ≤ 5)]
_ = Real.sqrt 5 / 2 := by norm_num
rw [h2]; ring
/-- The defining identity of the golden ratio: φ² = φ + 1. -/
theorem golden_self_referential :
let φ := (1 + Real.sqrt 5) / 2
φ^2 = φ + 1 := by
simp only
have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
field_simp
ring_nf
rw [show Real.sqrt 5 ^ 2 = 5 from h5]
ring
/-! ## §6. Coherence in log coordinates
C(r) = 2r/(1+r)^2 on (0, ∞). Writing r = e^μ,
this becomes C(r) = (1/2) * sech^2(μ/2). -/
noncomputable def coherence (r : ℝ) : ℝ := 2 * r / (1 + r)^2
theorem coherence_eq_sech_log (r : ℝ) (hr : 0 < r) :
coherence r = (1 / 2) * (1 / (Real.cosh (Real.log r / 2))^2) := by
unfold coherence
have hr0 : r ≠ 0 := ne_of_gt hr
have hcosh : Real.cosh (Real.log r / 2) = (Real.sqrt r + 1 / Real.sqrt r) / 2 := by
have hsp : 0 < Real.sqrt r := Real.sqrt_pos.2 hr
have hel : Real.exp (Real.log r / 2) = Real.sqrt r := by
rw [← Real.sqrt_eq_rpow hr.le, Real.rpow_def_of_pos hr]
ring_nf
have hel' : Real.exp (-(Real.log r / 2)) = 1 / Real.sqrt r := by
rw [Real.exp_neg, hel]
field_simp [hsp.ne']
rw [← mul_right_inj' (two_ne_zero : (2 : ℝ) ≠ 0)]
calc
(2 : ℝ) * Real.cosh (Real.log r / 2)
= (Complex.exp (((Real.log r / 2) : ℝ) : ℂ) +
Complex.exp (-(((Real.log r / 2) : ℝ) : ℂ))).re := by
simp [Real.cosh, Complex.two_cosh, Complex.add_re]
_ = Real.sqrt r + 1 / Real.sqrt r := by
simp [Complex.exp_ofReal, hel, hel', Complex.add_re, Complex.ofReal_re]
_ = (2 : ℝ) * ((Real.sqrt r + 1 / Real.sqrt r) / 2) := by ring
rw [hcosh]
have hsqrt : (Real.sqrt r)^2 = r := by rw [sq, Real.sq_sqrt (le_of_lt hr)]
field_simp [Real.sqrt_ne_zero'.2 hr, hr0, hsqrt]
ring
/-- `h`-form of coherence: `coherence (h^2) = (1/2) * sech(log h)^2` for `h > 0`. -/
theorem coherence_eq_half_sech_sq_log_h (h : ℝ) (hh : 0 < h) :
coherence (h^2) = (1 / 2) * (1 / (Real.cosh (Real.log h))^2) := by
have hsq_pos : 0 < h^2 := by positivity
rw [coherence_eq_sech_log (h^2) hsq_pos]
rw [Real.log_rpow hh.le]
norm_num
/-- Normalized coherence channel in the `h`-parameterization. -/
noncomputable def coherenceC (h : ℝ) : ℝ :=
Real.sqrt (2 * coherence (h^2))
/-- Magic transformation map: `h = e^μ` (real-parameter channel). -/
noncomputable def h_of_mu (μ : ℝ) : ℝ := Real.exp μ
/-- `h_of_mu` is always positive. -/
lemma h_of_mu_pos (μ : ℝ) : 0 < h_of_mu μ := by
unfold h_of_mu
exact Real.exp_pos μ
/-- Exact normalized identity: `C(h) = sech(log h)` for `h > 0`. -/
theorem coherenceC_eq_sech_log_h (h : ℝ) (hh : 0 < h) :
coherenceC h = 1 / Real.cosh (Real.log h) := by
unfold coherenceC
rw [coherence_eq_half_sech_sq_log_h h hh]
have hcalc :
2 * ((1 / 2) * (1 / (Real.cosh (Real.log h))^2))
= (1 / Real.cosh (Real.log h))^2 := by
ring
rw [hcalc, Real.sqrt_sq_eq_abs]
exact abs_of_nonneg (by positivity)
/-- Coherence channel through the magic map `h = e^μ`:
`C(e^μ) = sech(μ)`. -/
theorem coherenceC_eq_sech_of_h_eq_exp_mu (μ : ℝ) :
coherenceC (h_of_mu μ) = 1 / Real.cosh μ := by
have hpos : 0 < h_of_mu μ := h_of_mu_pos μ
calc
coherenceC (h_of_mu μ) = 1 / Real.cosh (Real.log (h_of_mu μ)) :=
coherenceC_eq_sech_log_h (h_of_mu μ) hpos
_ = 1 / Real.cosh μ := by
unfold h_of_mu
simp [Real.log_exp]
/-- `h = e^μ` is off-equilibrium exactly when `μ ≠ 0`. -/
theorem h_of_mu_off_equilibrium_iff_mu_ne_zero (μ : ℝ) :
h_of_mu μ ≠ 1 ↔ μ ≠ 0 := by
unfold h_of_mu
constructor
· intro h μ0
apply h
simp [μ0]
· intro hμ h1
apply hμ
have : Real.exp μ = Real.exp 0 := by simpa using h1
exact (Real.exp_injective this)
/-- Magic-map version of the normalized defect/coherence bundle:
in `μ`-coordinates, off-equilibrium is exactly `μ ≠ 0`. -/
theorem RH_defect_off_equilibrium_bundle_of_mu (μ : ℝ) :
((0 < RH_defectC (h_of_mu μ)) ↔ (μ ≠ 0))
∧ ((μ ≠ 0) ↔ (coherenceC (h_of_mu μ) < 1)) := by
have hbase : ((0 < RH_defectC (h_of_mu μ)) ↔ (h_of_mu μ ≠ 1))
∧ ((h_of_mu μ ≠ 1) ↔ (coherenceC (h_of_mu μ) < 1)) := by
exact RH_defect_off_equilibrium_bundle (h_of_mu μ) (h_of_mu_pos μ)
rcases hbase with ⟨hdef, hcoh⟩
constructor
· constructor
· intro hpos
exact (h_of_mu_off_equilibrium_iff_mu_ne_zero μ).1 (hdef.1 hpos)
· intro hμ
exact hdef.2 ((h_of_mu_off_equilibrium_iff_mu_ne_zero μ).2 hμ)
· constructor
· intro hμ
exact hcoh.1 ((h_of_mu_off_equilibrium_iff_mu_ne_zero μ).2 hμ)
· intro hlt
exact (h_of_mu_off_equilibrium_iff_mu_ne_zero μ).1 (hcoh.2 hlt)
/-- The r ↔ 1/r symmetry of coherence (= even-ness of sech). -/
theorem coherence_symmetric (r : ℝ) (hr : 0 < r) :
coherence r = coherence (1 / r) := by
unfold coherence
have hr' : r ≠ 0 := ne_of_gt hr
field_simp
ring
/-- Applying coherence to the medium modulus matches applying coherence to the source radius,
because coherence is symmetric under `r ↔ 1/r`. -/
theorem coherence_at_medium_modulus_eq_source :
coherence (Complex.abs C_canonical) = coherence (Complex.abs B_canonical) := by
have hBpos : 0 < Complex.abs B_canonical := by
rw [B_abs]
positivity
calc
coherence (Complex.abs C_canonical)
= coherence (1 / Complex.abs B_canonical) := by rw [medium_modulus_is_reciprocal_radius]
_ = coherence (Complex.abs B_canonical) := by
simpa using (coherence_symmetric (Complex.abs B_canonical) hBpos).symm
/-- Peak of coherence at r = 1. -/
theorem coherence_peak : coherence 1 = 1/2 := by
unfold coherence; norm_num
/-- Coherence is strictly below one on the positive radius channel. -/
theorem coherence_lt_one (r : ℝ) (hr : 0 < r) :
coherence r < 1 := by
unfold coherence
have hden : 0 < (1 + r) ^ 2 := by positivity
have hnum : 2 * r < (1 + r) ^ 2 := by
nlinarith [sq_nonneg r]
exact (div_lt_one hden).2 hnum
/-- RH defect channel in radius coordinates: `1 - C(r)`. -/
noncomputable def RH_defect (r : ℝ) : ℝ :=
1 - coherence r
/-- The RH defect profile is exactly the coherence residual `1 - C(r)`.
Here `C(r)` is `coherence r`. -/
theorem RH_defect_eq_coherence_residual (r : ℝ) :
RH_defect r = 1 - coherence r := by
rfl
/-- Positivity of the defect is equivalent to strict sub-unity coherence. -/
theorem RH_defect_pos_iff_coherence_lt_one (r : ℝ) :
0 < RH_defect r ↔ coherence r < 1 := by
simpa [RH_defect] using (sub_pos : 0 < 1 - coherence r ↔ coherence r < 1)
/-- Off-equilibrium in the normalized channel is exactly `C(h) < 1`.
This packages: off-critical (radius form) ↔ off-equilibrium ↔ `C < 1`. -/
theorem off_equilibrium_iff_coherenceC_lt_one (h : ℝ) (hh : 0 < h) :
h ≠ 1 ↔ coherenceC h < 1 := by
constructor
· intro hne
rw [coherenceC_eq_sech_log_h h hh]
have hlog_ne : Real.log h ≠ 0 := by