CompletedShiftedCornerEvaluation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.QuadraticEncoding.completed_shifted_corner_square line 15
Source documentation
The same corner action evaluates correctly on every formal shift, including shift 3.
```
theorem completed_shifted_corner_square (n : ℤ) :
    (completedDerivedEvaluation X).map
      (((functorExtension₂ (BoundedQ P) (BoundedQ P)).obj (shiftFunctor (BoundedQ P) n)).map
        (quotientCornerEnd e a he)) ≫ (completedShiftedSummandImageIso X e he n).hom =
    (completedShiftedSummandImageIso X e he n).hom ≫ (evaluatedCornerEnd X e a)⟦n⟧' := by
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.completedDerivedEvaluation, OAI.LittleFinitistic.QuadraticEncoding.BoundedQ, OAI.LittleFinitistic.QuadraticEncoding.quotientCornerEnd, OAI.LittleFinitistic.QuadraticEncoding.completedShiftedSummandImageIso, OAI.LittleFinitistic.QuadraticEncoding.evaluatedCornerEnd