Module lemma_discovery 

Committed-lemma consumption — the proof-side “sink” for auxiliary helper lemmas.

A normal aver proof parses a committed DiscoveredLemmas.lean (hash-gated for staleness via discovery_surface_hash), re-pins each in-scope Induction law to ProofStrategy::SimpOverLemmas(names), and the Lean backend embeds the lemma texts before the law theorem — re-proving them in the same lake build — and simps over their names. So a law that needs an auxiliary lemma closes universally once that lemma is committed in scope. Re-verification in lake build, NOT the hash, is the soundness guard: a stale or hand-edited file is ignored, never trusted.

The committed lemmas are produced EXTERNALLY — by hand or by the Method agent loop (the the-method skill: an agent proposes auxiliary laws, the kernel certifies them) — not by an in-tree enumerator. The brute-force equation enumerator that previously populated DiscoveredLemmas.lean (aver proof --discover / --emit-laws) was removed; its full source is archived at the git tag archive/lemma-discovery-enumerator.

Structs

CommittedLemma

A lemma available to a law’s proof: its theorem name plus Lean text (statement, and for embedded ones the tactic too). Two provenances flow through the same orientation / loop-exclusion / simp-selection machinery:

Enums

LemmaProvenance

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.

SimpDirection

How a committed lemma may join a simp set. Discovery commits equations in enumeration orientation, so usability as a rewrite rule is a property to RECOVER, not assume.

Functions

apply_simp_over_lemma_pins

Apply a plan_simp_over_lemma_pins plan to the lowered IR.

discovery_surface_hash

Staleness key for a committed DiscoveredLemmas.lean: an FNV-1a hash over the sorted signatures of the program’s pure-fn proof surface. A normal aver proof re-pins committed lemmas only when this matches the hash the file was tagged with — a changed surface means the committed lemmas may be stale, so they are ignored (the re-pin behaves exactly as if none existed). The hash gates staleness only; re-verification in lake build is the soundness guard, never the hash.

forbidden_token_in_lemma

Soundness validation for a parsed committed lemma: the embed path writes text VERBATIM into the generated entry root, where lake compiles it as top-level Lean — so a block absorbing anything beyond its own theorem … := by + tactic lines (the parser takes every non-theorem line as-is, and Lean accepts indented top-level commands) could smuggle a declaration like axiom cheat : False into the proof environment. Returns the first forbidden declaration keyword found outside -- line comments (skipping the block’s own leading theorem), or None when the block is clean. The CLI rejects the WHOLE artifact on any hit — a discovery-emitted file never contains these, so a hit means hand-edited or corrupted content that must not join a kernel-trust pipeline. (The axiom WHITELIST in the universal metric is the backstop; this check makes the failure loud and early instead.)

lemma_lhs_fns

Program fns a lemma’s LEFT-HAND SIDE mentions — the rewrite rule’s pattern, projected through lean_index like mentioned_fns. A Forward lemma fires against the consumer goal only through its LHS shape (length (append x y) = plus … matches a goal containing length (append …)), so a sibling whose LHS sits entirely inside the consumer’s proof cone is RELEVANT even when its RHS introduces an out-of-cone combinator (plus) — that combinator’s = a + b bridge is synthesized downstream, and loop safety is handled by simp_entries. Falls back to the whole statement when there is no top-level = (an invariant-shaped lemma, which is inert as a rewrite anyway).

mentioned_fns

Program fns a lemma’s Lean text mentions, projected through lean_index (Lean name → caller-chosen value, e.g. the source name). Token scan over identifier-shaped chunks; builtin lemma names (List.append_assoc, …) and binder names simply miss the index.

parse_committed_lemmas

Parse a committed DiscoveredLemmas.lean into its theorem blocks. A block starts at a column-0 theorem line and runs until the next one (proof lines are indented, so this never splits a tactic). Header comments before the first theorem are dropped; comment/blank lines between theorems are absorbed into the preceding block’s text (harmless Lean comments).

plan_simp_over_lemma_pins

Decide which laws get the committed lemmas. A lemma is in-scope for a law when every program fn its text mentions is inside the law’s proof cone (plus the law’s subject fn) — the same scope discovery enumerated over, so the embedded text can only reference fns already emitted before the law’s theorem. Only laws the lowerer pinned Induction are re-pinned: that is the strategy the discovery cluster (list/Peano homomorphisms) lands on, and the Lean renderer for SimpOverLemmas reuses the same induction ladder, so the swap can only ADD proving power.

simp_entries

Ready-to-emit simp set entries for a pinned lemma selection: a Forward lemma joins as name, a Reversed one as ← name — minus the loop-prone combinations. A Forward rule whose RHS mentions a program fn that some Reversed rule in the SAME set unfolds (its RHS head) would compose into a rewrite cycle — e.g. length (x0 ++ x1) = length (append x0 x1) (forward) against ← ((x0 ++ x1) = append x0 x1) ping-pongs ++ ↔ append under length forever. simp loops are NOT a caught failure: they abort the build with a deterministic maxHeartbeats ERROR that first cannot recover from, so the exclusion is a build-safety requirement, not a quality preference.

simp_orientation

Classify a committed lemma as a usable simp rewrite rule, or None (e.g. a 0 <= … invariant, or an equation connecting nothing to a program fn head). A None lemma stays EMBEDDED (other committed lemmas’ proofs may depend on it) but joins no simp set — a builtin-headed equation used left-to-right re-folds the very structure the induction ladder needs peeled, and loops against the fn’s own def unfold.