ConstraintAudit.lean

1 module
2 
3 public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
4 public import Mathlib.Tactic.NormNum
5 public import Mathlib.Tactic.FinCases
6 
7 /-!
8 Author: Komorebi P.
9 A scope audit of Paper VII Section 12. When the physical projector has image in
10 the exact common kernel, the proposed physical anomaly test vanishes identically.
11 This is not an operator-closure theorem or an existence theorem for a continuum tower.
12 -/
13 public section
14 set_option autoImplicit false
15 namespace KomorebiPaperVII.ConstraintAudit
16 open scoped BigOperators
17 
18 section Algebra
19 variable {R I : Type*} [Ring R] [Fintype I]
20 
21 /-- Scalar structure coefficients, including any factor i, may be embedded in R. -/
22 def anomaly (C : I → R) (f : I → R) (a b : I) : R :=
23   C a * C b - C b * C a - ∑ c, f c * C c
24 
25 /-- No projector axioms are needed: right annihilation alone suffices. -/
26 theorem anomaly_annihilates_common_kernel (C : I → R) (f : I → R)
27     (P : R) (hP : ∀ c, C c * P = 0) (a b : I) :
28     anomaly C f a b * P = 0 := by
29   simp [anomaly, sub_mul, Finset.sum_mul, mul_assoc, hP]
30 
31 theorem compressed_anomaly_zero (C : I → R) (f : I → R)
32     (P : R) (hP : ∀ c, C c * P = 0) (a b : I) :
33     P * anomaly C f a b * P = 0 := by
34   rw [mul_assoc, anomaly_annihilates_common_kernel C f P hP, mul_zero]
35 end Algebra
36 
37 /-- A nonzero exact physical packet, with two noncommuting Hermitian constraints
38 acting only on its complement. Rational matrices suffice for this counterexample. -/
39 def physical : Matrix (Fin 3) (Fin 3) ℚ := !![1,0,0; 0,0,0; 0,0,0]
40 def constraintX : Matrix (Fin 3) (Fin 3) ℚ := !![0,0,0; 0,0,1; 0,1,0]
41 def constraintZ : Matrix (Fin 3) (Fin 3) ℚ := !![0,0,0; 0,1,0; 0,0,-1]
42 
43 theorem physical_idempotent : physical * physical = physical := by
44   ext i j; fin_cases i <;> fin_cases j <;> norm_num [physical, Matrix.mul_apply, Fin.sum_univ_succ]
45 
46 theorem physical_nonzero : physical ≠ 0 := by
47   intro h
48   have h00 := congrArg (fun A : Matrix (Fin 3) (Fin 3) ℚ => A 0 0) h
49   norm_num [physical] at h00
50 
51 theorem constraints_annihilate_physical :
52     constraintX * physical = 0 ∧ constraintZ * physical = 0 := by
53   constructor <;> ext i j <;> fin_cases i <;> fin_cases j <;>
54     norm_num [physical, constraintX, constraintZ, Matrix.mul_apply, Fin.sum_univ_succ]
55 
56 theorem commutator_nonzero : constraintX * constraintZ - constraintZ * constraintX ≠ 0 := by
57   intro h
58   have h12 := congrArg (fun A : Matrix (Fin 3) (Fin 3) ℚ => A 1 2) h
59   norm_num [constraintX, constraintZ, Matrix.mul_apply, Fin.sum_univ_succ] at h12
60   norm_num [Matrix.cons_val_two] at h12
61 
62 theorem physical_commutator_zero :
63     physical * (constraintX * constraintZ - constraintZ * constraintX) * physical = 0 := by
64   simp only [mul_assoc, mul_sub, sub_mul, constraints_annihilate_physical.1,
65     constraints_annihilate_physical.2, mul_zero, sub_self]
66 
67 end KomorebiPaperVII.ConstraintAudit
68 
69 /-! Exported theorem axiom audit. -/
70 #print axioms KomorebiPaperVII.ConstraintAudit.anomaly_annihilates_common_kernel
71 #print axioms KomorebiPaperVII.ConstraintAudit.compressed_anomaly_zero
72 #print axioms KomorebiPaperVII.ConstraintAudit.physical_idempotent
73 #print axioms KomorebiPaperVII.ConstraintAudit.physical_nonzero
74 #print axioms KomorebiPaperVII.ConstraintAudit.constraints_annihilate_physical
75 #print axioms KomorebiPaperVII.ConstraintAudit.commutator_nonzero
76 #print axioms KomorebiPaperVII.ConstraintAudit.physical_commutator_zero

Back to source controls