dechenzhang/valg-ml-theory-agent/idea-formalizer

Idea Formalizer

Use this skill to formalize one approved branch-local idea into a theorem-ready setting.md for later theorem proving.

This is the internal formalization skill:

• write perspective_M/idea_N/setting.md
• formalize the approved branch-local idea rather than redesigning it
• do not modify controller-owned routing, tracker-row ownership, or controlled vocabularies

The goal of this skill is to remove ambiguity before proof work. The split proof pipeline should be able to read setting.md and start /proof-sketch without redefining the problem, guessing missing assumptions, or repairing symbol ambiguity.

Use ../_shared/templates/setting.md as the binding artifact structure.

Responsibilities

• Translate idea.md into a formal setting and a formalized goal.
• Keep the formalization aligned with the approved idea instead of inventing a nearby new idea.
• Make assumptions, notation, regime, and goal contract explicit enough for theorem proving, with stable ids for every technical assumption.

Required Inputs

• perspective_M/idea_N/idea.md

Optional Inputs

• workflow_feedback.md
• LITERATURE_SURVEY.md
• other branch-local files under perspective_M/
• current perspective_M/idea_N/setting.md draft when rerunning the formalization checkpoint for the same approved idea_N
• matching pending rerun feedback from workflow_feedback.md for the formalization checkpoint
• previous same-perspective idea_{N-1}/setting.md as a refinement reference when the current idea_N was created after controller-level idea modification
• previous same-perspective idea_{N-1}/proof_review.md as a refinement reference when the current idea_N was created after controller-level idea modification

Required Outputs

• perspective_M/idea_N/setting.md

Workflow

Step 1: Load the current branch context

• Read the exact current perspective_M/idea_N/idea.md.
• Read the Parent foundation papers, Transfer map, Source alignment, Progress type, Materiality, Feasibility, and Consistency entries from idea.md ## Notes as branch-lineage, source-direction, progress-type, and assumption-support guardrails for the formalization.
• If perspective_M/idea_N/setting.md already exists, read it as the latest draft for this branch; this is a same-idea formalization-checkpoint rerun rather than a new idea variant.
• If workflow_feedback.md contains pending rerun feedback for the current branch's Formalization checkpoint, treat that feedback as binding guidance for rerunning /idea-formalizer on the current approved idea_N.
• If the current branch is a fresh idea_N created after controller-level idea modification, read the immediately previous same-perspective idea_{N-1}/setting.md and idea_{N-1}/proof_review.md as refinement references and as the default baseline for unchanged formalization choices in this new branch.
• If available, read LITERATURE_SURVEY.md only as supporting context for standard notation, standard assumptions, and nearby theorem shapes.
• If useful, read earlier same-perspective idea_K/setting.md and idea_K/proof_review.md artifacts only as calibration signals for notation, setup style, and previously exposed ambiguity.
• Treat the approved idea.md as the primary contract. Literature and sibling branches may guide the formalization, but they must not overwrite the approved setting or goal.
• Treat source-alignment and progress-type metadata recorded in idea.md as binding when present. Preserve it in setting.md rather than reclassifying the branch during formalization.
• Treat the lineage recorded in idea.md as an alignment constraint: use it to preserve the approved parent-paper inheritance, not to import new unsupported assumptions from the literature.
• Treat the assumption support recorded in idea.md as binding: preserve whether theorem-critical assumptions are standard/literature-derived or novel example-verified, including the concrete verification examples for novel assumptions.
• Previous failed artifacts may suggest cleaner notation, better assumptions, a target-preserving primitive source, or a target-changing conservative theorem target, but they must not override the current branch's setting or goal in idea.md.
• If idea.md inherits a theorem-facing recovery, reduction, specialization, zero-defect, exact-limit, exact/noiseless, or baseline-case conclusion from a prior branch or failure record, preserve it in setting.md unless idea.md explicitly marks a target-changing repair.
• On fresh-idea formalization after controller-level idea modification, first identify the semantic delta between the nearest prior same-perspective idea and the current idea.md, together with the recorded failure reason. Preserve previously valid formalization choices from idea_{N-1}/setting.md when they remain consistent with the current idea.md and are not changed by that delta or implicated by the failure; rewrite only the modified or invalidated parts instead.
• On same-idea formalization reruns, preserve already-valid formalization choices unless the approved idea.md or the checkpoint feedback requires changing them.

Step 2: Draft the formalization

Write the current branch's theorem-ready perspective_M/idea_N/setting.md.

• Depending on the current flow, draft it from scratch, revise the current setting.md draft on a formalization-checkpoint rerun, or reuse still-valid parts of the previous same-perspective setting.md as a baseline reference when formalizing a fresh idea_N after controller-level idea modification.

Build # Formalized Setting

• Translate ## Setting in idea.md into # Formalized Setting.
• Split # Formalized Setting into:
• Basic setup
• Technical assumptions
• Place the setting dimensions from idea.md into the appropriate part of the formalized setting, including context, model, data, algorithm, regime, and any other branch-specific constructions needed later in the goal.
• Rewrite the setting in mathematical notation and precise definitions, defining all objects, notation, operators, parameters, regimes, losses, target quantities, and other constructions that the goal will later use.
• Formalize one coherent theorem contract from the approved idea. Do not turn broad parent labels, examples, provenance notes, or sibling artifacts into theorem-facing disjunctions of models, data regimes, algorithms, probability modes, target modes, or assumption packages unless idea.md explicitly requires a union, comparison, or conditional multi-case theorem.
• Assign every item in Technical assumptions a stable ASCII assumption id of the form assump:<slug> and a short descriptive name, for example assump:smoothness (Smoothness). The id is a downstream citation target, not a full LaTeX environment.
• Every theorem-critical technical assumption must be primitive/checkable and must preserve the support class from idea.md: standard/literature-derived assumptions stay tied to the parent literature or standard theorem regime, and novel assumptions may appear only if idea.md already records several concrete branch-specific verification examples. Do not introduce a new unsupported theorem-critical assumption during formalization.
• Distinguish primitive assumptions from derived properties. If a needed property should follow from primitive assumptions, formalize it as a proof obligation, bridge target, conditional branch, or weaker target rather than as a theorem-facing assumption.
• If idea.md introduces an upstream primitive condition intended to derive a needed bound, envelope, correlation, event, stability quantity, or invariant, formalize the upstream primitive condition as the theorem-facing assumption and make the derived control a named proof obligation, bridge target, or intermediate quantity to derive. Do not promote the derived control to an assump:<slug> merely because it is convenient for proof work.
• Formalize primitive sources as assump:<slug> items. Formalize consequences of those sources as bridge targets, intermediate quantities, or proof obligations unless each consequence is independently primitive and checkable.
• After a failure-driven idea revision, preserve the prior theorem mode, scope, conclusion, and inherited baseline invariance obligations when the approved idea records a target-preserving repair through a new supported primitive mechanism source. If the approved idea instead weakens the guarantee, changes theorem mode, changes theorem scope, replaces a nontrivial success criterion by a conservative one, or replaces an inherited baseline/recovery conclusion by a weaker surrogate, formalize that as a target-changing repair explicitly rather than treating it as the same theorem contract.
• Formalize primitive assumptions in the weakest natural control mode from idea.md or the nearest valid prior formalization. Do not strengthen norm, metric, probability, locality, uniformity, independence, smoothness, conditioning, or horizon mode merely for proof convenience. If a stronger-mode control is needed, state it as a bridge target, intermediate quantity, or proof obligation with explicit losses.
• When idea.md says a property should persist, be preserved, remain controlled, stay in a basin, maintain support, or satisfy an invariant, do not formalize that property as exact all-time equality, exact zero leakage, exact membership, or a hard all-time constraint unless idea.md explicitly requires exact invariance and the algorithm contains an exact-preserving mechanism. By default, formalize it as a derived bound, leakage or stability radius, bridge target, conditional target, or weaker target with explicit losses.
• Preserve the approved idea's assumption-form generality. Do not convert an upper or lower bound into an exact value, an inequality into an equality, a broad class into a subclass, or an optional or degenerate case into an exclusion unless idea.md explicitly and validly requires that narrowing.
• Preserve unaffected theorem population and assumption generality from the approved idea. Do not replace broad upper-bound, class, or subobject assumptions by exact, fixed-support, coordinate, or otherwise narrower assumptions unless idea.md explicitly ties that narrowing to the failure being repaired.
• If the approved idea needs a positive or nondegenerate component under a broader assumption, define the active parameter or active subobject and state primitive conditions on that active part rather than narrowing the whole theorem scope.
• For any new or modified theorem-critical assumption, preserve the admissibility support recorded in idea.md. Acceptable support is a cited paper that assumes, uses, or implies it; a standard theorem-regime fact with a short derivation path; or concrete example regimes where the assumption can be checked directly. When a supported constructive mechanism or primitive source can verify a needed property, formalize that mechanism or source as the theorem-facing assumption and keep the derived property as a bridge target, intermediate quantity, or proof obligation. If formalization needs a theorem-critical assumption without recorded support, route back to idea generation instead of adding it silently.
• During drafting, check whether the setting still contains vague or informal phrases; if so, replace them with explicit mathematical objects, conditions, exclusions, or assumptions.

Build # Formalized Goal