OAI/RepresentationTheory/SignedTensor/Domination.lean

GitHub source file

122 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CoordinateSweeps.SignedTensor.partialTrace_regroup line 23

   Source comment

   Partial-trace invariance of the actual regrouping signs on each fixed exception sector. No assumption of complex conditional probabilities occurs.

   theorem partialTrace_regroup {p l : ℕ} (E : Finset (Fin l))
       (v : Word p l × Word p l → ℂ)
       (hv : ∀ u w, v (u,w) ≠ 0 → ∀ i,
         (odd (u i) ↔ ¬ odd (w i)) ↔ i ∈ E) :
       partialTrace (PositiveTensor.outer (fun uw => regroupPhase uw.1 uw.2 * v uw)) =
         partialTrace (PositiveTensor.outer v) := by
   …

   Mentions: OAI.CoordinateSweeps.SignedTensor.Word, OAI.CoordinateSweeps.SignedTensor.odd, OAI.CoordinateSweeps.PositiveTensor.outer, OAI.CoordinateSweeps.SignedTensor.regroupPhase

2. abbrev OAI.CoordinateSweeps.SignedTensor.Pair line 49
3. abbrev OAI.CoordinateSweeps.SignedTensor.MatchedPair line 50
4. structure OAI.CoordinateSweeps.SignedTensor.ExceptionPattern line 54

   Source comment

   Valid pinned exceptional data. Injectivity is essential: it is supplied by the proved repeated-mismatch cancellation, not imposed on the kernel.

   structure ExceptionPattern (p l : ℕ) where
   …

5. def OAI.CoordinateSweeps.SignedTensor.entryPattern line 62

   Source comment

   Every nonzero commuting matrix entry has literal valid exceptional data.

   def entryPattern {p l : ℕ} (A : commutant p l) (u w : Word p l) (h : A.val u w ≠ 0) :
       ExceptionPattern p l where
   …

   Mentions: OAI.CoordinateSweeps.SignedTensor.commutant, OAI.CoordinateSweeps.SignedTensor.Word, OAI.CoordinateSweeps.SignedTensor.ExceptionPattern

6. def OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.encode line 77
7. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.encode_eq_some line 80
8. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.mem_sites_iff line 97
9. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.encode_injective line 105
10. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.card_le line 125
11. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.sites_card_le line 130
12. abbrev OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.Free line 135

    Source comment

    Slots not occupied by a pinned exceptional symbol.

    abbrev Free (F : ExceptionPattern p l) := {i : Fin l // i ∉ F.sites}

    Mentions: OAI.CoordinateSweeps.SignedTensor.ExceptionPattern

13. abbrev OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.FreeWord line 136
14. def OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.fillPair line 138
15. def OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.fill line 141
16. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.fillPair_at_pin line 144
17. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.fillPair_at_free line 147
18. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.fill_mismatch_iff line 150
19. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.fill_injective line 160
20. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.fill_disjoint line 168
21. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.entry_in_range line 186
22. def OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.extendPerm line 202

    Source comment

    Extend a permutation of the free slots by the identity on the exceptions.

    def extendPerm (F : ExceptionPattern p l) (σ : Equiv.Perm F.Free) : Equiv.Perm (Fin l) :=
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.ExceptionPattern

23. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.extendPerm_pin line 205
24. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.extendPerm_free line 209
25. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.fill_transport line 213
26. def OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.purified line 230
27. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.purified_invariant line 233
28. def OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.embedding line 249
29. def OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.component line 252
30. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.component_image line 255
31. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.component_inclusion line 259
32. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.purified_inclusion line 270
33. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.component_partialTrace line 283
34. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.component_sum line 296
35. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.component_square_sum line 313
36. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.purified_trace line 330
37. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.sum_purified_trace line 344
38. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.free_card line 357
39. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.free_card_pos line 359
40. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.free_card_le line 362
41. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.matchedPair_nonempty line 366
42. theorem OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.component_postselection line 371

    Source comment

    Exact domination of a pinned component by a finite product mixture on its free slots, after the proved sign cancellation in the genuine partial trace.

    theorem component_postselection (F : ExceptionPattern p l) (hp : 0 < p)
        (hl : (2*p)*(2*p) < l) (A : commutant p l) :
        ((Matrix.trace (OrdinaryTensor.outer (F.purified A)) *
            ((Fintype.card F.Free+1 : ℕ) : ℂ)^(2*Fintype.card (MatchedPair p))) •
          partialTrace (inclusion F.embedding * (OrdinaryTensor.finiteMixture (I := F.Free) (A := MatchedPair p)) * (inclusion F.embedding).conjTranspose) -
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.ExceptionPattern, OAI.CoordinateSweeps.SignedTensor.commutant, OAI.CoordinateSweeps.OrdinaryTensor.outer, OAI.CoordinateSweeps.SignedTensor.MatchedPair, OAI.CoordinateSweeps.OrdinaryTensor.finiteMixture

43. def OAI.CoordinateSweeps.SignedTensor.pairAmplitude line 392
44. lemma OAI.CoordinateSweeps.SignedTensor.pairAmplitude_unit_trace line 395
45. lemma OAI.CoordinateSweeps.SignedTensor.pairAmplitude_even line 413
46. def OAI.CoordinateSweeps.SignedTensor.pairDensity line 426

    Source comment

    The real even one-site density obtained by the literal auxiliary partial trace of a unit matched-pair vector.

    def pairDensity {p : ℕ} (z : MatchedPair p → ℂ) (hz : ∑ a, z a * star (z a) = 1) : EvenDensity p :=
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.MatchedPair, OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.SignedTensor.EvenDensity

47. def OAI.CoordinateSweeps.SignedTensor.basisDensity line 435
48. lemma OAI.CoordinateSweeps.SignedTensor.basisDensity_posSemidef line 438
49. lemma OAI.CoordinateSweeps.SignedTensor.basisDensity_le_one line 444
50. lemma OAI.CoordinateSweeps.SignedTensor.basisDensity_trace line 458
51. def OAI.CoordinateSweeps.SignedTensor.pinAmplitude line 461
52. lemma OAI.CoordinateSweeps.SignedTensor.pinAmplitude_density line 464
53. def OAI.CoordinateSweeps.SignedTensor.keep line 474
54. def OAI.CoordinateSweeps.SignedTensor.noise line 475
55. lemma OAI.CoordinateSweeps.SignedTensor.keep_nonneg line 477
56. lemma OAI.CoordinateSweeps.SignedTensor.noise_nonneg line 478
57. lemma OAI.CoordinateSweeps.SignedTensor.keep_add_noise line 479
58. def OAI.CoordinateSweeps.SignedTensor.depolarized line 485
59. lemma OAI.CoordinateSweeps.SignedTensor.depolarized_posSemidef line 488
60. lemma OAI.CoordinateSweeps.SignedTensor.depolarized_trace line 492
61. lemma OAI.CoordinateSweeps.SignedTensor.depolarized_even line 497
62. def OAI.CoordinateSweeps.SignedTensor.depolarizedDensity line 502
63. lemma OAI.CoordinateSweeps.SignedTensor.depolarized_free line 505
64. lemma OAI.CoordinateSweeps.SignedTensor.depolarized_pin line 510
65. def OAI.CoordinateSweeps.SignedTensor.pinnedDensity line 522
66. lemma OAI.CoordinateSweeps.SignedTensor.pinnedDensity_posSemidef line 526
67. lemma OAI.CoordinateSweeps.SignedTensor.keep_pow_lower line 534
68. lemma OAI.CoordinateSweeps.SignedTensor.pin_coefficient_le line 547
69. theorem OAI.CoordinateSweeps.SignedTensor.pinned_absorption line 566

    Source comment

    Each pinned ordinary product density is dominated by a tensor power of a single even density, with only polynomial cost per actual exception.

    theorem pinned_absorption (s : ℕ) (hp : 0 < p) (hls : l ≤ s)
        (E : Finset (Fin l)) (a : E → Letter p) (r : EvenDensity p) :
        (((s+1 : ℝ) * ((s+1 : ℝ)*(2*p))^E.card : ℝ) : ℂ) •
          densityPower l (depolarized s r) - pinnedDensity E a r |>.PosSemidef := by
    …

    Mentions: OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.SignedTensor.Letter, OAI.CoordinateSweeps.SignedTensor.EvenDensity, OAI.CoordinateSweeps.SignedTensor.densityPower, OAI.CoordinateSweeps.SignedTensor.depolarized, OAI.CoordinateSweeps.SignedTensor.pinnedDensity

70. theorem OAI.CoordinateSweeps.SignedTensor.pinned_absorption_uniform line 623
71. def OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.siteAmplitude line 641
72. def OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.pairProduct line 645
73. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.siteAmplitude_pin line 648
74. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.siteAmplitude_free line 654
75. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.pairProduct_fill line 660
76. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.pairProduct_nonzero line 667
77. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.pairProduct_inclusion line 684
78. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.filled_product_partialTrace line 697

    Source comment

    Partial tracing a filled product vector yields pinned basis densities at the true exceptions and the same even density at every remaining slot.

    lemma filled_product_partialTrace (F : ExceptionPattern p l) (z : MatchedPair p → ℂ)
        (hz : ∑ a, z a * star (z a) = 1) :
        partialTrace (PositiveTensor.outer ((inclusion F.embedding).mulVec (OrdinaryTensor.tensorVector z))) =
          pinnedDensity F.sites (fun i => (F.pair i).1) (pairDensity z hz) := by
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.ExceptionPattern, OAI.CoordinateSweeps.SignedTensor.MatchedPair, OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.PositiveTensor.outer, OAI.CoordinateSweeps.OrdinaryTensor.tensorVector, OAI.CoordinateSweeps.SignedTensor.pinnedDensity, OAI.CoordinateSweeps.SignedTensor.pairDensity

79. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.purified_trace_le line 719
80. abbrev OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.Data line 724
81. def OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.dataDensity line 727
82. def OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.dataPoint line 730
83. def OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.rawPinned line 734
84. def OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.rawDensity line 738
85. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.rawPinned_posSemidef line 742
86. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.rawDensity_posSemidef line 745
87. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.rawMixture_partialTrace line 749
88. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.rawPinned_domination line 765
89. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.rawPinned_absorption line 774
90. lemma OAI.CoordinateSweeps.SignedTensor.matchedPair_card_le line 787
91. def OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.empty line 793
92. instance OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.(instance at line 799) line 799
93. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.data_card_le line 801
94. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.free_power_le line 815
95. lemma OAI.CoordinateSweeps.SignedTensor.ExceptionPattern.component_uniform_domination line 822
96. abbrev OAI.CoordinateSweeps.SignedTensor.DensityProfile line 852
97. lemma OAI.CoordinateSweeps.SignedTensor.densityProfile_card_le line 854
98. lemma OAI.CoordinateSweeps.SignedTensor.densityProfile_nonempty line 864
99. def OAI.CoordinateSweeps.SignedTensor.profilePoint line 869
100. def OAI.CoordinateSweeps.SignedTensor.rawProfileDensity line 872
101. lemma OAI.CoordinateSweeps.SignedTensor.rawProfileDensity_eq line 876
102. lemma OAI.CoordinateSweeps.SignedTensor.rawProfileDensity_posSemidef line 880
103. theorem OAI.CoordinateSweeps.SignedTensor.commutant_covariance_domination line 885

     Source comment

     Finite postselection for the literal signed action commutant.

     theorem commutant_covariance_domination (s p l : ℕ) (hp : 0 < p) (hps : p ≤ s)
         (hls : l ≤ s) (hl : (2*p)*(2*p) < l) (A : commutant p l) :
         ((Matrix.trace (A.val*A.val.conjTranspose) * ((s+1 : ℕ) : ℂ)^(25*p^2)) •
           rawProfileDensity s p l hp hl - A.val*A.val.conjTranspose).PosSemidef := by
     …

     Mentions: OAI.CoordinateSweeps.SignedTensor.commutant, OAI.CoordinateSweeps.SignedTensor.rawProfileDensity

104. def OAI.CoordinateSweeps.FiniteAtomic.uniform line 918
105. instance OAI.CoordinateSweeps.FiniteAtomic.uniform_probability line 921
106. lemma OAI.CoordinateSweeps.FiniteAtomic.uniform_integral line 927
107. instance OAI.CoordinateSweeps.SignedTensor.(instance at line 939) line 939
108. lemma OAI.CoordinateSweeps.SignedTensor.isotypic_mem_commutant line 945
109. lemma OAI.CoordinateSweeps.SignedTensor.isotypic_self_mul line 951
110. lemma OAI.CoordinateSweeps.SignedTensor.isotypic_trace_le line 955
111. theorem OAI.CoordinateSweeps.SignedTensor.density_domination_large line 965

     Source comment

     The large-slot case, as an actual probability mixture of even densities.

     theorem density_domination_large (s p l : ℕ) (hp : 0 < p) (hps : p ≤ s) (hls : l ≤ s)
         (hl : (2*p)*(2*p) < l) (ρ : UnitaryIrrep (Equiv.Perm (Fin l))) :
         ∃ μ : Measure (EvenDensity p), IsProbabilityMeasure μ ∧
           (((ρ.dimension : ℂ) * ((s+1 : ℕ) : ℂ)^(41*p^2)) •
             (∫ r : EvenDensity p, densityPower l r.val ∂μ) - isotypic (p := p) ρ).PosSemidef := by
     …

     Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.SignedTensor.EvenDensity, OAI.CoordinateSweeps.SignedTensor.densityPower, OAI.CoordinateSweeps.SignedTensor.isotypic

112. def OAI.CoordinateSweeps.SignedTensor.uniformDensity line 1009
113. lemma OAI.CoordinateSweeps.SignedTensor.densityPower_one line 1019
114. lemma OAI.CoordinateSweeps.SignedTensor.densityPower_smul line 1029
115. lemma OAI.CoordinateSweeps.SignedTensor.uniformDensity_power line 1034
116. lemma OAI.CoordinateSweeps.SignedTensor.small_power_le line 1039
117. theorem OAI.CoordinateSweeps.SignedTensor.density_domination_small line 1048

     Source comment

     Small slot counts, including zero, require no exceptional-sector chart.

     theorem density_domination_small (s p l : ℕ) (hp : 0 < p) (hps : p ≤ s) (hls : l ≤ s)
         (hl : l ≤ (2*p)*(2*p)) (ρ : UnitaryIrrep (Equiv.Perm (Fin l))) :
         ∃ μ : Measure (EvenDensity p), IsProbabilityMeasure μ ∧
           (((ρ.dimension : ℂ) * ((s+1 : ℕ) : ℂ)^(12*p^2)) •
             (∫ r : EvenDensity p, densityPower l r.val ∂μ) - isotypic (p := p) ρ).PosSemidef := by
     …

     Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.SignedTensor.EvenDensity, OAI.CoordinateSweeps.SignedTensor.densityPower, OAI.CoordinateSweeps.SignedTensor.isotypic

118. lemma OAI.CoordinateSweeps.SignedTensor.domination_coefficient line 1075
119. theorem OAI.CoordinateSweeps.SignedTensor.signed_density_domination line 1088

     Source comment

     Source05 equation13, with a concrete absolute constant. The measure is constructed from finite empirical phase mixtures, not an added hypothesis.

     theorem signed_density_domination : Domination := by
     …

     Mentions: OAI.CoordinateSweeps.SignedTensor.Domination

120. lemma OAI.CoordinateSweeps.SignedTensor.finite_profile_domination line 1118
121. lemma OAI.CoordinateSweeps.SignedTensor.finite_uniform_domination line 1152
122. theorem OAI.CoordinateSweeps.SignedTensor.finite_density_domination line 1173

     Source comment

     Finite (not a hypothetical measure) version of source05:eq13.

     theorem finite_density_domination (s p l : ℕ) (hp : 0 < p) (hps : p ≤ s) (hls : l ≤ s)
         (ρ : UnitaryIrrep (Equiv.Perm (Fin l))) :
         ∃ (I : Type) (_ : Fintype I) (_ : Nonempty I) (r : I → EvenDensity p),
           (((ρ.dimension : ℂ)*((s+1 : ℕ) : ℂ)^(41*p^2)) •
             ((Fintype.card I : ℂ)⁻¹ • ∑ i, densityPower l (r i).val)-isotypic (p := p) ρ).PosSemidef := by
     …

     Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.SignedTensor.EvenDensity, OAI.CoordinateSweeps.SignedTensor.densityPower, OAI.CoordinateSweeps.SignedTensor.isotypic