Enum LemmaProvenance 

pub enum LemmaProvenance {
    Conjectured,
    Enumerated,
    Recognized,
    Calculated,
}

Who PROPOSED a lemma — the ORIGIN axis, orthogonal to the verification STRENGTH axis (the sidecar’s “verified (bounded), kernel proof pending” vs proven header). The proof system has several lemma proposers; each lands on a different point of the discovery-vs-plumbing map, so the artifacts carry the origin honestly instead of letting one proposer’s name (the --discover enumerator) stand in for all of them.

• Conjectured — an agent/LLM generalization, a LEAP into the discovery half of the map.
• Enumerated — the discover blind enumerate + hostile forward-check, a search that LANDS mostly on plumbing.
• Recognized — shape recognizers / bridges, FORCED by the program’s structure → plumbing.
• Calculated — Lemma-Calculation (residual → lemma), FORCED by the stuck goal → plumbing.

Variants

Conjectured

Agent/LLM generalization — a leap into discovery.

Enumerated

The discover blind enumerate + hostile forward-check — a search that lands mostly on plumbing.

Recognized

Shape recognizers / bridges — plumbing forced by structure.

Calculated

Lemma-Calculation (residual → lemma) — plumbing forced by the stuck goal.

Implementations

impl LemmaProvenance

pub fn as_tag(&self) -> &'static str

Stable lowercase tag for rendering and round-trip: "conjectured" / "enumerated" / "recognized" / "calculated".

Trait Implementations

impl Clone for LemmaProvenance

fn clone(&self) -> LemmaProvenance

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for LemmaProvenance

impl Debug for LemmaProvenance

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

Formats the value using the given formatter.

impl Display for LemmaProvenance

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

Formats the value using the given formatter.

impl Eq for LemmaProvenance

impl PartialEq for LemmaProvenance

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for LemmaProvenance