Struct LiaCert 

pub struct LiaCert { /* private fields */ }

A refutation of a constraint system, as the multipliers that refute it.

Farkas’ lemma in the form the checker uses: if every λᵢ ≥ 0 and Σ λᵢ·formᵢ is a CONSTANT c with c > 0 — or with c ≥ 0 when some λᵢ > 0 weights a STRICT constraint — then no assignment satisfies every formᵢ ≤ 0 at once, because that assignment would have to make a non-negative combination of non-positive numbers positive.

This is Lean’s Justification flattened. Lean keeps the derivation as a TREE of combo a j b k nodes (Lean/Elab/Tactic/Omega/Core.lean:49) because it must assemble a proof TERM out of combo_sat' applications; a checker that only has to agree with a VERDICT can multiply the tree out into one multiplier per assumption and check a single dot product. Same certificate, one level flatter, and the flattening is what makes the checker fit on a page.

Implementations

impl LiaCert

pub fn multipliers(&self) -> &[BigInt]

The multipliers, in constraint order.

pub fn from_multipliers(multipliers: Vec<BigInt>) -> LiaCert

Build a certificate from raw multipliers — the door a test uses to hand the checker a LIE and require it to be refused. A certificate no mutation can spoil is a certificate nothing is checking.

Trait Implementations

impl Clone for LiaCert

fn clone(&self) -> LiaCert

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for LiaCert

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl PartialEq for LiaCert

fn eq(&self, other: &LiaCert) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for LiaCert

impl StructuralPartialEq for LiaCert