GuardedPath.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

A deterministic arbitrary-repair obstruction for the fixed binary pattern. A selection records one common tree path, dummy positions, and four selected anchor frames per edge. Its guards contain only root, dummy, anchor, and anchor/body signature cells -- never the unconstrained variable body cells.

structure OAI.Problem348.GuardedPath.Selection line 17
Source documentation
Selected positions; no host construction or matching assumptions are hidden in this data structure. Values past the chosen depth are irrelevant.
```
structure Selection (n : ℕ) where
…
```
def OAI.Problem348.GuardedPath.Selection.CoreCell line 33
Source documentation
Root and dummy cells needed for Boolean propagation.
```
def CoreCell (P : Selection n) (h : ℕ) (rc : Fin n × Fin n) : Prop :=
…
```
Mentions: OAI.Problem348.GuardedPath.Selection
def OAI.Problem348.GuardedPath.Selection.EdgeCell line 39
Source documentation
Anchor and signature cells for the four modes at one edge.
```
def EdgeCell (P : Selection n) (i : ℕ) (rc : Fin n × Fin n) : Prop :=
…
```
Mentions: OAI.Problem348.GuardedPath.Selection
def OAI.Problem348.GuardedPath.Selection.GuardCell line 46
Source documentation
The protected cells of the whole selected path.
```
def GuardCell (P : Selection n) (h : ℕ) (rc : Fin n × Fin n) : Prop :=
…
```
Mentions: OAI.Problem348.GuardedPath.Selection
def OAI.Problem348.GuardedPath.Selection.guards line 49
theorem OAI.Problem348.GuardedPath.Selection.mem_guards line 53
structure OAI.Problem348.GuardedPath.Selection.Valid line 60
Source documentation
Explicit original-matrix conditions on a selected path. The frame validity contains all required order comparisons and all 64-anchor signatures.
```
structure Valid (P : Selection n) (A : BinaryMatrix n) (h : ℕ) : Prop where
…
```
Mentions: OAI.Problem348.GuardedPath.Selection, OAI.Problem348.BinaryMatrix
theorem OAI.Problem348.GuardedPath.Selection.Valid.transfer line 78
Source documentation
If no guard cell was edited, every condition needed for path propagation and exact anchor completion survives.
```
theorem Valid.transfer {P : Selection n} {A B : BinaryMatrix n} {h : ℕ}
    (hv : P.Valid A h)
    (hag : ∀ rc ∈ P.guards h, A rc.1 rc.2 = B rc.1 rc.2) :
    P.Valid B h := by
…
```
Mentions: OAI.Problem348.GuardedPath.Selection, OAI.Problem348.BinaryMatrix
theorem OAI.Problem348.GuardedPath.Selection.Valid.not_HFree line 116
Source documentation
Every valid selected path gives a copy of the exact fixed H.
```
theorem Valid.not_HFree {P : Selection n} {B : BinaryMatrix n} {h : ℕ}
    (hv : P.Valid B h) : ¬ HFree fixedH B := by
…
```
Mentions: OAI.Problem348.GuardedPath.Selection, OAI.Problem348.BinaryMatrix, OAI.Problem348.HFree, OAI.Problem348.fixedH
theorem OAI.Problem348.GuardedPath.Selection.not_HFree_of_agree line 127
Source documentation
Arbitrary edits outside the finite guard set cannot destroy all copies.
```
theorem not_HFree_of_agree {P : Selection n} {A B : BinaryMatrix n} {h : ℕ}
    (hv : P.Valid A h)
    (hag : ∀ rc ∈ P.guards h, A rc.1 rc.2 = B rc.1 rc.2) :
    ¬ HFree fixedH B :=
…
```
Mentions: OAI.Problem348.GuardedPath.Selection, OAI.Problem348.BinaryMatrix, OAI.Problem348.HFree, OAI.Problem348.fixedH
theorem OAI.Problem348.GuardedPath.Selection.repair_hits_guards line 135
Source documentation
Every H-free repair must hit the guard set of each valid selected path. This is a statement about all repairs, not just destroying original copies.
```
theorem repair_hits_guards {P : Selection n} {A B : BinaryMatrix n} {h : ℕ}
    (hv : P.Valid A h) (hfree : HFree fixedH B) :
    ∃ rc ∈ P.guards h, A rc.1 rc.2 ≠ B rc.1 rc.2 := by
…
```
Mentions: OAI.Problem348.GuardedPath.Selection, OAI.Problem348.BinaryMatrix, OAI.Problem348.HFree, OAI.Problem348.fixedH