Struct InventoryItem 

pub struct InventoryItem {
    pub kind: ClaimKind,
    pub name: String,
    pub status: ClaimStatus,
    pub finite_enumeration: bool,
    pub domain_bound: Option<String>,
    pub counterexample: Option<String>,
    pub vacuous: bool,
    pub proof: bool,
    pub certificate: Option<TheoremCertificate>,
    pub certificate_rechecks: Option<bool>,
}

ONE classified claim in the inventory.

Fields

kind: ClaimKind

name: String

The claim’s identity (the test’s prose name, or the theorem/axiom name).

status: ClaimStatus

finite_enumeration: bool

True when the claim was established by FINITE testing (an example, or a finite-enumeration property/bounded theorem) rather than an unbounded mathematical argument. The disclosure that keeps green from meaning “unbounded proof”.

domain_bound: Option<String>

The disclosed finite bound (integers sampled over [-1000, 1000], the exhausted boolean space, …) — present whenever a bound was actually covered, so a bounded claim can never masquerade as unbounded.

counterexample: Option<String>

A concrete counterexample, when the claim was falsified.

vacuous: bool

True only for the vacuous example — a green that asserted nothing.

proof: bool

Whether this item is an actual PROOF: true ONLY for a kernel-certified theorem. An example, a finite-enumeration property (even one exhausted over booleans), an axiom, and an admitted assumption are all false — finite testing and admitted premises are never unrestricted proofs.

certificate: Option<TheoremCertificate>

The independently re-checkable proof certificate — the kernel proof term, the goal it proves, and the theorem’s disclosed premises. Present ONLY on a proof: true theorem: a third party can re-verify it against the kernel WITHOUT trusting the prover. Never present on an axiom/assumption (an assumption is not a proof), a finite-enumeration item, or an unproved theorem.

certificate_rechecks: Option<bool>

Whether the carried certificate RE-CHECKS via the independent kernel checker (type-checking the term to the claimed goal, not re-running the prover). Some(true) on a certificate that re-verifies; None when there is no certificate to check. A proof: true theorem whose certificate does NOT re-check is a soundness alarm the consumer must treat as a failure.

Trait Implementations

impl Clone for InventoryItem

fn clone(&self) -> InventoryItem

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for InventoryItem

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

Formats the value using the given formatter.

impl Serialize for InventoryItem

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.