FiniteAmplificationReduction.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Finite amplification is reduced to centered symmetry tests on square Hilbert arrays. The operator replacement and its symmetry bound remain explicit local hypotheses; the padding, dilation, coordinate change, and perturbation losses are all proved here.

def OAI.KadisonSimilarity.amplifiedScalarRepresentation line 22
Source documentation
The actual diagonal amplification of a star representation.
```
def amplifiedScalarRepresentation (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (n : ℕ) :
    A →⋆ₐ[ℂ] (HilbertCopies H n →L[ℂ] HilbertCopies H n) where
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.amplifiedScalarRepresentation_apply line 36
theorem OAI.KadisonSimilarity.norm_represented_commutator_pad_both line 42
Source documentation
Matrix padding and multiplicity padding preserve the actual represented commutator, with independent injections on the two indices.
```
theorem norm_represented_commutator_pad_both {r m s t : ℕ}
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (e : Fin r ↪ Fin m) (f : Fin s ↪ Fin t)
    (Y : HilbertCopies H r →L[ℂ] HilbertCopies H r)
    (X : CStarMatrix (Fin s) (Fin s) A) :
    ‖commutator (amplify (padArrayOperator e Y) t)
      (representedMatrix (amplifiedScalarRepresentation σ m) (cstarMatrixPadding f X))‖ =
    ‖commutator (amplify Y s) (representedMatrix (amplifiedScalarRepresentation σ r) X)‖ := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.padArrayOperator, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.amplifiedScalarRepresentation, OAI.KadisonSimilarity.cstarMatrixPadding
theorem OAI.KadisonSimilarity.norm_represented_flattened_symmetry_le line 58
Source documentation
The represented flattened symmetry is contractive even for a degenerate representation, since it is the image of an actual unitary.
```
theorem norm_represented_flattened_symmetry_le {n : ℕ} [NeZero n]
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (X : CStarMatrix (Fin n) (Fin n) A) (hX : ‖X‖ ≤ 1) :
    ‖representedMatrix σ (fourfoldMatrixFlatten n (contractionSymmetryUnitary X hX))‖ ≤ 1 := by
…
```
Mentions: OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.fourfoldMatrixFlatten, OAI.KadisonSimilarity.contractionSymmetryUnitary

theorem OAI.KadisonSimilarity.flattened_symmetry_bound_of_approximation line 70

Source documentation

Restoring the original operator after a norm-small replacement loses at most twice that distance on the flattened unitary test.

theorem flattened_symmetry_bound_of_approximation {n : ℕ} [NeZero n]
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (Y : H →L[ℂ] H)
    (X : CStarMatrix (Fin n) (Fin n) A) (hX : ‖X‖ ≤ 1)
    (Y₀ : HilbertCopies H (4 * n) →L[ℂ] HilbertCopies H (4 * n))
    {η B : ℝ} (hclose : ‖Y₀ - amplify Y (4 * n)‖ ≤ η)
    (hbound : ‖commutator Y₀
      (representedMatrix σ (fourfoldMatrixFlatten n (contractionSymmetryUnitary X hX)))‖ ≤ B) :
    ‖commutator (amplify Y n) (representedMatrix σ X)‖ ≤ B + 2 * η := by
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.fourfoldMatrixFlatten, OAI.KadisonSimilarity.contractionSymmetryUnitary

theorem OAI.KadisonSimilarity.finite_amplification_bound_of_one_symmetry line 94

Source documentation

A test of arbitrary matrix size and multiplicity is controlled by one centered symmetry test in a square array. The symmetry bound is an explicit hypothesis, rather than an assumed conclusion about all matrix tests.

theorem finite_amplification_bound_of_one_symmetry {r h n : ℕ} [NeZero n]
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (e : Fin r ↪ Fin (4 * n)) (f : Fin h ↪ Fin n)
    (Y : HilbertCopies H r →L[ℂ] HilbertCopies H r)
    (X : CStarMatrix (Fin h) (Fin h) A) (hX : ‖X‖ ≤ 1)
    (Y₀ : HilbertCopies (HilbertCopies H (4 * n)) (4 * n) →L[ℂ]
      HilbertCopies (HilbertCopies H (4 * n)) (4 * n))
    {η B : ℝ}
    (hclose : ‖Y₀ - amplify (padArrayOperator e Y) (4 * n)‖ ≤ η)
    (hbound : ‖commutator Y₀
      (representedMatrix (amplifiedScalarRepresentation σ (4 * n))
        (fourfoldMatrixFlatten n (contractionSymmetryUnitary (cstarMatrixPadding f X)
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.padArrayOperator, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.amplifiedScalarRepresentation, OAI.KadisonSimilarity.fourfoldMatrixFlatten, OAI.KadisonSimilarity.contractionSymmetryUnitary, OAI.KadisonSimilarity.cstarMatrixPadding

theorem OAI.KadisonSimilarity.norm_amplify_sub_le line 117
Source documentation
Amplifying the replacement does not enlarge its norm distance.
```
theorem norm_amplify_sub_le (S T : H →L[ℂ] H) (n : ℕ) :
    ‖amplify S n - amplify T n‖ ≤ ‖S - T‖ := by
…
```
Mentions: OAI.KadisonSimilarity.amplify

theorem OAI.KadisonSimilarity.finite_amplification_bound_of_multiplicity_approximation line 127

Source documentation

The manuscript's replacement lives on the multiplicity space; its amplification supplies the square-array replacement without further loss.

theorem finite_amplification_bound_of_multiplicity_approximation
    {r h n : ℕ} [NeZero n]
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (e : Fin r ↪ Fin (4 * n)) (f : Fin h ↪ Fin n)
    (Y : HilbertCopies H r →L[ℂ] HilbertCopies H r)
    (X : CStarMatrix (Fin h) (Fin h) A) (hX : ‖X‖ ≤ 1)
    (Y₀ : HilbertCopies H (4 * n) →L[ℂ] HilbertCopies H (4 * n))
    {η B : ℝ} (hclose : ‖Y₀ - padArrayOperator e Y‖ ≤ η)
    (hbound : ‖commutator (amplify Y₀ (4 * n))
      (representedMatrix (amplifiedScalarRepresentation σ (4 * n))
        (fourfoldMatrixFlatten n (contractionSymmetryUnitary (cstarMatrixPadding f X)
          (by simpa only [norm_cstarMatrixPadding] using hX))))‖ ≤ B) :
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.padArrayOperator, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.amplifiedScalarRepresentation, OAI.KadisonSimilarity.fourfoldMatrixFlatten, OAI.KadisonSimilarity.contractionSymmetryUnitary, OAI.KadisonSimilarity.cstarMatrixPadding, OAI.KadisonSimilarity.norm_cstarMatrixPadding

theorem OAI.KadisonSimilarity.padded_flattened_symmetry_properties line 146
Source documentation
The symmetry appearing in the preceding reduction is selfadjoint, squares to one, and is centered for the actual normalized matrix trace.
```
theorem padded_flattened_symmetry_properties {h n : ℕ} [NeZero n]
    (τ : A →ₚ[ℂ] ℂ) (f : Fin h ↪ Fin n)
    (X : CStarMatrix (Fin h) (Fin h) A) (hX : ‖X‖ ≤ 1) :
    let S := fourfoldMatrixFlatten n (contractionSymmetryUnitary (cstarMatrixPadding f X)
…
```
Mentions: OAI.KadisonSimilarity.fourfoldMatrixFlatten, OAI.KadisonSimilarity.contractionSymmetryUnitary, OAI.KadisonSimilarity.cstarMatrixPadding

theorem OAI.KadisonSimilarity.finite_amplification_bound_of_centered_tests line 160

Source documentation

Uniform centered-square symmetry bounds, together with the actual norm approximation, control every finite matrix amplification. This theorem is a reduction: its symmetry bound must be proved separately in the application.

theorem finite_amplification_bound_of_centered_tests {r : ℕ}
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (τ : A →ₚ[ℂ] ℂ)
    (Y : HilbertCopies H r →L[ℂ] HilbertCopies H r) {η B : ℝ}
    (hconstant : 0 ≤ B + 2 * η)
    (hreplace : ∀ (n : ℕ) [NeZero n], ∀ e : Fin r ↪ Fin (4 * n),
      ∃ Y₀ : HilbertCopies (HilbertCopies H (4 * n)) (4 * n) →L[ℂ]
          HilbertCopies (HilbertCopies H (4 * n)) (4 * n),
        ‖Y₀ - amplify (padArrayOperator e Y) (4 * n)‖ ≤ η ∧
        ∀ S : CStarMatrix (Fin (4 * n)) (Fin (4 * n)) A,
          star S = S → S * S = 1 → normalizedMatrixTrace τ (4 * n) S = 0 →
          ‖commutator Y₀ (representedMatrix (amplifiedScalarRepresentation σ (4 * n)) S)‖ ≤ B)
    (h : ℕ) (X : CStarMatrix (Fin h) (Fin h) A) :
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.padArrayOperator, OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.amplifiedScalarRepresentation