dechenzhang/valg-ml-theory-agent/proof-sketch

Proof Sketch

Use this internal skill as the split workflow's proof-roadmap and proof-sketch stage before step-level proof writing.

Contract

Required inputs:

• perspective_M/idea_N/setting.md
• perspective_M/idea_N/proof_tracker.md

Optional inputs:

• perspective_M/idea_N/idea.md
• LITERATURE_SURVEY.md
• theory_tracker.md
• perspective_M/idea_N/technical_survey.md
• latest perspective_M/idea_N/proof_sketch.md when repairing the current sketch
• prior same-perspective idea_K/{setting.md, technical_survey.md, proof_review.md} artifacts
• triggering proof_sketch_review.md, global_proof.md, global_proof_review.md, proof_steps/<Step ID>/review.md, or final proof_review.md when rerunning after a loop route
• controller-provided retry mode: revise_sketch

Outputs:

• perspective_M/idea_N/proof_sketch.md
• optionally perspective_M/idea_N/technical_survey.md

Do not write step proofs, step reviews, final latex_template/, trackers, worker logs, or accepted results.

Internal Constants

• SEARCH_MODE = OPEN

SEARCH_MODE is internal to /proof-sketch, not a public controller argument.

SEARCH_MODE = CLOSE means no direct web search and no use of externally derived artifacts such as LITERATURE_SURVEY.md or any technical_survey.md. Branch-local tracker history, the latest sketch, and triggering review artifacts may still be used.

Responsibilities

• Select or repair a proof roadmap for the exact formalized setting and goal.
• Build or update technical_survey.md only for idea-local proof techniques and framework search.
• Convert the selected roadmap into explicit, lemma-sized sketch steps.
• Expose high-risk proof obligations as steps rather than broad prose.
• Record blockers honestly when no viable sketch exists.

Workflow

1. Read setting.md and identify whether the branch is in exact-goal mode or target-spec mode.
2. Read proof_tracker.md and prior same-perspective failures as sketch-roadmap memory, not authority.
3. Determine retry mode from the controller prompt or triggering artifact. Use revise_sketch for sketch-review REVISE_SKETCH, global-proof-review REVISE_SKETCH, step-review REVISE_SKETCH, or final PROOF_SKETCH_FLAW; otherwise treat this as an initial sketch attempt.
4. If SEARCH_MODE = OPEN and search context is available, create, reuse, or extend technical_survey.md using the technical survey rules below.
5. Select or repair a proof roadmap according to retry mode.
6. If the setting, goal, user request, or target-spec exposes quantitative dependence, define the theorem's rate objective before splitting steps. Classify it as fixed-time, fixed-horizon, horizon-uniform, structural-parameter explicit, confidence-explicit, regularity-explicit, numerical-error explicit, or another domain-appropriate explicit-dependence mode named from the setting. If the setting, goal, user request, triggering review, or prior same-perspective branch exposes a baseline invariance obligation, identify the inherited recovery, reduction, specialization, zero-defect, exact-limit, exact/noiseless, or baseline-case conclusion and localize the bridge that preserves it.
7. Apply the shared Assumption Provenance Contract, Exported Interface Feasibility Gate, Residual-To-Target Adequacy Gate, Scope-Accumulation Compatibility Gate, Noncircular Closure Gate, Entry-State / Activation Trace Gate, and Generated Output Flow Gate from ../_shared/checklists/artifact-contracts.md. Identify every generated-object, event, local-validity, stability, boundedness, recurrence, or invariant fact needed by the roadmap, and decide whether it is a primitive condition, a derived invariant to be proved, or a local conditional hypothesis. For every theorem-critical output target consumed downstream, record the raw controls available before export, exact exported interface, defect terms to dominate or transfer, which defects are controlled by which parameter/event/source, required dominance or transfer relation, source of any threshold or positive margin, producer-consumer path, and object-target compatibility when the output depends on an initialization, entry, reference, population, no-error, or baseline object, including residual-to-target adequacy for any same-target bridge when the produced object is transformed, weighted, preconditioned, whitened, reference-operator-modified, or otherwise surrogate relative to the consumed target, or record a blocker. For every theorem-critical generated condition, recurrence, invariant, stability, boundedness, membership, convergence, or quantitative specialization that must hold across a repeated, iterated, recursive, limiting, or otherwise accumulated scope, record the controlled quantity, local interface or recurrence, accumulated defect or forcing term, sign status, accumulation behavior, closure mechanism, mechanism source, concrete budget/potential or mechanism-specific control relation, one-step charge/absorption/potential-drop, preservation, projection, coupling, stopping, or conditioning relation, finite-budget or declared-scope validity justification, and noncircular closure status when applicable, or record a blocker. For theorem-critical recursive, iterative, descent, contraction, convergence, all-time, recurrence closure, invariant, basin/support, mode-conversion, or exact/noiseless specialization claims, record an entry-state / first-update stress result when applicable, or record a blocker. For every theorem-facing generated output consumed downstream, record its producer, consumers, final theorem use, dependency path, and object-target compatibility when an entry, reference, population, no-error, or baseline object is consumed, including residual-to-target adequacy for same-target bridges from transformed or surrogate produced objects, or record a blocker.
8. Split the roadmap into stable Step IDs such as step_001, each with an exact intended claim, dependencies, assumptions used by stable setting.md assumption ids, technical challenge, proof tool or cited result, output target, rate objective when the step is rate-bearing, and Review status = PENDING.
9. Check that the dependency graph is acyclic and that every dependency points only to an earlier step.
10. Write proof_sketch.md using ../_shared/templates/proof-sketch.md.

Technical Survey Rules

Use technical_survey.md only for idea-local proof-technique and framework search. Do not use this stage to revise LITERATURE_SURVEY.md, change the approved perspective, or reopen upstream gap selection.

• If SEARCH_MODE = OPEN and no usable technical_survey.md exists, create it from ../_shared/templates/technical-survey.md.
• If technical_survey.md exists, update and reuse it rather than rewriting it from scratch unless entries are obsolete.
• Candidate framework sources are relevant papers from LITERATURE_SURVEY.md, current-idea parent foundation papers or transfer-map notes, prior same-perspective technical_survey.md artifacts, and focused theory-only web search scoped to the current formalized setting and goal when existing context is too sparse or too coarse.
• On later sketch attempts, extend technical_survey.md only when prior failures show current frameworks are exhausted, too coarse, or missing technical tools needed for repair.
• When reading new papers, search results, or prior artifacts, extract only proof frameworks, reusable lemmas, reductions, assumptions, transfer challenges, and repair tools relevant to the current branch.
• ## Current Idea Branch must record the current perspective, current idea, and a setting/goal summary consistent with setting.md.
• Each candidate framework must be one concrete proof framework, not a loose paper summary or a merged set of unrelated approaches.
• Source papers must contain traceable provenance only: concrete paper titles, concrete bibliographic identifiers, or explicit prior same-perspective artifact paths such as perspective_M/idea_K/technical_survey.md.
• Do not use generic placeholders in Source papers; generic technique descriptions belong in Key lemmas / ingredients, Main transfer challenges, or Potential repair techniques and supporting references.
• Applicability to current branch must explain why the framework is close to or far from the current setting and goal, plus the remaining adaptation burden.
• Proof roadmap items must state the item goal, earlier-item dependencies, and assumptions used.
• If the current idea.md names parent foundation papers, prefer frameworks that inherit from those parents. If the selected framework switches parents, explain why in Branch notes.
• Keep at most one framework marked selected. Mark other viable alternatives as backup and unsuitable ones as rejected.
• Do not leave a framework marked selected unless its Source papers field is traceable. If provenance is missing but the framework may still be useful, downgrade it to backup.
• For each framework, record key reusable lemmas or ingredients, main transfer challenges, and potential repair tools. Each important repair tool needs a concrete supporting reference and a short explanation of why it may help.
• Branch notes must record why the framework was selected, deferred, or rejected, including lessons from prior failures when relevant.
• Deduplicate repeated papers and repeated frameworks.

Proof Roadmap Selection Rules

A proof roadmap is a refined plan for the formalized goal, not a final proof.