ImmPairingCompatibility.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.closePaths_immInternalPathVertices line 11

Source documentation

Closing the four internal IMM paths gives the canonical endpoint-fixed labels.

theorem closePaths_immInternalPathVertices (d : ℕ)
    (p q r s : Fin d → Fin (d + 1)) (t : Fin (d + 2)) :
    Pairings.closePaths 0 (fun i => ⟨p i, q i, r i, s i⟩) t =
      (⟨immInternalPathVertices d p t, immInternalPathVertices d q t,
        immInternalPathVertices d r t, immInternalPathVertices d s t⟩ :
          Pairings.Labels (Fin (d + 1))) := by
…

Mentions: OAI.Problem335.Pairings.closePaths, OAI.Problem335.immInternalPathVertices, OAI.Problem335.Pairings.Labels

theorem OAI.Problem335.layerLabels_immInternalCoordinate line 25

Source documentation

Layer labels used in the relaxed pairing sum are the actual four IMM coordinates.

theorem layerLabels_immInternalCoordinate (d : ℕ)
    (p q r s : Fin d → Fin (d + 1)) (t : Fin (d + 1)) :
    MomentPairing.layerLabels 0 (fun i => ⟨p i, q i, r i, s i⟩) t =
      (⟨immInternalCoordinate d p t, immInternalCoordinate d q t,
        immInternalCoordinate d r t, immInternalCoordinate d s t⟩ :
          Pairings.Labels (Fin (d + 1) × Fin (d + 1))) := by
…

Mentions: OAI.Problem335.MomentPairing.layerLabels, OAI.Problem335.immInternalCoordinate, OAI.Problem335.Pairings.Labels

theorem OAI.Problem335.immInternalPath_shift_sub_eq_iff_compatible line 36

Source documentation

The actual four-path shift constraint is exactly the compatibility predicate used by the weighted exact-to-relaxed pairing inequality.

theorem immInternalPath_shift_sub_eq_iff_compatible (d : ℕ)
    (side : Fin (d + 1) → Bool) (p q r s : Fin d → Fin (d + 1)) :
    occupationShift (fun e => side e.1) (immInternalPathEdges d p) -
        occupationShift (fun e => side e.1) (immInternalPathEdges d q) =
      occupationShift (fun e => side e.1) (immInternalPathEdges d r) -
        occupationShift (fun e => side e.1) (immInternalPathEdges d s) ↔
      MomentPairing.Compatible 0 (fun i => ⟨p i, q i, r i, s i⟩) := by
…

Mentions: OAI.Problem335.occupationShift, OAI.Problem335.immInternalPathEdges, OAI.Problem335.MomentPairing.Compatible