ClockCancellation.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

The actual cancellation coefficients

These are the algebraic relations of the degree 0,1,-1 coefficients of the existing cancellation path. They follow from the two orthogonal isometries and the supplied unitary; no new path or unitarity hypothesis is introduced for the clock-corrected expression.

def OAI.WeakPureInfiniteness.clockCancellationIncrement line 21
Source documentation
The sum of the two diagonal corner increments.
```
def clockCancellationIncrement (a b u : E) : E :=
…
```
def OAI.WeakPureInfiniteness.clockCancellationCross line 25
Source documentation
The positive-degree off-diagonal coefficient.
```
def clockCancellationCross (a b u : E) : E := a * (u - 1) * star b
```
def OAI.WeakPureInfiniteness.clockCancellationDiagonal line 28
Source documentation
The constant coefficient of the cancellation polynomial.
```
def clockCancellationDiagonal (a b u : E) (τ : ℝ) : E :=
…
```
lemma OAI.WeakPureInfiniteness.clock_corner_mul line 31
lemma OAI.WeakPureInfiniteness.clock_corner_zero line 37
lemma OAI.WeakPureInfiniteness.clockCancellationCross_star line 43
lemma OAI.WeakPureInfiniteness.clockCancellationCross_sq line 47
lemma OAI.WeakPureInfiniteness.clockCancellationIncrement_star line 53
lemma OAI.WeakPureInfiniteness.clockCancellationIncrement_cross line 58
lemma OAI.WeakPureInfiniteness.clockCancellationIncrement_star_cross line 70
lemma OAI.WeakPureInfiniteness.clockCancellationIncrement_gram line 85
lemma OAI.WeakPureInfiniteness.clockCancellationIncrement_normal line 103
lemma OAI.WeakPureInfiniteness.clockCancellationIncrement_identity line 118
lemma OAI.WeakPureInfiniteness.clockCancellationDiagonal_star_cross line 136
lemma OAI.WeakPureInfiniteness.clockCancellationDiagonal_cross line 145

lemma OAI.WeakPureInfiniteness.clockCancellationDiagonal_gram line 155

Source documentation

The constant Gram coefficient is exactly one; the nonzero coefficients cancel by the preceding cross relations and square-zero identity.

lemma clockCancellationDiagonal_gram (a b u : E)
    (ha : star a * a = 1) (hb : star b * b = 1) (hab : star a * b = 0)
    (hu : u ∈ unitary E) (τ ν : ℝ) (hτν : τ ^ 2 + ν ^ 2 = τ) :
    star (clockCancellationDiagonal a b u τ) * clockCancellationDiagonal a b u τ +
      (ν ^ 2) • (star (clockCancellationCross a b u) * clockCancellationCross a b u +
        clockCancellationCross a b u * star (clockCancellationCross a b u)) = 1 := by
…

Mentions: OAI.WeakPureInfiniteness.clockCancellationDiagonal, OAI.WeakPureInfiniteness.clockCancellationCross

lemma OAI.WeakPureInfiniteness.clockCancellationDiagonal_cogram line 176

lemma OAI.WeakPureInfiniteness.clockCancellation_actual_grams line 194

Source documentation

The trigonometric parameters of the actual cancellation path satisfy both constant-coefficient Gram identities.

lemma clockCancellation_actual_grams (a b u : E)
    (ha : star a * a = 1) (hb : star b * b = 1) (hab : star a * b = 0)
    (hu : u ∈ unitary E) (θ : ℝ) :
    (star (clockCancellationDiagonal a b u (Real.cos θ ^ 2)) *
      clockCancellationDiagonal a b u (Real.cos θ ^ 2) +
      (Real.sin θ * Real.cos θ) ^ 2 •
        (star (clockCancellationCross a b u) * clockCancellationCross a b u +
          clockCancellationCross a b u * star (clockCancellationCross a b u)) = 1) ∧
    (clockCancellationDiagonal a b u (Real.cos θ ^ 2) *
      star (clockCancellationDiagonal a b u (Real.cos θ ^ 2)) +
      (Real.sin θ * Real.cos θ) ^ 2 •
        (star (clockCancellationCross a b u) * clockCancellationCross a b u +
…

Mentions: OAI.WeakPureInfiniteness.clockCancellationDiagonal, OAI.WeakPureInfiniteness.clockCancellationCross

def OAI.WeakPureInfiniteness.clockCancellationDegrees line 214
Source documentation
The three actual homogeneous degrees and coefficients.
```
def clockCancellationDegrees : Fin 3 → ℤ := ![0, 1, -1]
```
def OAI.WeakPureInfiniteness.clockCancellationCoefficients line 216
lemma OAI.WeakPureInfiniteness.clockCorrectedCancellation_eq_sum line 221

lemma OAI.WeakPureInfiniteness.clockThreeTerm_initial_gram line 238

Source documentation

The initial Gram polynomial vanishes in every nonzero degree.

lemma clockThreeTerm_initial_gram (k : unitary E) (D X : E) (ν : ℝ)
    (hX : X * X = 0) (hDX : star D * X = X * D)
    (hG : star D * D + ν ^ 2 • (star X * X + X * star X) = 1) :
    clockDegreeCorrection k 0 (star D * D) +
      clockDegreeCorrection k 1 (star D * (ν • X)) +
      clockDegreeCorrection k (-1) (star D * (-ν • star X)) +
      (clockDegreeCorrection k (-1) (star (ν • X) * D) +
       clockDegreeCorrection k 0 (star (ν • X) * (ν • X)) +
       clockDegreeCorrection k (-2) (star (ν • X) * (-ν • star X))) +
      (clockDegreeCorrection k 1 (star (-ν • star X) * D) +
       clockDegreeCorrection k 2 (star (-ν • star X) * (ν • X)) +
       clockDegreeCorrection k 0 (star (-ν • star X) * (-ν • star X))) = 1 := by
…

Mentions: OAI.WeakPureInfiniteness.clockDegreeCorrection

lemma OAI.WeakPureInfiniteness.clockThreeTerm_final_gram line 262

Source documentation

The final Gram polynomial has the same exact cancellation.

lemma clockThreeTerm_final_gram (k : unitary E) (D X : E) (ν : ℝ)
    (hX : X * X = 0) (hDX : D * X = X * star D)
    (hG : D * star D + ν ^ 2 • (star X * X + X * star X) = 1) :
    clockDegreeCorrection k 0 (D * star D) +
      clockDegreeCorrection k (-1) (D * star (ν • X)) +
      clockDegreeCorrection k 1 (D * star (-ν • star X)) +
      (clockDegreeCorrection k 1 ((ν • X) * star D) +
       clockDegreeCorrection k 0 ((ν • X) * star (ν • X)) +
       clockDegreeCorrection k 2 ((ν • X) * star (-ν • star X))) +
      (clockDegreeCorrection k (-1) ((-ν • star X) * star D) +
       clockDegreeCorrection k (-2) ((-ν • star X) * star (ν • X)) +
       clockDegreeCorrection k 0 ((-ν • star X) * star (-ν • star X))) = 1 := by
…

Mentions: OAI.WeakPureInfiniteness.clockDegreeCorrection

lemma OAI.WeakPureInfiniteness.clockCancellation_convolution_grams line 287

Source documentation

Exact initial and final convolution identities for the actual three coefficients, before estimating the noncentral clock corrections.

lemma clockCancellation_convolution_grams (k : unitary E) (a b u : E)
    (ha : star a * a = 1) (hb : star b * b = 1) (hab : star a * b = 0)
    (hu : u ∈ unitary E) (θ : ℝ) :
    (∑ i, ∑ j, clockDegreeCorrection k
      (-clockCancellationDegrees i + clockCancellationDegrees j)
      (star (clockCancellationCoefficients a b u θ i) *
        clockCancellationCoefficients a b u θ j)) = 1 ∧
    (∑ i, ∑ j, clockDegreeCorrection k
      (clockCancellationDegrees i - clockCancellationDegrees j)
      (clockCancellationCoefficients a b u θ i *
        star (clockCancellationCoefficients a b u θ j))) = 1 := by
…

Mentions: OAI.WeakPureInfiniteness.clockDegreeCorrection, OAI.WeakPureInfiniteness.clockCancellationDegrees, OAI.WeakPureInfiniteness.clockCancellationCoefficients