FrozenCancel.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.cancel_frozen line 25
Source documentation
Frozen dipole cancellation in a picture which also has arbitrary free macro faces. It removes complete opposite frozen cells, preserves every surviving frozen face, and preserves the exact elementary signed chain.
```
theorem cancel_frozen (B : FrozenTarget T) (hm : P.FrozenMapped B)
    (a : P.Dart) (ha : T.free (T.kind (P.index a)) = false)
    (hop : P.index (P.pairing.edge a) = T.opposite (P.index a)) :
    ∃ Q : WalkPicture.{u} T, Nonempty (P.Survives Q) ∧ Q.FrozenMapped B ∧
      Fintype.card Q.Dart < Fintype.card P.Dart ∧ Q.chain = P.chain := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.FrozenTarget