OAI/RepresentationTheory/RowColumn/Dephasing.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RowColumn.Signed.actWord_swap_fixed line 16
2. lemma OAI.RowColumn.Signed.oddPerm_swap_sign line 29
3. lemma OAI.RowColumn.Signed.commuting_coefficient_zero_of_pair_repeat line 50

   Source documentation

   Repeated opposite-parity pair symbols force a commutant coefficient to vanish. This is the finite-sign obstruction behind signed postselection.

   lemma commuting_coefficient_zero_of_pair_repeat
       (T : Representation.IntertwiningMap (representation (S := S) (odd := odd) (k := k))
   …

   Mentions: OAI.RowColumn.Signed.representation

4. abbrev OAI.RowColumn.Signed.ParityMismatch line 73
5. lemma OAI.RowColumn.Signed.mismatch_pair_injective line 77
6. lemma OAI.RowColumn.Signed.commuting_parity_bandwidth line 90

   Source documentation

   Every nonzero coefficient changes parity in at most |C|² slots. For the actual slot space C=Fin h ⊕ Fin h this is at most 4h², independent of s.

   lemma commuting_parity_bandwidth
       (T : Representation.IntertwiningMap (representation (S := S) (odd := odd) (k := k))
   …

   Mentions: OAI.RowColumn.Signed.representation

7. abbrev OAI.RowColumn.ShortSubsets line 105
8. def OAI.RowColumn.shortSubsetCode line 107
9. lemma OAI.RowColumn.shortSubsetCode_mem line 111
10. lemma OAI.RowColumn.shortSubsetCode_injective line 127
11. lemma OAI.RowColumn.card_shortSubsets_le line 135
12. def OAI.RowColumn.parityDifference line 140
13. def OAI.RowColumn.parityNear line 142
14. instance OAI.RowColumn.(instance at line 144) line 144
15. lemma OAI.RowColumn.parityNear_symm line 147
16. lemma OAI.RowColumn.parityDifference_injective line 157
17. lemma OAI.RowColumn.parityNear_count line 165
18. def OAI.RowColumn.energy line 185
19. lemma OAI.RowColumn.positive_cross_bound line 187
20. lemma OAI.RowColumn.positive_banded_sum line 203

    Source documentation

    A positive block-banded matrix is dominated by its block diagonal times the maximum number of nonzero block neighbours. This will be applied to physical parity allocations, where signed symmetry supplies a polynomial bound.

    lemma positive_banded_sum (A : V →ₗ[ℂ] V) (hA : A.IsPositive)
        (v : B → V) (R : B → B → Prop) [DecidableRel R]
        (hRs : Std.Symm R) (D : ℕ)
        (hD : ∀ i, (Finset.univ.filter (R i)).card ≤ D)
        (hz : ∀ i j, ¬ R i j → inner ℂ (v i) (A (v j)) = 0) :
        energy A (∑ i, v i) ≤ (D : ℝ) * ∑ i, energy A (v i) := by
    …

    Mentions: OAI.RowColumn.energy

21. def OAI.RowColumn.Signed.parityPattern line 260
22. def OAI.RowColumn.Signed.parityMask line 262
23. lemma OAI.RowColumn.Signed.sum_parityMasks line 267
24. lemma OAI.RowColumn.Signed.inner_wordVector line 272
25. lemma OAI.RowColumn.Signed.parityNear_of_coefficient_ne_zero line 276
26. lemma OAI.RowColumn.Signed.parityMask_inner_zero line 293
27. theorem OAI.RowColumn.Signed.signed_parity_dephasing line 322

    Source documentation

    Exact signed dephasing inequality. No LR or highest-weight estimate: positivity plus the swap-forced bandwidth yields polynomial cost in the physical parity allocation, the hard structural step for local domination.

    theorem signed_parity_dephasing
        (T : Representation.IntertwiningMap (representation (S := S) (odd := odd) (k := k))
    …

    Mentions: OAI.RowColumn.Signed.representation

28. lemma OAI.RowColumn.Signed.swap_mem_lineGroup line 345
29. lemma OAI.RowColumn.Signed.line_coefficient_zero_of_pair_repeat line 355
30. lemma OAI.RowColumn.Signed.line_mismatch_injective line 377
31. lemma OAI.RowColumn.Signed.line_parity_bandwidth line 390
32. lemma OAI.RowColumn.Signed.line_parityNear_of_coefficient_ne_zero line 400
33. lemma OAI.RowColumn.Signed.line_parityMask_inner_zero line 417
34. theorem OAI.RowColumn.Signed.line_signed_parity_dephasing line 446

    Source documentation

    Exact signed dephasing inequality. No LR or highest-weight estimate: positivity plus the swap-forced bandwidth yields polynomial cost in the physical parity allocation, the hard structural step for local domination.

    theorem line_signed_parity_dephasing
        (T : Representation.IntertwiningMap (lineRepresentation (odd := odd) (k := k) line)
    …

    Mentions: OAI.RowColumn.Signed.lineRepresentation