Kernel-checked affine covering certificates

This module is the arithmetic trust boundary for the external cone-covering kernel. An affine form has integral coefficients and is evaluated only on an integral point. A cone is a finite conjunction of inequalities a(x) >= 0.

The external program may emit a passive contradiction tree. Branching on a form a adds its exact integral complement

-a(x) - 1 >= 0.

Leaves carry sparse rational Farkas multipliers. The executable checker verifies their signs, the vanishing of every variable coefficient, and a strictly negative constant sum. The soundness theorem proves that an accepted tree covers every integral point of the advertised base region by at least one advertised cone. No linear-programming algorithm is trusted or implemented here.

Row numbering agrees directly with the external C emitter: base-region rows come first, followed by asserted violation rows in root-to-leaf branch order. Thus a branch extends the active row list by appending its violation, rather than prepending it.

This layer deliberately gives no graph, subdivision, or divisor semantics to the cones. Those belong in a separate local-certificate checker.

Proof-free finite Boolean folds

def Utilities.Certificate.AffineCover.allFin {k : ℕ} (test : Fin k → Bool) : Bool

Boolean universal quantification over Fin k, implemented as a list fold rather than a proof-producing Decidable computation.

Equations

• Utilities.Certificate.AffineCover.allFin test = (List.ofFn test).all id

@[simp]

theorem Utilities.Certificate.AffineCover.allFin_eq_true_iff {k : ℕ} (test : Fin k → Bool) : allFin test = true ↔ ∀ (index : Fin k), test index = true

def Utilities.Certificate.AffineCover.allFinset {α : Type u_1} (elements : Finset α) (test : α → Bool) : Bool

Boolean universal quantification over an arbitrary finite set. Finset.fold keeps kernel evaluation proof-free even when the element type itself is a finite combinatorial object such as Finset (Fin n).

Equations

• Utilities.Certificate.AffineCover.allFinset elements test = Finset.fold (fun (left right : Bool) => left && right) true test elements

@[simp]

theorem Utilities.Certificate.AffineCover.allFinset_eq_true_iff {α : Type u_1} (elements : Finset α) (test : α → Bool) : allFinset elements test = true ↔ ∀ element ∈ elements, test element = true

structure Utilities.Certificate.AffineCover.AffineForm (m : ℕ) : Type

An integral affine form in m variables.

• fixedValue : ℤ

  The integer constant term of the affine form.

• coefficient : Fin m → ℤ

  The integer coefficient of each of the m coordinates.

@[instance_reducible]

instance Utilities.Certificate.AffineCover.instDecidableEqAffineForm {m✝ : ℕ} : DecidableEq (AffineForm m✝)

Equations

• Utilities.Certificate.AffineCover.instDecidableEqAffineForm = Utilities.Certificate.AffineCover.instDecidableEqAffineForm.decEq

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

Equations

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

@[instance_reducible]

instance Utilities.Certificate.AffineCover.AffineForm.instZero {m : ℕ} : Zero (AffineForm m)

Equations

• Utilities.Certificate.AffineCover.AffineForm.instZero = { zero := { fixedValue := 0, coefficient := fun (x : Fin m) => 0 } }

def Utilities.Certificate.AffineCover.AffineForm.equal {m : ℕ} (left right : AffineForm m) : Bool

Proof-free extensional equality for integral affine forms. In particular, this avoids asking Decidable to construct an equality proof between two function-valued coefficient fields while a large generated certificate is being reduced by the kernel.

Equations

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

@[simp]

theorem Utilities.Certificate.AffineCover.AffineForm.equal_eq_true_iff {m : ℕ} (left right : AffineForm m) : left.equal right = true ↔ left = right

def Utilities.Certificate.AffineCover.AffineForm.mem {m : ℕ} (form : AffineForm m) (forms : List (AffineForm m)) : Bool

Proof-free list membership for integral affine forms.

Equations

• form.mem forms = forms.any fun (candidate : Utilities.Certificate.AffineCover.AffineForm m) => form.equal candidate

@[simp]

theorem Utilities.Certificate.AffineCover.AffineForm.mem_eq_true_iff {m : ℕ} (form : AffineForm m) (forms : List (AffineForm m)) : form.mem forms = true ↔ form ∈ forms

def Utilities.Certificate.AffineCover.AffineForm.eval {m : ℕ} (form : AffineForm m) (point : Fin m → ℤ) : ℤ

Evaluation of an integral affine form at an integral point.

Equations

• form.eval point = form.fixedValue + ∑ i : Fin m, form.coefficient i * point i

def Utilities.Certificate.AffineCover.AffineForm.Holds {m : ℕ} (form : AffineForm m) (point : Fin m → ℤ) : Prop

The closed integral inequality represented by an affine form.

Equations

• form.Holds point = (0 ≤ form.eval point)

def Utilities.Certificate.AffineCover.AffineForm.violation {m : ℕ} (form : AffineForm m) : AffineForm m

The exact closed complement of form.Holds on integral points.

If a(x) >= 0 fails and a(x) is integral, then a(x) <= -1, equivalently -a(x)-1 >= 0.

Equations

• form.violation = { fixedValue := -form.fixedValue - 1, coefficient := fun (i : Fin m) => -form.coefficient i }

@[simp]

theorem Utilities.Certificate.AffineCover.AffineForm.eval_zero {m : ℕ} (point : Fin m → ℤ) : eval 0 point = 0

@[simp]

theorem Utilities.Certificate.AffineCover.AffineForm.eval_violation {m : ℕ} (form : AffineForm m) (point : Fin m → ℤ) : form.violation.eval point = -form.eval point - 1

@[simp]

theorem Utilities.Certificate.AffineCover.AffineForm.holds_violation_iff_not {m : ℕ} (form : AffineForm m) (point : Fin m → ℤ) : form.violation.Holds point ↔ ¬form.Holds point

def Utilities.Certificate.AffineCover.AffineForm.evalRat {m : ℕ} (form : AffineForm m) (point : Fin m → ℤ) : ℚ

Rational evaluation, used only in the proof of Farkas soundness.

Equations

• form.evalRat point = ↑form.fixedValue + ∑ i : Fin m, ↑(form.coefficient i) * ↑(point i)

@[simp]

theorem Utilities.Certificate.AffineCover.AffineForm.evalRat_eq_cast_eval {m : ℕ} (form : AffineForm m) (point : Fin m → ℤ) : form.evalRat point = ↑(form.eval point)

def Utilities.Certificate.AffineCover.FormsHold {m : ℕ} (forms : List (AffineForm m)) (point : Fin m → ℤ) : Prop

A finite conjunction of affine inequalities. This is used for base regions and for individual proof cones.

Equations

• Utilities.Certificate.AffineCover.FormsHold forms point = ∀ form ∈ forms, form.Holds point

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

A family of cones covers a base region at every integral point.

Equations

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

structure Utilities.Certificate.AffineCover.FarkasTerm : Type

One sparse rational multiplier names a row of the current region.

• row : ℕ

  The index of the active affine row used by this sparse Farkas term.

• weight : ℚ

  The proposed rational multiplier of the selected affine row; its admissibility is checked by the validity predicate.

def Utilities.Certificate.AffineCover.instDecidableEqFarkasTerm.decEq (x✝ x✝¹ : FarkasTerm) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Utilities.Certificate.AffineCover.instDecidableEqFarkasTerm : DecidableEq FarkasTerm

Equations

• Utilities.Certificate.AffineCover.instDecidableEqFarkasTerm = Utilities.Certificate.AffineCover.instDecidableEqFarkasTerm.decEq

@[instance_reducible]

instance Utilities.Certificate.AffineCover.instReprFarkasTerm : Repr FarkasTerm

Equations

• Utilities.Certificate.AffineCover.instReprFarkasTerm = { reprPrec := Utilities.Certificate.AffineCover.instReprFarkasTerm.repr }

def Utilities.Certificate.AffineCover.instReprFarkasTerm.repr : FarkasTerm → ℕ → Std.Format

Equations

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

structure Utilities.Certificate.AffineCover.FarkasData : Type

Passive sparse Farkas data. Repeated row indices are permitted.

• terms : List FarkasTerm

  The ordered sparse row multipliers of the proposed Farkas combination; repeated indices are allowed.

def Utilities.Certificate.AffineCover.instDecidableEqFarkasData.decEq (x✝ x✝¹ : FarkasData) : Decidable (x✝ = x✝¹)

Equations

• Utilities.Certificate.AffineCover.instDecidableEqFarkasData.decEq { terms := a } { terms := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Utilities.Certificate.AffineCover.instDecidableEqFarkasData : DecidableEq FarkasData

Equations

• Utilities.Certificate.AffineCover.instDecidableEqFarkasData = Utilities.Certificate.AffineCover.instDecidableEqFarkasData.decEq

@[instance_reducible]

instance Utilities.Certificate.AffineCover.instReprFarkasData : Repr FarkasData

Equations

• Utilities.Certificate.AffineCover.instReprFarkasData = { reprPrec := Utilities.Certificate.AffineCover.instReprFarkasData.repr }

def Utilities.Certificate.AffineCover.instReprFarkasData.repr : FarkasData → ℕ → Std.Format

Equations

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

def Utilities.Certificate.AffineCover.FarkasData.rowAt {m : ℕ} (rows : List (AffineForm m)) (index : ℕ) : AffineForm m

Look up an affine row, returning the zero form when the index is out of range.

Equations

• Utilities.Certificate.AffineCover.FarkasData.rowAt rows index = rows.getD index 0

def Utilities.Certificate.AffineCover.FarkasData.constantSum {m : ℕ} (data : FarkasData) (rows : List (AffineForm m)) : ℚ

Sum of the constant coefficients in the proposed Farkas combination.

Equations

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

def Utilities.Certificate.AffineCover.FarkasData.coefficientSum {m : ℕ} (data : FarkasData) (rows : List (AffineForm m)) (coordinate : Fin m) : ℚ

Sum of one variable coefficient in the proposed Farkas combination.

Equations

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

def Utilities.Certificate.AffineCover.FarkasData.Valid {m : ℕ} (data : FarkasData) (rows : List (AffineForm m)) : Prop

Mathematical validity of sparse Farkas data for the displayed rows.

Equations

• data.Valid rows = ((∀ term ∈ data.terms, term.row < rows.length ∧ 0 ≤ term.weight) ∧ (∀ (coordinate : Fin m), data.coefficientSum rows coordinate = 0) ∧ data.constantSum rows < 0)

def Utilities.Certificate.AffineCover.FarkasData.integralWeights (data : FarkasData) : Bool

Whether every sparse multiplier is integral. External emitters may always clear denominators within one homogeneous Farkas contradiction.

Equations

• data.integralWeights = data.terms.all fun (term : Utilities.Certificate.AffineCover.FarkasTerm) => decide (term.weight.den = 1)

@[simp]

theorem Utilities.Certificate.AffineCover.FarkasData.integralWeights_eq_true_iff (data : FarkasData) : data.integralWeights = true ↔ ∀ term ∈ data.terms, term.weight.den = 1

def Utilities.Certificate.AffineCover.FarkasData.coefficientSumInt {m : ℕ} (data : FarkasData) (rows : List (AffineForm m)) (coordinate : Fin m) : ℤ

Integer coefficient sum used by the kernel-reduction fast path.

Equations

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

def Utilities.Certificate.AffineCover.FarkasData.constantSumInt {m : ℕ} (data : FarkasData) (rows : List (AffineForm m)) : ℤ

Integer constant sum used by the kernel-reduction fast path.

Equations

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

def Utilities.Certificate.AffineCover.FarkasData.integralCheck {m : ℕ} (data : FarkasData) (rows : List (AffineForm m)) : Bool

Proof-free arithmetic replay for a leaf whose multipliers have denominator one. Unlike rational multiplication and addition, these integer operations are transparent to ordinary kernel reduction.

Equations

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

def Utilities.Certificate.AffineCover.FarkasData.rationalCheck {m : ℕ} (data : FarkasData) (rows : List (AffineForm m)) : Bool

General rational checker retained as the fallback for hand-written or legacy certificates whose denominators have not been cleared.

Equations

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

def Utilities.Certificate.AffineCover.FarkasData.check {m : ℕ} (data : FarkasData) (rows : List (AffineForm m)) : Bool

Executable exact checker for a Farkas leaf. Integral multipliers take a kernel-transparent fast path; arbitrary rationals retain the original exact checker.

Equations

• data.check rows = match data.integralWeights with | true => data.integralCheck rows | false => data.rationalCheck rows

@[simp]

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

theorem Utilities.Certificate.AffineCover.FarkasData.not_formsHold_of_valid {m : ℕ} (data : FarkasData) (rows : List (AffineForm m)) {point : Fin m → ℤ} (hValid : data.Valid rows) : ¬FormsHold rows point

A valid Farkas leaf proves that its current affine region is empty.

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

Passive contradiction tree emitted by an external covering search.

branch cone arity children has one child for every form of the named cone; the checker adds that form's exact integral violation in the corresponding child. skip mirrors the external kernel's shared-form compression, while empty closes immediately when one advertised cone has no inequalities.

Active rows are ordered exactly as the C certificate numbers them: the base rows first, then branch violations appended in root-to-leaf order.

• leaf {m : ℕ} (farkas : FarkasData) : CoverTree m
• empty {m : ℕ} (cone : ℕ) : CoverTree m
• skip {m : ℕ} (cone form : ℕ) (next : CoverTree m) : CoverTree m
• branch {m : ℕ} (cone arity : ℕ) (children : Fin arity → CoverTree m) : CoverTree m

def Utilities.Certificate.AffineCover.CoverTree.coneAt {m : ℕ} (cones : List (List (AffineForm m))) (index : ℕ) : List (AffineForm m)

Look up a cone in the cover table, returning an empty cone for an out-of-range index.

Equations

• Utilities.Certificate.AffineCover.CoverTree.coneAt cones index = cones.getD index []

def Utilities.Certificate.AffineCover.CoverTree.formAt {m : ℕ} (cone : List (AffineForm m)) (index : ℕ) : AffineForm m

Look up an affine constraint in a cone, returning the zero form for an out-of-range index.

Equations

• Utilities.Certificate.AffineCover.CoverTree.formAt cone index = cone.getD index 0

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

Mathematical validity of a contradiction tree under the currently active affine rows.

Equations

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

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

Recursive Boolean replay of a contradiction tree under active rows.

Equations

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

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

Executable exact checker for a complete covering tree.

Equations

• tree.check base cones = Utilities.Certificate.AffineCover.CoverTree.checkActive cones base tree

@[simp]

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

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

Soundness of the passive checker: an accepted contradiction tree proves integral coverage of the base region by the advertised union of cones.

Proof-carrying cone reduction

The search layer is allowed to delete an inequality from a local proof cone when that inequality follows from the base region and the other inequalities still present at that stage. This can make the global covering tree orders of magnitude smaller. It must not, however, enlarge the trusted interface.

Every deletion therefore carries a Farkas contradiction for

base ++ remaining ++ [violation removed].

The checker below replays those contradictions. Its soundness theorem runs the deletion chain backwards: the final reduced cone implies the last deleted row, then the preceding row, and eventually the complete original local cone.

structure Utilities.Certificate.AffineCover.ReductionStep (m : ℕ) : Type

Passive data for one proof-carrying deletion from a cone.

• removed : AffineForm m

  The affine row proposed for deletion from the current cone.

• farkas : FarkasData

  The Farkas data intended to certify that deleting this row preserves the required implication.

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

Equations

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

@[instance_reducible]

instance Utilities.Certificate.AffineCover.instDecidableEqReductionStep {m✝ : ℕ} : DecidableEq (ReductionStep m✝)

Equations

• Utilities.Certificate.AffineCover.instDecidableEqReductionStep = Utilities.Certificate.AffineCover.instDecidableEqReductionStep.decEq

structure Utilities.Certificate.AffineCover.ReductionChain (m : ℕ) : Type

A sequence of row deletions used to reduce a local proof cone.

• steps : List (ReductionStep m)

  The ordered row-deletion steps of the reduction, each carrying its proposed Farkas justification.

@[instance_reducible]

instance Utilities.Certificate.AffineCover.instDecidableEqReductionChain {m✝ : ℕ} : DecidableEq (ReductionChain m✝)

Equations

• Utilities.Certificate.AffineCover.instDecidableEqReductionChain = Utilities.Certificate.AffineCover.instDecidableEqReductionChain.decEq

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

Equations

• Utilities.Certificate.AffineCover.instDecidableEqReductionChain.decEq { steps := a } { steps := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Utilities.Certificate.AffineCover.ReductionChain.resultRows {m : ℕ} : List (AffineForm m) → List (ReductionStep m) → Option (List (AffineForm m))

The cone left after applying all named deletions. A missing row makes the chain structurally invalid and returns none.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.AffineCover.ReductionChain.resultRows x✝ [] = some x✝

def Utilities.Certificate.AffineCover.ReductionChain.ValidRows {m : ℕ} (base : List (AffineForm m)) : List (AffineForm m) → List (ReductionStep m) → Prop

Mathematical validity of rows deleted in the exact forward order in which they disappear from the cone.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.AffineCover.ReductionChain.ValidRows base x✝ [] = True

def Utilities.Certificate.AffineCover.ReductionChain.Valid {m : ℕ} (chain : ReductionChain m) (base full : List (AffineForm m)) : Prop

Mathematical validity of every deletion in a chain.

Equations

• chain.Valid base full = Utilities.Certificate.AffineCover.ReductionChain.ValidRows base full chain.steps

def Utilities.Certificate.AffineCover.ReductionChain.checkRows {m : ℕ} (base reduced : List (AffineForm m)) : List (AffineForm m) → List (ReductionStep m) → Bool

Boolean replay of row deletions from rows down to the claimed result.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.AffineCover.ReductionChain.checkRows base reduced x✝ [] = decide (x✝ = reduced)

def Utilities.Certificate.AffineCover.ReductionChain.check {m : ℕ} (chain : ReductionChain m) (base full reduced : List (AffineForm m)) : Bool

Executable exact replay of a reduction chain, including its claimed final reduced cone.

Equations

• chain.check base full reduced = Utilities.Certificate.AffineCover.ReductionChain.checkRows base reduced full chain.steps

@[simp]

theorem Utilities.Certificate.AffineCover.ReductionChain.check_eq_true_iff {m : ℕ} (chain : ReductionChain m) (base full reduced : List (AffineForm m)) : chain.check base full reduced = true ↔ chain.Valid base full ∧ resultRows full chain.steps = some reduced

theorem Utilities.Certificate.AffineCover.ReductionChain.formsHold_full_of_valid {m : ℕ} (chain : ReductionChain m) (base full reduced : List (AffineForm m)) (hValid : chain.Valid base full) (hResult : resultRows full chain.steps = some reduced) (point : Fin m → ℤ) (hBase : FormsHold base point) (hReduced : FormsHold reduced point) : FormsHold full point

Soundness of a valid deletion chain: if the final rows hold in the base region, then every row of the original local proof cone holds.

theorem Utilities.Certificate.AffineCover.ReductionChain.formsHold_full_of_check_eq_true {m : ℕ} (chain : ReductionChain m) (base full reduced : List (AffineForm m)) (hCheck : chain.check base full reduced = true) (point : Fin m → ℤ) (hBase : FormsHold base point) (hReduced : FormsHold reduced point) : FormsHold full point

A successful Boolean reduction replay proves the semantic implication from the reduced search cone back to the full local proof cone.

Small closed examples

def Utilities.Certificate.AffineCover.Examples.form1 (fixedValue a : ℤ) : AffineForm 1

The affine form constant + a*x.

Equations

• Utilities.Certificate.AffineCover.Examples.form1 fixedValue a = { fixedValue := fixedValue, coefficient := ![a] }

def Utilities.Certificate.AffineCover.Examples.form2 (fixedValue a b : ℤ) : AffineForm 2

The affine form constant + a*x + b*y.

Equations

• Utilities.Certificate.AffineCover.Examples.form2 fixedValue a b = { fixedValue := fixedValue, coefficient := ![a, b] }

def Utilities.Certificate.AffineCover.Examples.strictPartitionCones : List (List (AffineForm 2))

The two cones x-y >= 1 and y-x >= 0. Their use of constants -1 and 0 is the strict integer partition required by the C kernel grammar.

Equations

• Utilities.Certificate.AffineCover.Examples.strictPartitionCones = [[Utilities.Certificate.AffineCover.Examples.form2 (-1) 1 (-1)], [Utilities.Certificate.AffineCover.Examples.form2 0 (-1) 1]]

def Utilities.Certificate.AffineCover.Examples.strictPartitionTree : CoverTree 2

If both one-row cones were violated, the active rows would be x-y-1 >= 0 and y-x >= 0; adding them gives -1 >= 0.

Equations

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

theorem Utilities.Certificate.AffineCover.Examples.strictPartitionTree_check : strictPartitionTree.check [] strictPartitionCones = true

theorem Utilities.Certificate.AffineCover.Examples.strictPartitionCovers : Covers [] strictPartitionCones

Kernel-checked exact coverage of every integral pair by the strict partition x-y >= 1 or y-x >= 0.

theorem Utilities.Certificate.AffineCover.Examples.strictPartition (x y : ℤ) : x - y ≥ 1 ∨ y - x ≥ 0

A direct human-readable specialization of strictPartitionCovers.

The base row x - 1 >= 0 implies the local row x >= 0. The reduction step checks this by contradicting -x - 1 >= 0; adding the two active rows gives the impossible constant -2.

def Utilities.Certificate.AffineCover.Examples.implicationReductionBase : List (AffineForm 1)

The base constraint x - 1 ≥ 0 in the one-variable implication-reduction example.

Equations

• Utilities.Certificate.AffineCover.Examples.implicationReductionBase = [Utilities.Certificate.AffineCover.Examples.form1 (-1) 1]

def Utilities.Certificate.AffineCover.Examples.implicationReductionFull : List (AffineForm 1)

The redundant constraint x ≥ 0 that the example deletes using its stronger base constraint.

Equations

• Utilities.Certificate.AffineCover.Examples.implicationReductionFull = [Utilities.Certificate.AffineCover.Examples.form1 0 1]

def Utilities.Certificate.AffineCover.Examples.implicationReduction : ReductionChain 1

The single-step certificate deleting x ≥ 0, with unit weights on the two contradiction rows.

Equations

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

theorem Utilities.Certificate.AffineCover.Examples.implicationReduction_check : implicationReduction.check implicationReductionBase implicationReductionFull [] = true

theorem Utilities.Certificate.AffineCover.Examples.implicationReduction_sound (x : ℤ) (hx : 1 ≤ x) : 0 ≤ x

The checked reduction really reconstructs its omitted local inequality.