Lemma-Calc: mechanically CALCULATE the forced auxiliary lemma from a stuck
--explain residual goal (UntranslatedGoal). A pure function of the goal
and the induction hypothesis — no enumeration, no search, no solver. Every
step is deterministic; anything that is not forced is an HONEST DECLINE
(CalcVerdict::Decline) with a named reason. The result feeds the same VM
sample-check + candidate renderer as the raw residual (--explain in
src/main/commands.rs); on decline the caller falls back to the raw
candidate, so the calculator only ever ADDS a stronger lemma, never removes
information.
aver proof --explain: Lean goal JSON → ast::Expr (the bilingual-out
layer). This is the INVERSE of the Aver → Lean expression translator
(super::expr), defined ONLY on the closed grammar of Expr shapes our own
emitter produces: literals, BinOp arithmetic/comparisons, Eq claims,
module-qualified function calls, and ∀-binders. Anything outside that
grammar — a match, a lambda, a bare projection, a constructor, an
unrecognised head constant — is an HONEST DECLINE (EngineGap), never a
guess: the caller renders it as an “engine-form gap” verdict rather than a
misleading candidate law.
The marker every Lean runtime panic prints into captured build output.
Empirically pinned against real lake build transcripts (both panic
sites below produce it):
Panic message baked into every fuel wrapper’s exhaustion arm. This is a
SOUNDNESS marker, not just a diagnostic: Lean’s panic! does NOT abort
evaluation — it prints PANIC at … <this message> and returns the type’s
default value, so under native_decide an exhausted-fuel sample reduces
both sides of a model-vs-model equation to default and the kernel
certifies a vacuous (possibly FALSE) equality with lake still exiting 0.
aver proof --check therefore scans captured lake output for panic lines
(crate::codegen::lean::count_model_panic_lines) and treats any hit as
a hard check failure. The scan keys on Lean’s generic PANIC at line
marker — every prelude panic! site shares the vacuity vector, not just
this one — so this constant is purely the emission message; changing it
cannot blind the gate.
aver proof --explain residual probe — turns an emitted main law theorem’s
source lines into a normalization-only twin so Lean reports its residual
(unsolved goals). Used by the --check harness in the aver binary.
aver proof --explain residual probe: turn an emitted main law theorem’s
source lines into a normalization-only twin so Lean reports its residual
(unsolved goals). Re-exported up to codegen::lean for the --check
harness in the aver binary; see induction::residual_probe_body.
aver proof --explain residual probe. Given the EMITTED Lean source lines of
ONE main law theorem (the theorem … := by line through its last arm), render
a NORMALIZATION-ONLY twin whose body strips the closing tactic cascade so
Lean’s elaborator reports the law’s residual (unsolved goals) instead of
closing it with sorry/omega/split. The leftover goal IS what a
Lemma-Calculation agent applies the IH against, so the cons arm’s IH must stay
in canonical recursive form: each arm is replaced by (try simp only [<the theorem's own def simp set>, List.cons_append]) — def-unfold + cons-peel ONLY,
no done/omega/split/simp_all/| sorry.
aver proof --explain residual probe — turns an emitted main law theorem’s
source lines into a normalization-only twin so Lean reports its residual
(unsolved goals). Used by the --check harness in the aver binary.
aver proof --explain residual probe: turn an emitted main law theorem’s
source lines into a normalization-only twin so Lean reports its residual
(unsolved goals). Re-exported up to codegen::lean for the --check
harness in the aver binary; see induction::residual_probe_body.
Like residual_probe_body, but when dump_label is Some(fn.law) each
normalization-only arm is followed by (try aver_dump_goal "<fn.law>") — the
second, fail-soft --explain stage that serialises the residual goal to JSON
via the info log (see codegen::lean::untranslate::AVER_DUMP_GOAL_ELAB). The
try keeps a dump/elaboration failure from disturbing the arm, so a broken
dump degrades to “no JSON for this law”, never a corrupted probe.