ExtendedLocalMoment.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.LocalMoments.sourcePathAmplitude line 15
Source documentation
The explicit path amplitude on the canonical fixed-bidegree source indices.
```
def sourcePathAmplitude {ι σ : Type*} [Fintype ι]
    {side : ι → Bool} {a b : ℕ} (M : BidegreeSource (σ := σ) side a b)
…
```
lemma OAI.Problem335.LocalMoments.sourceIndex_shiftRelation line 20
theorem OAI.Problem335.LocalMoments.extended_four_path_product_eq line 36
Source documentation
The complete zero-extension bridge required by the eliminated-source second trace. Valid shifts remain in the fixed bidegree domain; invalid shifts give zero on both sides.
```
theorem extended_four_path_product_eq {ι σ : Type*} [Fintype ι] [Fintype σ]
    [DecidableEq σ] {side : ι → Bool} {a b : ℕ}
    (M : BidegreeSource (σ := σ) side a b) (p q r s : ι → σ)
…
```