WeightedCycles.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.KervaireMatrix.clock_rotate line 22

Source documentation

The finite clock advances by a root of unity, including at the cut.

theorem clock_rotate {n : ℕ} (z : ℂ) (hz : z^(n+1) = 1) (i : Fin (n+1)) :
    z^((finRotate (n+1) i).val) = z * z^i.val := by
…

theorem OAI.KervaireMatrix.clock_weightedShift line 32
Source documentation
Rephasing a labelled weighted cycle implements scalar rotation exactly.
```
theorem clock_weightedShift (n : ℕ) (z : ℂ) (hz : z^(n+1) = 1)
    (u : Fin (n+1) → ℂ) (a : Fin (n+1) → A) :
    scalarDiagonal (A := A) (fun i : Fin (n+1) => z^i.val) *
…
```
Mentions: OAI.KervaireMatrix.scalarDiagonal

theorem OAI.KervaireMatrix.phase_weightedShift_root line 47

Source documentation

Spectral phase of a finite weighted cycle is invariant under every clock rotation.

theorem phase_weightedShift_root (n : ℕ) (z : ℂ) (hz : z^(n+1) = 1)
    (hzu : z ∈ unitary ℂ) (u : Fin (n+1) → ℂ) (a : Fin (n+1) → A)
    (hu : ∀ i, u i ∈ unitary ℂ) :
    let _ := isStarNormal_of_mem_unitary (weightedShift_unitary (finRotate (n+1)) u a hu)
…

Mentions: OAI.KervaireMatrix.weightedShift_unitary

theorem OAI.KervaireMatrix.phase_weightedShift_grid line 73

Source documentation

The exact first half of the boundary-cycle phase computation.

theorem phase_weightedShift_grid (n : ℕ) (u : Fin (n+1) → ℂ)
    (a : Fin (n+1) → A) (hu : ∀ i, u i ∈ unitary ℂ) :
    let _ := isStarNormal_of_mem_unitary (weightedShift_unitary (finRotate (n+1)) u a hu)
…

Mentions: OAI.KervaireMatrix.weightedShift_unitary

theorem OAI.KervaireSpectral.vectorPhase_eq_of_moments line 102
def OAI.KervaireRegular.leftOperator line 119
theorem OAI.KervaireRegular.leftOperator_delta line 121
theorem OAI.KervaireRegular.leftOperator_one line 124
theorem OAI.KervaireRegular.leftOperator_mul line 128
theorem OAI.KervaireRegular.leftOperator_pow line 132
theorem OAI.KervaireRegular.leftOperator_unitary line 137
def OAI.KervaireRegular.groupPhase line 148
Source documentation
Exact scalar-rotated fractional phase of a group element.
```
def groupPhase (z : ℂ) (hz : z ∈ unitary ℂ) (a : A) : ℝ :=
…
```
theorem OAI.KervaireRegular.moment_group_weight line 153
Source documentation
Scalar moments really are the coefficients of the left-regular circuit word.
```
theorem moment_group_weight (z : ℂ) (a : A) (n : ℕ) :
    inner ℂ (delta (1 : A)) (((z • leftOperator a)^n) (delta 1)) =
      if a^n = 1 then z^n else 0 := by
…
```
Mentions: OAI.KervaireRegular.delta, OAI.KervaireRegular.leftOperator
theorem OAI.KervaireRegular.groupPhase_conjugate line 162
Source documentation
Changing the starting point of a labelled circuit preserves its exact phase.
```
theorem groupPhase_conjugate (z : ℂ) (hz : z ∈ unitary ℂ) (a b : A) :
    groupPhase z hz (b*a*b⁻¹) = groupPhase z hz a := by
…
```
Mentions: OAI.KervaireRegular.groupPhase
theorem OAI.KervaireMatrix.weightedDiagonal_pow_delta line 185
theorem OAI.KervaireMatrix.phase_weightedDiagonal line 198
Source documentation
The phase of the diagonal circuit power is the sum of the literal regular phases.
```
theorem phase_weightedDiagonal (u : D → ℂ) (a : D → A)
    (hu : ∀ i, u i ∈ unitary ℂ) :
    let _ := isStarNormal_of_mem_unitary (weightedShift_unitary (Equiv.refl D) u a hu)
…
```
Mentions: OAI.KervaireMatrix.weightedShift_unitary

def OAI.KervaireCycle.orbitWeight line 223

Source documentation

Circuit weights in their actual operator multiplication order.

def orbitWeight (σ : Equiv.Perm D) (b : D → B) : ℕ → D → B
  | 0, _ => 1
  | n+1, i => b ((σ^n) i) * orbitWeight σ b n i

theorem OAI.KervaireCycle.orbitWeight_zero line 227
theorem OAI.KervaireCycle.orbitWeight_succ line 229

theorem OAI.KervaireCycle.orbitWeight_add line 233

Source documentation

Cutting an oriented circuit respects the noncommutative order of labels.

theorem orbitWeight_add (σ : Equiv.Perm D) (b : D → B) (n m : ℕ) (i : D) :
    orbitWeight σ b (n+m) i =
      orbitWeight σ b n ((σ^m) i) * orbitWeight σ b m i := by
…

Mentions: OAI.KervaireCycle.orbitWeight

theorem OAI.KervaireCycle.orbitWeight_cycle line 243
Source documentation
A circuit with trivial permutation has conjugate weights at successive points.
```
theorem orbitWeight_cycle (σ : Equiv.Perm D) (b : D → B) (n : ℕ)
    (hn : σ^n = 1) (i : D) :
    orbitWeight σ b n (σ i) * b i = b i * orbitWeight σ b n i := by
…
```
Mentions: OAI.KervaireCycle.orbitWeight

theorem OAI.KervaireCycle.rotate_pow_apply line 250

Source documentation

The rotate permutation is addition modulo its size.

theorem rotate_pow_apply (d : ℕ) [NeZero d] (n : ℕ) (i : Fin d) :
    ((finRotate d)^n) i = i + (↑n : Fin d) := by
…

theorem OAI.KervaireCycle.rotate_pow_self line 258

theorem OAI.KervaireMatrix.weightedShift_pow line 270

Source documentation

Exact powers of the scalar/group-labelled shift.

theorem weightedShift_pow (σ : Equiv.Perm D) (u : D → ℂ) (a : D → A) (n : ℕ) :
    weightedShift σ u a ^ n = weightedShift (σ^n)
      (orbitWeight σ u n) (orbitWeight σ a n) := by
…

Mentions: OAI.KervaireMatrix.weightedShift

theorem OAI.KervaireMatrix.weightedShift_cycle_pow line 280

Source documentation

After one complete circuit the operator is diagonal, with the original circuit weights.

theorem weightedShift_cycle_pow (d : ℕ) [NeZero d] (u : Fin d → ℂ) (a : Fin d → A) :
    weightedShift (finRotate d) u a ^ d = weightedShift (Equiv.refl (Fin d))
      (orbitWeight (finRotate d) u d) (orbitWeight (finRotate d) a d) := by
…

Mentions: OAI.KervaireMatrix.weightedShift

theorem OAI.KervaireCycle.orbitWeight_mem line 291
Source documentation
All full and partial circuit products remain in any submonoid containing the labels.
```
theorem orbitWeight_mem (H : Submonoid B) (σ : Equiv.Perm D) (b : D → B)
    (hb : ∀ i, b i ∈ H) (n : ℕ) (i : D) : orbitWeight σ b n i ∈ H := by
…
```
Mentions: OAI.KervaireCycle.orbitWeight

theorem OAI.KervaireCycle.orbitWeight_start line 298

Source documentation

Starting a full circuit after a partial traversal conjugates its weight.

theorem orbitWeight_start (σ : Equiv.Perm D) (b : D → B) (d j : ℕ)
    (hd : σ^d = 1) (i : D) :
    orbitWeight σ b d ((σ^j) i) * orbitWeight σ b j i =
      orbitWeight σ b j i * orbitWeight σ b d i := by
…

Mentions: OAI.KervaireCycle.orbitWeight

theorem OAI.KervaireMatrix.scalar_orbitWeight_constant line 313

Source documentation

The scalar circuit weight is independent of its starting point, literally.

theorem scalar_orbitWeight_constant (d : ℕ) [NeZero d] (u : Fin d → ℂ)
    (hu : ∀ i, u i ∈ unitary ℂ) (i : Fin d) :
    orbitWeight (finRotate d) u d i = orbitWeight (finRotate d) u d 0 := by
…

theorem OAI.KervaireMatrix.group_orbitWeight_conjugate line 325

Source documentation

The group circuit weight is conjugated in the exact operator order.

theorem group_orbitWeight_conjugate (d : ℕ) [NeZero d] (a : Fin d → A) (i : Fin d) :
    orbitWeight (finRotate d) a d i =
      orbitWeight (finRotate d) a i.val 0 * orbitWeight (finRotate d) a d 0 *
        (orbitWeight (finRotate d) a i.val 0)⁻¹ := by
…

theorem OAI.KervaireMatrix.groupPhase_orbitWeight_constant line 335

Source documentation

The diagonal full-circuit power has identical scalar regular phases on every slot.

theorem groupPhase_orbitWeight_constant (d : ℕ) [NeZero d] (u : Fin d → ℂ)
    (a : Fin d → A) (hu : ∀ i, u i ∈ unitary ℂ) (i : Fin d) :
    groupPhase (orbitWeight (finRotate d) u d i)
        (orbitWeight_mem (unitary ℂ) _ u hu _ _) (orbitWeight (finRotate d) a d i) =
      groupPhase (orbitWeight (finRotate d) u d 0)
        (orbitWeight_mem (unitary ℂ) _ u hu _ _) (orbitWeight (finRotate d) a d 0) := by
…

theorem OAI.KervaireMatrix.phase_weightedCycle line 346
Source documentation
The literal weighted boundary-cycle formula, including the phase cut at 1. No cyclic-word hypothesis, approximation, or finite-group restriction is used.
```
theorem phase_weightedCycle (n : ℕ) (u : Fin (n+1) → ℂ)
    (a : Fin (n+1) → A) (hu : ∀ i, u i ∈ unitary ℂ) :
    let _ := isStarNormal_of_mem_unitary (weightedShift_unitary (finRotate (n+1)) u a hu)
…
```
Mentions: OAI.KervaireMatrix.weightedShift_unitary