BinaryPrescriptions.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Binary Prescriptions

def OAI.HadwigerCounterexample.aiming line 16
Source documentation
list for a cross edge
```
def aiming (a b : I → Bool) (i j : Bool) :=
…
```
abbrev OAI.HadwigerCounterexample.Script line 22
Source documentation
within-endpoint L/R bit tests. Read only a x=a y, x≠y. (tests between ordered points; no double counting since L,R and both orientations are in the mixer hypothesis).
```
abbrev Script (p : Shape) (I : Type) := I → I → Vec (MOne p)
…
```
Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.MOne
def OAI.HadwigerCounterexample.Volley.reads line 26
def OAI.HadwigerCounterexample.prescribedB line 31
def OAI.HadwigerCounterexample.prescribedT line 35
def OAI.HadwigerCounterexample.fulfills line 40
theorem OAI.HadwigerCounterexample.Volley.B1_eval line 50
theorem OAI.HadwigerCounterexample.Volley.grads_by_script line 68

theorem OAI.HadwigerCounterexample.binary_plan line 93

Source documentation

Solve symmetric row sums at one endpoint. Couple via opposite same-target pmiss/role sum equality. Only the resulting necessary (common d+f sum) is used as input here.

private theorem binary_plan (a b : I→Bool) (i : Bool) (d f : Vec I)
    (h : (∑ j∈aiming a b i true,(d j+f j))=∑ j∈aiming a b i false,(d j+f j))
    (h' : ∀ j,(aiming a b i j).Nonempty) :
    ∃ M : Mat I I, Mᵀ=M ∧ (∀ x,M x x=d x) ∧ ∀ j : Bool,∀ x∈Finset.univ.filter (fun l => a l=i),
      (∑ l∈aiming a b i j,M l x) = d x+(if j=b x then 0 else f x) := by
…

Mentions: OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.aiming, OAI.HadwigerCounterexample.Mat

theorem OAI.HadwigerCounterexample.scripted line 191
theorem OAI.HadwigerCounterexample.choose_script line 218