PatternSuffixFaces.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.ParityBridge.patternEmbed_smul line 20

Source documentation

Every literal recursive suffix has its original D action.

theorem patternEmbed_smul (p : List Bool)
    (hbase : ∀ (d : D) (v : N), (inl d : A) • v = d • v)
    (d : D) (v : patternTerm k D X N p) :
    embed k D X N p (d • v) = (inl d : A) • embed k D X N p v := by
…

theorem OAI.DerivedBar.ParityBridge.patternEmbed_ideal_zero line 38
Source documentation
The leading X annihilates any X-leading suffix, irrespective of later blocks.
```
theorem patternEmbed_ideal_zero (p : List Bool) (x : X)
    (v : patternTerm k D X N (true :: p)) :
    (inr x : A) • embed k D X N (true :: p) v = 0 := by
…
```

theorem OAI.DerivedBar.ParityBridge.idealPatternEmbed_smul line 49

Source documentation

Compatibility of every X-leading recursive suffix needs no condition at N.

theorem idealPatternEmbed_smul (p : List Bool) (d : D)
    (v : patternTerm k D X N (true :: p)) :
    embed k D X N (true :: p) (d • v) =
      (inl d : A) • embed k D X N (true :: p) v := by
…

theorem OAI.DerivedBar.ParityBridge.parity_recursiveSuffix line 61
Source documentation
All later X and D blocks are admitted literally, with no assumed chain comparison.
```
theorem parity_recursiveSuffix (p : List Bool) (n : ℕ)
    (v : X ⊗[k] term k D (patternTerm k D X N (true :: p)) (n+1)) :
    let M := patternTerm k D X N (true :: p)
…
```
Mentions: OAI.DerivedBar.term

theorem OAI.DerivedBar.ParityBridge.parity_recursiveSuffix_zero line 77

Source documentation

Empty intervening D blocks retain exactly the later suffix differential.

theorem parity_recursiveSuffix_zero (p : List Bool)
    (v : X ⊗[k] patternTerm k D X N (true :: p)) :
    SquareZero.multibarAugmentedDifferential k D X N (p.length+1)
      (idealSuffixEmbed k D X N _ (p.length+1) 0 (embed k D X N (true :: p)) v) =
    idealSuffixEmbed k D X N _ p.length 0
      ((SquareZero.multibarAugmentedDifferential k D X N p.length).comp
        (embed k D X N (true :: p))) v := by
…

Mentions: OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.idealSuffixEmbed