SmithDyadic.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import Mathlib.Analysis.SpecificLimits.Normed
7 import Mathlib.Algebra.Order.Floor.Div
8 import Mathlib.Data.Fintype.BigOperators
9 import Mathlib.Data.List.OfFn
10 import Mathlib.Algebra.Polynomial.Basic
11 import Mathlib.Algebra.Polynomial.Coeff
12 import Mathlib.Data.Finset.NatAntidiagonal
13 import Mathlib.Data.Fintype.Card
14 import Mathlib.Data.Matrix.Basic
15 import Mathlib.LinearAlgebra.Matrix.Adjugate
16 import Mathlib.RingTheory.PowerSeries.Basic
17 import Mathlib.RingTheory.PowerSeries.Inverse
18 import Mathlib.Analysis.Normed.Ring.Basic
19 import Mathlib.Tactic.NoncommRing
20 import Mathlib.Algebra.BigOperators.Intervals
21 import Mathlib.Algebra.Module.Submodule.LinearMap
22 import Mathlib.Algebra.Polynomial.Eval.Defs
23 import Mathlib.Analysis.Normed.Operator.Basic
24 import Mathlib.Tactic.Abel
25 import Mathlib.Util.AssertNoSorry
26 import Mathlib.Analysis.Complex.Exponential
27 import Mathlib.LinearAlgebra.Matrix.Notation
28 import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
29 import Mathlib.Data.Nat.ChineseRemainder
30 import Mathlib.GroupTheory.SpecificGroups.Cyclic
31 import Mathlib.NumberTheory.Padics.PadicVal.Basic
32 import Mathlib.RingTheory.Polynomial.Resultant.Basic
33 import Mathlib.Tactic.NormNum
34 import Mathlib.Tactic.Ring
35 import Mathlib.Tactic.FinCases
36 import Mathlib.Tactic.FieldSimp
37 import Mathlib.Tactic.Push
38 import Mathlib.Tactic.ByContra
39 import Mathlib.Tactic.SplitIfs
40 import Mathlib.Tactic.FunProp
41 
42 /-!
43 # Paper II: Smith fibres and the exceptional dyadic sign split
44 
45 Author: Komorebi P.
46 
47 The first half proves the concrete one-coordinate congruence calculation over `ZMod (p ^ L)`:
48 `p ^ s * x = b` is solvable exactly when `p ^ min s L` divides the canonical representative of
49 `b`, and every solvable fibre has cardinality `p ^ min s L`.  These results construct the explicit
50 Smith certificates used by the finite product theorem.  The certificate API is also split into
51 independently reusable solvability and cardinality components.
52 
53 The second half checks the rational two-by-two sign involution and its two projectors entry by
54 entry.  Their exact global and genuinely `p`-local denominator weights are one at `2`; the
55 resultant of the two sign factors is computed as `2`, whose natural `padicValNat` is one at `2`
56 and zero at every distinct prime.  Finally, the Smith phase parameter `-1` is shown to act by
57 inversion.
58 -/
59 
60 set_option autoImplicit false
61 
62 namespace Komorebi.PaperII.SmithDyadic
63 
64 open scoped BigOperators Matrix
65 
66 universe u v
67 
68 /-! ## Independent finite coordinate fibres -/
69 
70 /-- The global solution fibre of independent coordinate fibres. -/
71 abbrev GlobalFiber {ι : Type u} (fiber : ι → Type v) : Type (max u v) :=
72   ∀ i, fiber i
73 
74 /-! ## Concrete one-coordinate Smith arithmetic over `ZMod (p ^ L)` -/
75 
76 /-- Multiplication by `p ^ weight`, regarded as an additive endomorphism of the finite quotient
77 `ZMod (p ^ depth)`. -/
78 def smithZModMulHom (p weight depth : ℕ) :
79     ZMod (p ^ depth) →+ ZMod (p ^ depth) :=
80   nsmulAddMonoidHom (p ^ weight)
81 
82 /-- The actual solution fibre of the one-coordinate Smith congruence
83 `p ^ weight * x = target` modulo `p ^ depth`. -/
84 abbrev SmithZModFiber (p weight depth : ℕ) (target : ZMod (p ^ depth)) :=
85   ↥(smithZModMulHom p weight depth ⁻¹' {target})
86 
87 /-- The concrete fibre is finite, inherited from the finite quotient `ZMod (p ^ depth)`. -/
88 noncomputable instance smithZModFiberFintype (p weight depth : ℕ) [NeZero (p ^ depth)]
89     (target : ZMod (p ^ depth)) : Fintype (SmithZModFiber p weight depth target) :=
90   Fintype.ofFinite _
91 
92 /-- Concrete divisibility admissibility for a one-coordinate Smith congruence. -/
93 def SmithZModAdmissible (p weight depth : ℕ) (target : ZMod (p ^ depth)) : Prop :=
94   p ^ min weight depth ∣ target.val
95 
96 /-- Concrete Smith admissibility is decidable by natural-number divisibility. -/
97 instance smithZModAdmissibleDecidable (p weight depth : ℕ) (target : ZMod (p ^ depth)) :
98     Decidable (SmithZModAdmissible p weight depth target) := by
99   unfold SmithZModAdmissible
100   infer_instance
101 
102 /-- The concrete additive endomorphism is multiplication by `p ^ weight`. -/
103 theorem smithZModMulHom_apply (p weight depth : ℕ) (x : ZMod (p ^ depth)) :
104     smithZModMulHom p weight depth x = (p ^ weight : ZMod (p ^ depth)) * x := by
105   simp [smithZModMulHom, nsmul_eq_mul]
106 
107 /-- The concrete Smith congruence is solvable exactly when the target is divisible by
108 `p ^ min weight depth`.  This is the one-coordinate arithmetic statement that was previously
109 only represented by a certificate field. -/
110 theorem smithZModFiber_nonempty_iff {p weight depth : ℕ} (hp : 1 < p)
111     (target : ZMod (p ^ depth)) :
112     Nonempty (SmithZModFiber p weight depth target) ↔
113       SmithZModAdmissible p weight depth target := by
114   let _ : NeZero (p ^ depth) := ⟨pow_ne_zero _ (Nat.ne_of_gt (lt_trans Nat.zero_lt_one hp))⟩
115   constructor
116   · rintro ⟨⟨x, hx⟩⟩
117     have hxEq : smithZModMulHom p weight depth x = target :=
118       Set.mem_singleton_iff.mp hx
119     have hx' : ((p ^ weight * x.val : ℕ) : ZMod (p ^ depth)) = target := by
120       rw [Nat.cast_mul, Nat.cast_pow]
121       rw [ZMod.natCast_zmod_val]
122       simpa [smithZModMulHom_apply] using hxEq
123     have hval := congrArg ZMod.val hx'
124     rw [ZMod.val_natCast] at hval
125     have hmodulus : p ^ min weight depth ∣ p ^ depth :=
126       Nat.pow_dvd_pow p (min_le_right weight depth)
127     have hcoefficient : p ^ min weight depth ∣ p ^ weight :=
128       Nat.pow_dvd_pow p (min_le_left weight depth)
129     unfold SmithZModAdmissible
130     rw [← hval, Nat.dvd_mod_iff hmodulus]
131     exact dvd_mul_of_dvd_left hcoefficient x.val
132   · intro hadmissible
133     rcases Nat.le_total weight depth with hwd | hdw
134     · rw [SmithZModAdmissible, Nat.min_eq_left hwd] at hadmissible
135       rcases hadmissible with ⟨k, hk⟩
136       refine ⟨⟨(k : ZMod (p ^ depth)), ?_⟩⟩
137       apply Set.mem_singleton_iff.mpr
138       rw [smithZModMulHom_apply, ← Nat.cast_pow, ← Nat.cast_mul, ← hk]
139       exact ZMod.natCast_zmod_val target
140     · rw [SmithZModAdmissible, Nat.min_eq_right hdw] at hadmissible
141       have hval_zero : target.val = 0 :=
142         Nat.eq_zero_of_dvd_of_lt hadmissible target.val_lt
143       have htarget_zero : target = 0 := (ZMod.val_eq_zero target).mp hval_zero
144       exact ⟨⟨0, by simp [htarget_zero]⟩⟩
145 
146 /-- Every inhabited concrete Smith fibre has exactly `p ^ min weight depth` elements. -/
147 theorem smithZModFiber_card_of_admissible {p weight depth : ℕ} [NeZero (p ^ depth)] (hp : 1 < p)
148     (target : ZMod (p ^ depth))
149     (hadmissible : SmithZModAdmissible p weight depth target) :
150     Fintype.card (SmithZModFiber p weight depth target) = p ^ min weight depth := by
151   obtain ⟨x, hx⟩ := (smithZModFiber_nonempty_iff hp target).mpr hadmissible
152   let f : ZMod (p ^ depth) →+ ZMod (p ^ depth) := smithZModMulHom p weight depth
153   have hxEq : f x = target := Set.mem_singleton_iff.mp hx
154   have e : SmithZModFiber p weight depth target ≃ f.ker := by
155     simpa only [SmithZModFiber, f, hxEq] using f.fiberEquivKer x
156   calc
157     Fintype.card (SmithZModFiber p weight depth target) =
158         Nat.card (SmithZModFiber p weight depth target) := Nat.card_eq_fintype_card.symm
159     _ = Nat.card f.ker := Nat.card_congr e
160     _ = (Nat.card (ZMod (p ^ depth))).gcd (p ^ weight) := by
161       simpa [f, smithZModMulHom] using
162         IsAddCyclic.card_nsmulAddMonoidHom_ker (ZMod (p ^ depth)) (p ^ weight)
163     _ = (p ^ depth).gcd (p ^ weight) := by rw [Nat.card_zmod]
164     _ = p ^ min weight depth := by
165       rcases Nat.le_total weight depth with hwd | hdw
166       · rw [Nat.min_eq_left hwd, Nat.gcd_eq_right_iff_dvd.mpr (Nat.pow_dvd_pow p hwd)]
167       · rw [Nat.min_eq_right hdw, Nat.gcd_eq_left_iff_dvd.mpr (Nat.pow_dvd_pow p hdw)]
168 
169 /-- A product fibre is inhabited exactly when every coordinate fibre is inhabited. -/
170 theorem globalFiber_nonempty_iff_coordinatewise {ι : Type u} (fiber : ι → Type v) :
171     Nonempty (GlobalFiber fiber) ↔ ∀ i, Nonempty (fiber i) := by
172   constructor
173   · rintro ⟨x⟩ i
174     exact ⟨x i⟩
175   · intro h
176     classical
177     exact ⟨fun i => Classical.choice (h i)⟩
178 
179 /-- Explicit input for one Smith coordinate at residue depth `depth`.
180 
181 The classical DVR calculation is deliberately supplied as the two fields: the coordinate fibre
182 is nonempty exactly under its admissibility predicate, and an admissible fibre has the displayed
183 cardinality.  The global theorems below do not claim to construct Smith normal form.
184 -/
185 structure SmithCoordinateCertificate (fiber : Type v) [Fintype fiber]
186     (admissible : Prop) (q weight depth : ℕ) : Prop where
187   nonempty_iff : Nonempty fiber ↔ admissible
188   card_of_admissible : admissible → Fintype.card fiber = q ^ min weight depth
189 
190 /-- The logical half of a Smith coordinate certificate, separated for APIs that only need
191 solvability and not finite cardinality. -/
192 structure SmithSolvabilityCertificate (fiber : Type v) (admissible : Prop) : Prop where
193   nonempty_iff : Nonempty fiber ↔ admissible
194 
195 /-- The counting half of a Smith coordinate certificate, separated from solvability. -/
196 structure SmithCardinalityCertificate (fiber : Type v) [Fintype fiber]
197     (admissible : Prop) (q weight depth : ℕ) : Prop where
198   card_of_admissible : admissible → Fintype.card fiber = q ^ min weight depth
199 
200 /-- Forget the counting field of a full Smith coordinate certificate. -/
201 theorem SmithCoordinateCertificate.toSolvabilityCertificate
202     {fiber : Type v} [Fintype fiber] {admissible : Prop} {q weight depth : ℕ}
203     (certificate : SmithCoordinateCertificate fiber admissible q weight depth) :
204     SmithSolvabilityCertificate fiber admissible :=
205   ⟨certificate.nonempty_iff⟩
206 
207 /-- Forget the solvability field of a full Smith coordinate certificate. -/
208 theorem SmithCoordinateCertificate.toCardinalityCertificate
209     {fiber : Type v} [Fintype fiber] {admissible : Prop} {q weight depth : ℕ}
210     (certificate : SmithCoordinateCertificate fiber admissible q weight depth) :
211     SmithCardinalityCertificate fiber admissible q weight depth :=
212   ⟨certificate.card_of_admissible⟩
213 
214 /-- Assemble the independently usable solvability and cardinality halves. -/
215 theorem SmithCoordinateCertificate.ofParts
216     {fiber : Type v} [Fintype fiber] {admissible : Prop} {q weight depth : ℕ}
217     (solvability : SmithSolvabilityCertificate fiber admissible)
218     (cardinality : SmithCardinalityCertificate fiber admissible q weight depth) :
219     SmithCoordinateCertificate fiber admissible q weight depth :=
220   ⟨solvability.nonempty_iff, cardinality.card_of_admissible⟩
221 
222 /-- A full legacy-compatible coordinate certificate derived from the concrete congruence
223 arithmetic over `ZMod (p ^ depth)`. -/
224 theorem smithZModCoordinateCertificate {p weight depth : ℕ} [NeZero (p ^ depth)] (hp : 1 < p)
225     (target : ZMod (p ^ depth)) :
226     SmithCoordinateCertificate (SmithZModFiber p weight depth target)
227       (SmithZModAdmissible p weight depth target) p weight depth :=
228   ⟨smithZModFiber_nonempty_iff hp target, smithZModFiber_card_of_admissible hp target⟩
229 
230 variable {ι : Type u}
231 variable (fiber : ι → Type v)
232 variable (admissible : ι → Prop) (q depth : ℕ) (weight : ι → ℕ)
233 
234 /-- Coordinatewise solvability from the minimal, counting-free certificate API. -/
235 theorem global_solvable_iff_coordinatewise_of_solvability
236     (certificate : ∀ i, SmithSolvabilityCertificate (fiber i) (admissible i)) :
237     Nonempty (GlobalFiber fiber) ↔ ∀ i, admissible i := by
238   rw [globalFiber_nonempty_iff_coordinatewise]
239   constructor
240   · intro h i
241     exact (certificate i).nonempty_iff.mp (h i)
242   · intro h i
243     exact (certificate i).nonempty_iff.mpr (h i)
244 
245 variable [∀ i, Fintype (fiber i)]
246 
247 /-- Smith solvability is exactly coordinatewise admissibility. -/
248 theorem global_solvable_iff_coordinatewise
249     (certificate : ∀ i, SmithCoordinateCertificate (fiber i) (admissible i)
250       q (weight i) depth) :
251     Nonempty (GlobalFiber fiber) ↔ ∀ i, admissible i := by
252   exact global_solvable_iff_coordinatewise_of_solvability fiber admissible
253     (fun i => (certificate i).toSolvabilityCertificate)
254 
255 section FiniteCount
256 
257 variable [Fintype ι] [DecidableEq ι]
258 
259 /-- Conditional product count from only the cardinality half of the local certificates. -/
260 theorem global_card_of_admissible_of_cardinality
261     (certificate : ∀ i, SmithCardinalityCertificate (fiber i) (admissible i)
262       q (weight i) depth)
263     (hAdmissible : ∀ i, admissible i) :
264     Fintype.card (GlobalFiber fiber) = q ^ ∑ i, min (weight i) depth := by
265   rw [Fintype.card_pi]
266   calc
267     (∏ i, Fintype.card (fiber i)) = ∏ i, q ^ min (weight i) depth := by
268       apply Finset.prod_congr rfl
269       intro i _
270       exact (certificate i).card_of_admissible (hAdmissible i)
271     _ = q ^ ∑ i, min (weight i) depth := by
272       simpa using Finset.prod_pow_eq_pow_sum Finset.univ
273         (fun i : ι => min (weight i) depth) q
274 
275 /-- Conditional Smith product count for an admissible finite system. -/
276 theorem global_card_of_admissible
277     (certificate : ∀ i, SmithCoordinateCertificate (fiber i) (admissible i)
278       q (weight i) depth)
279     (hAdmissible : ∀ i, admissible i) :
280     Fintype.card (GlobalFiber fiber) = q ^ ∑ i, min (weight i) depth := by
281   exact global_card_of_admissible_of_cardinality fiber admissible q depth weight
282     (fun i => (certificate i).toCardinalityCertificate) hAdmissible
283 
284 /-- One inadmissible coordinate forces the global count to vanish, using only the
285 solvability half of the local certificates. -/
286 theorem global_card_eq_zero_of_inadmissible_of_solvability
287     (certificate : ∀ i, SmithSolvabilityCertificate (fiber i) (admissible i))
288     (hBad : ∃ i, ¬ admissible i) :
289     Fintype.card (GlobalFiber fiber) = 0 := by
290   rcases hBad with ⟨i, hi⟩
291   rw [Fintype.card_pi]
292   apply Finset.prod_eq_zero (Finset.mem_univ i)
293   rw [Fintype.card_eq_zero_iff]
294   exact not_nonempty_iff.mp (fun h => hi ((certificate i).nonempty_iff.mp h))
295 
296 /-- If one coordinate is inadmissible, the global solution count is zero. -/
297 theorem global_card_eq_zero_of_inadmissible
298     (certificate : ∀ i, SmithCoordinateCertificate (fiber i) (admissible i)
299       q (weight i) depth)
300     (hBad : ∃ i, ¬ admissible i) :
301     Fintype.card (GlobalFiber fiber) = 0 := by
302   exact global_card_eq_zero_of_inadmissible_of_solvability fiber admissible
303     (fun i => (certificate i).toSolvabilityCertificate) hBad
304 
305 /-- The two count branches assembled as one conditional statement. -/
306 theorem smith_conditional_product_count
307     [Decidable (∀ i, admissible i)]
308     (certificate : ∀ i, SmithCoordinateCertificate (fiber i) (admissible i)
309       q (weight i) depth) :
310     Fintype.card (GlobalFiber fiber) =
311       if ∀ i, admissible i then q ^ ∑ i, min (weight i) depth else 0 := by
312   classical
313   split_ifs with h
314   · exact global_card_of_admissible fiber admissible q depth weight certificate h
315   · apply global_card_eq_zero_of_inadmissible fiber admissible q depth weight certificate
316     simpa only [not_forall] using h
317 
318 end FiniteCount
319 
320 /-! ## Concrete finite Smith systems -/
321 
322 section ConcreteProduct
323 
324 variable {κ : Type u}
325 
326 /-- A finite diagonal system over `ZMod (p ^ depth)` is solvable exactly when every target
327 coordinate satisfies its concrete divisibility condition. -/
328 theorem smithZMod_global_solvable_iff {p depth : ℕ} [NeZero (p ^ depth)] (hp : 1 < p)
329     (weight : κ → ℕ) (target : κ → ZMod (p ^ depth)) :
330     Nonempty (GlobalFiber (fun i => SmithZModFiber p (weight i) depth (target i))) ↔
331       ∀ i, SmithZModAdmissible p (weight i) depth (target i) := by
332   exact global_solvable_iff_coordinatewise
333     (fiber := fun i => SmithZModFiber p (weight i) depth (target i))
334     (admissible := fun i => SmithZModAdmissible p (weight i) depth (target i))
335     p depth weight (fun i => smithZModCoordinateCertificate hp (target i))
336 
337 variable [Fintype κ] [DecidableEq κ]
338 
339 /-- Exact cardinality of a finite concrete diagonal Smith system, including the zero branch
340 when at least one coordinate target is inadmissible. -/
341 theorem smithZMod_global_conditional_count {p depth : ℕ} [NeZero (p ^ depth)] (hp : 1 < p)
342     (weight : κ → ℕ) (target : κ → ZMod (p ^ depth)) :
343     Fintype.card (GlobalFiber (fun i => SmithZModFiber p (weight i) depth (target i))) =
344       if ∀ i, SmithZModAdmissible p (weight i) depth (target i)
345       then p ^ ∑ i, min (weight i) depth else 0 := by
346   classical
347   exact smith_conditional_product_count
348     (fiber := fun i => SmithZModFiber p (weight i) depth (target i))
349     (admissible := fun i => SmithZModAdmissible p (weight i) depth (target i))
350     p depth weight (fun i => smithZModCoordinateCertificate hp (target i))
351 
352 end ConcreteProduct
353 
354 /-! ## The rational sign involution and its projectors -/
355 
356 /-- Rational two-by-two matrices used in the sign-splitting example. -/
357 abbrev RatMatrix2 := Matrix (Fin 2) (Fin 2) ℚ
358 
359 /-- The integral involution `[[1,1],[0,-1]]`. -/
360 def signInvolution : RatMatrix2 :=
361   !![1, 1; 0, -1]
362 
363 /-- The positive-sign projector `(I + A) / 2`. -/
364 def positiveSignProjector : RatMatrix2 :=
365   !![1, (1 : ℚ) / 2; 0, 0]
366 
367 /-- The negative-sign projector `(I - A) / 2`. -/
368 def negativeSignProjector : RatMatrix2 :=
369   !![0, -(1 : ℚ) / 2; 0, 1]
370 
371 /-- The displayed integral matrix is an involution. -/
372 theorem signInvolution_mul_self : signInvolution * signInvolution = 1 := by
373   ext i j
374   fin_cases i <;> fin_cases j <;>
375     norm_num [signInvolution, Matrix.mul_apply, Fin.sum_univ_two, Matrix.one_apply]
376 
377 /-- Entrywise verification of `E+ = (I + A) / 2`. -/
378 theorem positiveSignProjector_formula :
379     positiveSignProjector = (2 : ℚ)⁻¹ • ((1 : RatMatrix2) + signInvolution) := by
380   ext i j
381   fin_cases i <;> fin_cases j <;>
382     norm_num [positiveSignProjector, signInvolution, Matrix.one_apply]
383 
384 /-- Entrywise verification of `E- = (I - A) / 2`. -/
385 theorem negativeSignProjector_formula :
386     negativeSignProjector = (2 : ℚ)⁻¹ • ((1 : RatMatrix2) - signInvolution) := by
387   ext i j
388   fin_cases i <;> fin_cases j <;>
389     norm_num [negativeSignProjector, signInvolution, Matrix.one_apply]
390 
391 /-- The positive-sign projector is idempotent. -/
392 theorem positiveSignProjector_idempotent :
393     positiveSignProjector * positiveSignProjector = positiveSignProjector := by
394   ext i j
395   fin_cases i <;> fin_cases j <;>
396     norm_num [positiveSignProjector, Matrix.mul_apply, Fin.sum_univ_two]
397 
398 /-- The negative-sign projector is idempotent. -/
399 theorem negativeSignProjector_idempotent :
400     negativeSignProjector * negativeSignProjector = negativeSignProjector := by
401   ext i j
402   fin_cases i <;> fin_cases j <;>
403     norm_num [negativeSignProjector, Matrix.mul_apply, Fin.sum_univ_two]
404 
405 /-- The two sign projectors are orthogonal in the displayed order. -/
406 theorem positive_mul_negative_eq_zero :
407     positiveSignProjector * negativeSignProjector = 0 := by
408   ext i j
409   fin_cases i <;> fin_cases j <;>
410     norm_num [positiveSignProjector, negativeSignProjector,
411       Matrix.mul_apply, Fin.sum_univ_two]
412 
413 /-- The two sign projectors are orthogonal in the reverse order as well. -/
414 theorem negative_mul_positive_eq_zero :
415     negativeSignProjector * positiveSignProjector = 0 := by
416   ext i j
417   fin_cases i <;> fin_cases j <;>
418     norm_num [positiveSignProjector, negativeSignProjector,
419       Matrix.mul_apply, Fin.sum_univ_two]
420 
421 /-- The two sign projectors are complete. -/
422 theorem signProjectors_complete :
423     positiveSignProjector + negativeSignProjector = 1 := by
424   ext i j
425   fin_cases i <;> fin_cases j <;>
426     norm_num [positiveSignProjector, negativeSignProjector, Matrix.one_apply]
427 
428 /-! ## Exact dyadic denominator weight -/
429 
430 /-- Entrywise integrality for a rational matrix, characterized by reduced denominator one. -/
431 def IntegralMatrix (A : RatMatrix2) : Prop :=
432   ∀ i j, (A i j).den = 1
433 
434 /-- A rational number is integral at `p` when `p` does not divide its reduced denominator. -/
435 def PIntegralRational (p : ℕ) (x : ℚ) : Prop :=
436   ¬ p ∣ x.den
437 
438 /-- Entrywise `p`-integrality for a rational two-by-two matrix.  This is the finite-coordinate
439 counterpart of preserving the standard `p`-adic lattice. -/
440 def PIntegralMatrix (p : ℕ) (A : RatMatrix2) : Prop :=
441   ∀ i j, PIntegralRational p (A i j)
442 
443 /-- Every positive-sign projector entry is integral at a prime distinct from two. -/
444 theorem positiveSignProjector_pIntegral_of_prime_ne_two {p : ℕ}
445     (hp : p.Prime) (hp2 : p ≠ 2) :
446     PIntegralMatrix p positiveSignProjector := by
447   have hp_not_dvd_two : ¬ p ∣ 2 := by
448     intro h
449     exact hp2 ((Nat.prime_dvd_prime_iff_eq hp Nat.prime_two).mp h)
450   intro i j
451   fin_cases i <;> fin_cases j <;>
452     norm_num [PIntegralRational, positiveSignProjector, hp.not_dvd_one, hp_not_dvd_two]
453 
454 /-- Every negative-sign projector entry is integral at a prime distinct from two. -/
455 theorem negativeSignProjector_pIntegral_of_prime_ne_two {p : ℕ}
456     (hp : p.Prime) (hp2 : p ≠ 2) :
457     PIntegralMatrix p negativeSignProjector := by
458   have hp_not_dvd_two : ¬ p ∣ 2 := by
459     intro h
460     exact hp2 ((Nat.prime_dvd_prime_iff_eq hp Nat.prime_two).mp h)
461   intro i j
462   fin_cases i <;> fin_cases j <;>
463     norm_num [PIntegralRational, negativeSignProjector, hp.not_dvd_one, hp_not_dvd_two]
464 
465 /-- Multiplication by two clears every denominator of the positive projector. -/
466 theorem two_smul_positiveSignProjector_integral :
467     IntegralMatrix ((2 : ℚ) • positiveSignProjector) := by
468   intro i j
469   fin_cases i <;> fin_cases j <;> norm_num [positiveSignProjector]
470 
471 /-- Multiplication by two clears every denominator of the negative projector. -/
472 theorem two_smul_negativeSignProjector_integral :
473     IntegralMatrix ((2 : ℚ) • negativeSignProjector) := by
474   intro i j
475   fin_cases i <;> fin_cases j <;> norm_num [negativeSignProjector]
476 
477 /-- The positive projector is not integral before scaling. -/
478 theorem positiveSignProjector_not_integral :
479     ¬ IntegralMatrix positiveSignProjector := by
480   intro h
481   have h01 := h (0 : Fin 2) (1 : Fin 2)
482   norm_num [positiveSignProjector] at h01
483 
484 /-- The negative projector is not integral before scaling. -/
485 theorem negativeSignProjector_not_integral :
486     ¬ IntegralMatrix negativeSignProjector := by
487   intro h
488   have h01 := h (0 : Fin 2) (1 : Fin 2)
489   norm_num [negativeSignProjector] at h01
490 
491 /-- `s` is the exact entrywise denominator weight at the natural prime `p`. -/
492 def HasExactDenominatorWeight (p : ℕ) (A : RatMatrix2) (s : ℕ) : Prop :=
493   IntegralMatrix (((p : ℚ) ^ s) • A) ∧
494     ∀ t < s, ¬ IntegralMatrix (((p : ℚ) ^ t) • A)
495 
496 /-- `s` is the exact denominator weight at `p`, measured locally: scaling by `p ^ s` makes every
497 entry `p`-integral, while every smaller power leaves at least one denominator divisible by `p`.
498 Unlike `HasExactDenominatorWeight`, this predicate does not demand integrality at other primes. -/
499 def HasExactPLocalDenominatorWeight (p : ℕ) (A : RatMatrix2) (s : ℕ) : Prop :=
500   PIntegralMatrix p (((p : ℚ) ^ s) • A) ∧
501     ∀ t < s, ¬ PIntegralMatrix p (((p : ℚ) ^ t) • A)
502 
503 /-- The positive sign projector has exact dyadic denominator weight one. -/
504 theorem positiveSignProjector_exact_dyadic_weight :
505     HasExactDenominatorWeight 2 positiveSignProjector 1 := by
506   constructor
507   · simpa using two_smul_positiveSignProjector_integral
508   · intro t ht
509     have ht0 : t = 0 := Nat.lt_one_iff.mp ht
510     subst t
511     simpa using positiveSignProjector_not_integral
512 
513 /-- The negative sign projector has exact dyadic denominator weight one. -/
514 theorem negativeSignProjector_exact_dyadic_weight :
515     HasExactDenominatorWeight 2 negativeSignProjector 1 := by
516   constructor
517   · simpa using two_smul_negativeSignProjector_integral
518   · intro t ht
519     have ht0 : t = 0 := Nat.lt_one_iff.mp ht
520     subst t
521     simpa using negativeSignProjector_not_integral
522 
523 /-- The positive sign projector has exact `2`-local denominator weight one. -/
524 theorem positiveSignProjector_exact_dyadic_pLocal_weight :
525     HasExactPLocalDenominatorWeight 2 positiveSignProjector 1 := by
526   constructor
527   · intro i j
528     fin_cases i <;> fin_cases j <;>
529       norm_num [PIntegralMatrix, PIntegralRational, positiveSignProjector]
530   · intro t ht
531     have ht0 : t = 0 := Nat.lt_one_iff.mp ht
532     subst t
533     intro h
534     have h01 := h (0 : Fin 2) (1 : Fin 2)
535     norm_num [PIntegralRational, positiveSignProjector] at h01
536 
537 /-- The negative sign projector has exact `2`-local denominator weight one. -/
538 theorem negativeSignProjector_exact_dyadic_pLocal_weight :
539     HasExactPLocalDenominatorWeight 2 negativeSignProjector 1 := by
540   constructor
541   · intro i j
542     fin_cases i <;> fin_cases j <;>
543       norm_num [PIntegralMatrix, PIntegralRational, negativeSignProjector]
544   · intro t ht
545     have ht0 : t = 0 := Nat.lt_one_iff.mp ht
546     subst t
547     intro h
548     have h01 := h (0 : Fin 2) (1 : Fin 2)
549     norm_num [PIntegralRational, negativeSignProjector] at h01
550 
551 /-- At every prime other than two, the positive sign projector already has exact local
552 denominator weight zero. -/
553 theorem positiveSignProjector_exact_pLocal_weight_zero_of_prime_ne_two {p : ℕ}
554     (hp : p.Prime) (hp2 : p ≠ 2) :
555     HasExactPLocalDenominatorWeight p positiveSignProjector 0 := by
556   constructor
557   · simpa using positiveSignProjector_pIntegral_of_prime_ne_two hp hp2
558   · intro t ht
559     exact (Nat.not_lt_zero t ht).elim
560 
561 /-- At every prime other than two, the negative sign projector already has exact local
562 denominator weight zero. -/
563 theorem negativeSignProjector_exact_pLocal_weight_zero_of_prime_ne_two {p : ℕ}
564     (hp : p.Prime) (hp2 : p ≠ 2) :
565     HasExactPLocalDenominatorWeight p negativeSignProjector 0 := by
566   constructor
567   · simpa using negativeSignProjector_pIntegral_of_prime_ne_two hp hp2
568   · intro t ht
569     exact (Nat.not_lt_zero t ht).elim
570 
571 /-- The concrete resultant of the two linear sign factors `X - 1` and `X + 1` is `2`. -/
572 theorem signFactors_resultant :
573     Polynomial.resultant (Polynomial.X - Polynomial.C (1 : ℤ))
574       (Polynomial.X + Polynomial.C (1 : ℤ)) = 2 := by
575   rw [Polynomial.natDegree_X_sub_C, Polynomial.natDegree_X_add_C]
576   norm_num
577 
578 /-- The denominator/resultant `2` has `2`-adic valuation one. -/
579 theorem padicValNat_two_two : padicValNat 2 2 = 1 := by
580   exact padicValNat_self
581 
582 /-- The positive projector's exact dyadic local weight is the `2`-adic valuation of the
583 computed sign-factor resultant. -/
584 theorem positiveSignProjector_exact_pLocal_weight_at_resultantValuation :
585     HasExactPLocalDenominatorWeight 2 positiveSignProjector (padicValNat 2 2) := by
586   rw [padicValNat_two_two]
587   exact positiveSignProjector_exact_dyadic_pLocal_weight
588 
589 /-- The negative projector's exact dyadic local weight is the `2`-adic valuation of the
590 computed sign-factor resultant. -/
591 theorem negativeSignProjector_exact_pLocal_weight_at_resultantValuation :
592     HasExactPLocalDenominatorWeight 2 negativeSignProjector (padicValNat 2 2) := by
593   rw [padicValNat_two_two]
594   exact negativeSignProjector_exact_dyadic_pLocal_weight
595 
596 /-- Combined endpoint: the sign-factor resultant is `2`, its `2`-adic valuation is one, and
597 that value is the exact `2`-local denominator weight of both sign projectors. -/
598 theorem signProjectors_resultant_dyadic_weight_endpoint :
599     Polynomial.resultant (Polynomial.X - Polynomial.C (1 : ℤ))
600         (Polynomial.X + Polynomial.C (1 : ℤ)) = 2 ∧
601       padicValNat 2 2 = 1 ∧
602       HasExactPLocalDenominatorWeight 2 positiveSignProjector (padicValNat 2 2) ∧
603       HasExactPLocalDenominatorWeight 2 negativeSignProjector (padicValNat 2 2) := by
604   exact ⟨signFactors_resultant, padicValNat_two_two,
605     positiveSignProjector_exact_pLocal_weight_at_resultantValuation,
606     negativeSignProjector_exact_pLocal_weight_at_resultantValuation⟩
607 
608 /-- At every prime distinct from two (hence every odd prime), the denominator/resultant `2` has
609 valuation zero. -/
610 theorem padicValNat_two_at_odd_prime {p : ℕ} (hp : p.Prime) (hp2 : p ≠ 2) :
611     padicValNat p 2 = 0 := by
612   let _ : Fact p.Prime := ⟨hp⟩
613   exact padicValNat_primes hp2
614 
615 /--
616 Direct traceability wrapper for the manuscript's odd-adic versus dyadic sign
617 proposition.  It combines the exact local weights of both displayed
618 projectors with the resultant valuation at two and at every other prime.
619 -/
620 theorem oddAdicVersusDyadicSignBehavior_trace :
621     HasExactPLocalDenominatorWeight 2 positiveSignProjector 1 ∧
622       HasExactPLocalDenominatorWeight 2 negativeSignProjector 1 ∧
623       Polynomial.resultant (Polynomial.X - Polynomial.C (1 : ℤ))
624           (Polynomial.X + Polynomial.C (1 : ℤ)) = 2 ∧
625       padicValNat 2 2 = 1 ∧
626       ∀ p : ℕ, p.Prime → p ≠ 2 →
627         HasExactPLocalDenominatorWeight p positiveSignProjector 0 ∧
628         HasExactPLocalDenominatorWeight p negativeSignProjector 0 ∧
629         padicValNat p 2 = 0 := by
630   refine ⟨positiveSignProjector_exact_dyadic_pLocal_weight,
631     negativeSignProjector_exact_dyadic_pLocal_weight,
632     signFactors_resultant, padicValNat_two_two, ?_⟩
633   intro p hp hp2
634   exact ⟨positiveSignProjector_exact_pLocal_weight_zero_of_prime_ne_two hp hp2,
635     negativeSignProjector_exact_pLocal_weight_zero_of_prime_ne_two hp hp2,
636     padicValNat_two_at_odd_prime hp hp2⟩
637 
638 /-! ## Smith phase -/
639 
640 /-- The pulled-back phase action on a normalized Smith impedance. -/
641 def smithPhase {k : Type u} [Field k] (omega z : k) : k :=
642   ((1 + omega) * z + (1 - omega)) /
643     ((1 - omega) * z + (1 + omega))
644 
645 /-- Over every field in which two is nonzero, the phase `omega = -1` interchanges impedance and
646 admittance by inversion. -/
647 theorem smithPhase_neg_one_eq_inv {k : Type u} [Field k] [NeZero (2 : k)]
648     (z : k) (_hz : z ≠ 0) :
649     smithPhase (-1) z = z⁻¹ := by
650   simp only [smithPhase, add_neg_cancel, zero_mul, zero_add, sub_neg_eq_add,
651     one_add_one_eq_two, add_zero]
652   calc
653     (2 : k) / (2 * z) = ((2 : k) * 1) / ((2 : k) * z) := by rw [mul_one]
654     _ = 1 / z := mul_div_mul_left 1 z (NeZero.ne (2 : k))
655     _ = z⁻¹ := one_div z
656 
657 end Komorebi.PaperII.SmithDyadic

Back to source controls