GlobalIndexedComparison.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.ParityBridge.eqToHom_chain_d line 29
theorem OAI.DerivedBar.ParityBridge.flatEmbedding_differential line 37
Source documentation
The full leading comparison transferred through the actual flattening.
```
theorem flatEmbedding_differential (r n : ℕ) :
    flatEmbedding k D X N r (n+1) ≫
      ModuleCat.ofHom (SquareZero.multibarTwoSidedDifferential k D X N (r+n)) =
    RecursiveTotal.differential (leadingBarSequence k D X r) Z (r+1) n ≫ flatEmbedding k D X N r n := by
…
```
Mentions: OAI.DerivedBar.ParityBridge.flatEmbedding, OAI.DerivedBar.SquareZero.multibarTwoSidedDifferential, OAI.DerivedBar.RecursiveTotal.differential, OAI.DerivedBar.leadingBarSequence
theorem OAI.DerivedBar.ParityBridge.conjugated_differential_comp line 45
theorem OAI.DerivedBar.ParityBridge.indexedDifferential_assembly line 55
Source documentation
The original Shape differential intertwines the independently defined literal parity faces through the original tensor-block assembly.
```
theorem indexedDifferential_assembly (r n : ℕ) :
    indexedDifferential k D X N r n ≫ shapeAssembly k D X N r n =
      shapeAssembly k D X N r (n+1) ≫
        ModuleCat.ofHom (SquareZero.multibarTwoSidedDifferential k D X N (r+n)) := by
…
```
Mentions: OAI.DerivedBar.ParityBridge.shapeAssembly, OAI.DerivedBar.SquareZero.multibarTwoSidedDifferential
theorem OAI.DerivedBar.ParityBridge.inflated_ideal_zero line 65
theorem OAI.DerivedBar.ParityBridge.globalIndexedComparison line 71
Source documentation
The global comparison identifies the independently defined recursive differential, Shape coordinates, signed block differential, and both sign identities.
```
theorem globalIndexedComparison (r n : ℕ) :
    (indexedDifferential k D X N r n).hom =
      (-1:k)^r • Multibar.Indexed.blockDifferential k D X N
        (fun x v => inflated_ideal_zero D X N x v) (r+n) r := by
…
```
Mentions: OAI.DerivedBar.Multibar.Indexed.blockDifferential, OAI.DerivedBar.ParityBridge.inflated_ideal_zero