GuardedFrame.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact selected-anchor frames and their protected cells. The frame does not constrain any of the four body entries.

structure OAI.Problem348.GuardedPath.AnchorFrame line 12
structure OAI.Problem348.GuardedPath.AnchorFrame.Valid line 21
Source documentation
All data needed to extend a body, except the body entries themselves.
```
structure Valid (F : AnchorFrame n) (A : BinaryMatrix n)
    (r₀ r₁ c₀ c₁ : Fin n) : Prop where
…
```
Mentions: OAI.Problem348.GuardedPath.AnchorFrame, OAI.Problem348.BinaryMatrix
def OAI.Problem348.GuardedPath.AnchorFrame.Cell line 34
Source documentation
Precisely the anchor and signature cells of one selected frame.
```
def Cell (F : AnchorFrame n) (r₀ r₁ c₀ c₁ : Fin n)
    (rc : Fin n × Fin n) : Prop :=
…
```
Mentions: OAI.Problem348.GuardedPath.AnchorFrame

theorem OAI.Problem348.GuardedPath.AnchorFrame.Valid.transfer line 41

Source documentation

Agreement only on frame cells preserves anchor and signature validity.

theorem Valid.transfer {F : AnchorFrame n} {A B : BinaryMatrix n}
    {r₀ r₁ c₀ c₁ : Fin n} (hF : F.Valid A r₀ r₁ c₀ c₁)
    (hag : ∀ rc, F.Cell r₀ r₁ c₀ c₁ rc → A rc.1 rc.2 = B rc.1 rc.2) :
    F.Valid B r₀ r₁ c₀ c₁ := by
…

Mentions: OAI.Problem348.GuardedPath.AnchorFrame, OAI.Problem348.BinaryMatrix

theorem OAI.Problem348.GuardedPath.AnchorFrame.Valid.not_HFree line 58
Source documentation
A valid frame and the body give a genuine ordered copy of the fixed H.
```
theorem Valid.not_HFree {F : AnchorFrame n} {B : BinaryMatrix n}
    {r₀ r₁ c₀ c₁ : Fin n} (hF : F.Valid B r₀ r₁ c₀ c₁)
    (hbody : PathPropagation.Body B r₀ r₁ c₀ c₁) : ¬ HFree fixedH B := by
…
```
Mentions: OAI.Problem348.GuardedPath.AnchorFrame, OAI.Problem348.BinaryMatrix, OAI.Problem348.PathPropagation.Body, OAI.Problem348.HFree, OAI.Problem348.fixedH