Affine wall-decision cover certificates

AffineCover.CoverTree proves a union of cones by choosing a violated row from every cone. Highly overlapping cone families can make that proof enormous. This file supplies the dual passive certificate: branch on one integral affine wall and its exact strict complement, stop as soon as one advertised cone is literally contained in the active rows, and close infeasible sign chambers by a Farkas certificate.

The checker is deliberately small. Generated search code is untrusted; only the Boolean replay and the theorem below enter the proof.

inductive Utilities.Certificate.AffineCover.DecisionTreeData (m : ℕ) : Type

Passive, emitter-friendly wall decision data.

• impossible {m : ℕ} (farkas : FarkasData) : DecisionTreeData m
• select {m : ℕ} (cone : ℕ) : DecisionTreeData m
• branch {m : ℕ} (form : AffineForm m) (holds fails : DecisionTreeData m) : DecisionTreeData m

def Utilities.Certificate.AffineCover.instDecidableEqDecisionTreeData.decEq {m✝ : ℕ} (x✝ x✝¹ : DecisionTreeData m✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Utilities.Certificate.AffineCover.instDecidableEqDecisionTreeData {m✝ : ℕ} : DecidableEq (DecisionTreeData m✝)

Equations

• Utilities.Certificate.AffineCover.instDecidableEqDecisionTreeData = Utilities.Certificate.AffineCover.instDecidableEqDecisionTreeData.decEq

def Utilities.Certificate.AffineCover.DecisionTreeData.ValidActive {m : ℕ} (cones : List (List (AffineForm m))) (active : List (AffineForm m)) : DecisionTreeData m → Prop

Validity of a decision tree relative to the affine constraints active at this node.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.AffineCover.DecisionTreeData.ValidActive cones active (Utilities.Certificate.AffineCover.DecisionTreeData.impossible farkas) = farkas.Valid active

def Utilities.Certificate.AffineCover.DecisionTreeData.checkActive {m : ℕ} (cones : List (List (AffineForm m))) (active : List (AffineForm m)) : DecisionTreeData m → Bool

Check active affine constraints at each decision-tree node using Boolean arithmetic.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.AffineCover.DecisionTreeData.checkActive cones active (Utilities.Certificate.AffineCover.DecisionTreeData.impossible farkas) = farkas.check active

def Utilities.Certificate.AffineCover.DecisionTreeData.Valid {m : ℕ} (data : DecisionTreeData m) (base : List (AffineForm m)) (cones : List (List (AffineForm m))) : Prop

Mathematical validity of wall-decision data at the displayed base rows.

Equations

• data.Valid base cones = Utilities.Certificate.AffineCover.DecisionTreeData.ValidActive cones base data

def Utilities.Certificate.AffineCover.DecisionTreeData.check {m : ℕ} (data : DecisionTreeData m) (base : List (AffineForm m)) (cones : List (List (AffineForm m))) : Bool

Executable exact replay of wall-decision data.

Equations

• data.check base cones = Utilities.Certificate.AffineCover.DecisionTreeData.checkActive cones base data

@[simp]

theorem Utilities.Certificate.AffineCover.DecisionTreeData.check_branch {m : ℕ} (form : AffineForm m) (holds fails : DecisionTreeData m) (active : List (AffineForm m)) (cones : List (List (AffineForm m))) : (branch form holds fails).check active cones = (holds.check (active ++ [form]) cones && fails.check (active ++ [form.violation]) cones)

Public one-step reduction rule, allowing large generated trees to cache checked subtrees in separate modules instead of reducing the whole tree in one kernel invocation.

@[simp]

theorem Utilities.Certificate.AffineCover.DecisionTreeData.check_eq_true_iff {m : ℕ} (data : DecisionTreeData m) (base : List (AffineForm m)) (cones : List (List (AffineForm m))) : data.check base cones = true ↔ data.Valid base cones

theorem Utilities.Certificate.AffineCover.DecisionTreeData.covers_of_check_eq_true {m : ℕ} (data : DecisionTreeData m) (base : List (AffineForm m)) (cones : List (List (AffineForm m))) (hCheck : data.check base cones = true) : Covers base cones

Accepted wall-decision data proves that the advertised cones cover the base region at every integral point.

theorem Utilities.Certificate.AffineCover.DecisionTreeData.exists_index_of_check_eq_true {m : ℕ} (data : DecisionTreeData m) (base : List (AffineForm m)) (cones : List (List (AffineForm m))) (hCheck : data.check base cones = true) (point : Fin m → ℤ) (hBase : FormsHold base point) : ∃ cone < cones.length, FormsHold (CoverTree.coneAt cones cone) point

Indexed form of covers_of_check_eq_true, for consumers whose semantic payload is stored in a list parallel to the advertised cones.