econcs-formalizer

name

econcs-formalizer

description

Formalize economics-and-computation papers in Lean. Use when asked to add, continue, triage, or plan Lean formalizations of EC/ACM EC/SIGecom-style papers; inventory sources, build paper DAGs, prepare paper interfaces, extract reusable primitives, coordinate formalization status, run audits, or prepare handoff and closeout guidance. For active theorem proving or proof repair, use econcs-prover as the proof-production companion.

EconCS Formalizer

Use this skill to turn economics-and-computation papers into maintainable Lean code. Keep repository-specific status out of this file; in EconCSLib, that belongs in paper-local status.json, docs/PAPER_STATUS.md, and the website status table.

For new Lean files, new shared-library APIs, new paper-facing declarations, and code already being substantially rewritten, follow skills/lean-community-conventions/SKILL.md. Apply those conventions forward-looking only: do not start broad repository-wide renaming, formatting, import, or documentation refactors during active proof work unless the user explicitly asks for a cleanup pass. Paper-local source-indexed names may remain when needed for source auditability; shared reusable APIs should follow the convention style.

When updating skills from prior sessions or user corrections, use skills/econcs-session-insights/SKILL.md as the provenance workflow. Promote durable day-to-day formalization rules into this skill or its proof references; do not leave them as a parallel operational rulebook in the session-insights skill.

When planning automation-heavy formalization workflows, multi-agent proof campaigns, retrieval-grounded statement translation, or compiler-guided repair loops, also consult skills/ai-formalization-workflows/SKILL.md. That skill is a source-credited ledger of external AI-formalization workflow patterns; this formalizer skill remains the operational rulebook for EconCSLib.

When actively proving a theorem, closing a sorry/admit, or repairing a broken Lean proof, use skills/econcs-prover/SKILL.md as the proof-production companion. This skill owns paper workflow, source provenance, audit surfaces, and closeout; the prover skill owns the local Lean error/search/repair loop.

When syncing EconCSLib-private and EconCSLib-public, preparing public PRs from private work, copying generated DAG/report PDFs, or reconciling audit sidecars across sibling checkouts, read skills/econcs-formalizer/references/public-private-sync.md first. Use that semantic sync workflow instead of raw repository merges or broad folder copies.

Before declaring a paper done, running post-validation/post-formalization audits, updating a final validation report, or preparing a public PR closeout, read skills/econcs-formalizer/references/post-formalization-closeout.md. Keep final validation report structure, post-formalization audits, DAG/source/source-json comparison, LOC sourcing, and note/gap/deviation rules in that one closeout reference for now. Do not split the closeout workflow into more files yet; if it later gets too large, move only DAG-specific visual/layout rules to a future references/dependency-dags.md.

Component 1: Workflow and Organization

1.1 Core Rule

Formalize theorem seams, not PDFs. Start from the paper's precise definitions, the main result to be checked, and the smallest reusable lemmas needed to close that result.

When a paper source has already been downloaded into the repository, treat that local TeX/text cache as the working source of truth. Do not keep repeating web searches for the same source during proof work. If the source is missing and the exact TeX/later-version convention is needed, first check sibling public, private, recovered, and archived worktrees for an existing cache and copy it into the active paper folder. Only download when no local cache exists. Record where the local cache lives, then use that copy for subsequent source checks. Prefer source TeX over PDF text extraction for displayed formulas, numbered equations, theorem labels, and appendix proof steps; PDF text is often good enough for orientation but too noisy to settle algebraic disputes. Before asserting that the source has an issue, a theorem is fixed, or a coauthor-facing edit is still needed, check the current authoritative source cache for that paper. Old source-issue memos, validation reports, LLM sidecars, session notes, and prior suggested-edits files are leads, not evidence about the current draft or published source. State the distinction explicitly when needed: "the repo memo records X" is weaker than "the current source still contains X." If the source changed, classify the old finding as still present, changed, removed, or not rechecked before repeating it.

Use formalized as the repository status word for Lean-checked paper results. Lean verification is the mechanism, not a separate paper status. Do not answer status questions with "verified in Lean" when the intended claim is formalized; reserve "reviewed" for saved human dashboard review entries and "validation" for the audit/checking workflow. Treat status.json human-facing notes as human-authored copy, even when a field is marked draft. Do not add, elaborate, summarize, or reframe human_summary, public notes, website notes, or paper-table comments unless the user explicitly asks for that exact prose change. If the user asks to remove a phrase, remove only that phrase and preserve the remaining text. If the user says a note should be empty, set the source field to the empty string and regenerate script-owned surfaces from that source. Put technical audit details in validation reports, handoffs, or machine-readable audit sidecars, not in sparse public/paper notes. Treat formalized as a strong provenance claim: every exposed paper result is proved by Lean from imported Lean/mathlib/library declarations plus explicit theorem parameters that are either discharged by the proof or recorded as validated paper-source assumptions. The LLM-as-judge checks are audit evidence that the exposed Lean statements and explicit assumptions match the source paper, but they are not themselves Lean proofs, human review, or certification of hidden premises. Before saying a whole paper is fully formalized, confirm the Lean-native axiom audit (#print axioms via scripts/audit_repository.py), the row-local statement checks, and the visible-premise/source-assumption checks are current and clean for that paper. Treat any user request for a "Lean axiom" or "axiom dependency" check on a paper result as a request for the recursive repository audit path, not a single ad hoc #print axioms call: the audit must expand the paper-facing row, follow paper-local aliases and relevant library declarations, then call Lean's axiom printer on the resulting declarations and report hidden premises/certificate APIs along the path. When the user explicitly approves closing a paper modulo one external theorem, prefer a single theorem-shaped, paper-local axiom over a broad endpoint axiom. The axiom should state the external library theorem or theorem bundle being imported, such as a stochastic-convergence or fixed-dimension solver theorem, while deterministic paper source semantics are still encoded as concrete source model records and bridge theorems. The final audit must expose exactly the named axiom, plus approved Lean foundations, and the paper status/report must call the result conditional or axiom-boundary until that theorem is proved in the library. Treat source-formula correctness as a separate provenance obligation from statement text matching. Lean can prove an internally consistent theorem whose inputs already contain a wrong displayed formula; an LLM statement judge can also miss that the formula was assumed rather than derived. For every formula-bearing paper result, know where the formula enters the proof: definition body, derived lemma, explicit validated source assumption, or partial boundary. A result is not fully formalized merely because the final wrapper has the right-looking theorem text. Run a recursive abstraction-debt audit whenever a paper-facing row depends on a record, certificate, replay, process, semantics object, source model, bridge, package, or consequences bundle. Expand the theorem's visible premises and then inspect every input semantically against the paper source model; names are only routing hints and are never evidence by themselves. For each input, either identify the exact paper primitive/source assumption it corresponds to, cite the Lean-checked constructor theorem that derives it from those primitives, route it through an approved external boundary, or mark the row conditional/partial. For Certificate, Replay, Process, and Bridge inputs in particular, the audit must ask for an instantiation path from the paper's primitive model, not just a source-looking type name or theorem wrapper. Then inspect the fields of every such structure recursively until each field is classified as a proved Lean consequence, an imported shared-library theorem, a validated paper-source formula/assumption, a recursively audited container field, a derived consequence-record output, a non-propositional witness datum, an approved external proof boundary, or unresolved proof debt. The LLM-as-judge prompt for these rows must explicitly ask whether any theorem input or field smuggles in the result being claimed, a displayed formula, trajectory generation, convexity, continuity, equilibrium, response semantics, replay/trace validity, transfer preservation, or convergence that should have been derived. Rows whose proof merely projects an opaque field such as trace, replay, process, bridge, directionalField_eq, convex_solutionSpace, response, isMax, convergence, or continuity are conditional on instantiating that field, even if Lean compiles and the top-level theorem statement matches the paper. Mark those rows as source-model boundaries or proof debt unless a separate reviewed row proves the field from more primitive paper assumptions. The recursive audit is a search for an eventual source-backed leaf, not a permission to stop at an intermediate Lean package. If a paper-facing theorem assumes a field that is not directly a source definition/model primitive, the audit must point to the upstream theorem or nested field that derives it from source primitives. If that chain cannot be followed because a structure is missing, the maximum depth is reached, a cycle appears, or a nested container is classified as an ordinary source assumption, treat it as an audit error: a Lean statement is not backed by the source until the derivation chain reaches a validated source assumption, a proved primitive consequence, or an explicitly approved external boundary. This recursive audit must be code-backed before closeout. Run or extend the skill helper python3 skills/econcs-formalizer/scripts/source_record_audit.py --paper <paper-folder> --out papers/<paper-folder>/audit/source_record_audit.json so the audit payload is generated from the current Lean files, includes Lean #check output for the paper rows and structure fields, and gives the LLM judge the actual kernel-checked statements rather than a prose summary. The judge must classify every source-record field as proved_from_primitives, validated_source_assumption, approved_external_boundary, nonpropositional_witness_data, or unresolved_assumed_math; it may use container_recursively_audited only for a field whose type is another audited source/record/certificate and whose nested fields are separately judged, and derived_consequence_record only for theorem output records whose constructor proof is checked and whose premise records are separately audited. Use nonpropositional_witness_data only for bare data witnesses whose type is not proposition-valued and does not itself state a formula, equality, recurrence, optimality, measurability, convergence, continuity, response semantics, or trajectory semantics; the proof fields that constrain those witnesses must still be audited separately. Do not accept matches for a row whose decisive math appears only as a record field projection. At a real closeout/publication boundary, the provenance gate invokes python3 scripts/audit_repository.py --paper <paper-folder> --paper-closeout --include-active --info-limit 0. During active formalization on an unfinished paper, do not run that closeout gate unless the user explicitly asks for post-validation; use targeted Lean builds, placeholder scans, and row-scoped LLM-as-judge checks for the exact changed statements, assumptions, or source-record fields. Do not start the full dashboard/sidecar/final-report audit loop merely because a proof-surface row, source record, or status entry changed while the paper is still known unfinished. If a proof pass adds or changes source-record fields, run the code-backed recursive audit or LLM judge only for those changed records/rows when needed to prevent hidden assumptions, but defer full dashboard prechecks, full statement sidecar regeneration, DAG/final-report audit updates, and --paper-closeout until the paper is actually done or the user explicitly asks for that validation phase. The eventual closeout gate must report missing, stale, or unresolved source_record_audit.json / source_record_match_llm.json sidecars as assumption/provenance findings. In a proof-production turn, spend time on proof-side progress first. Do not refresh DAGs, validation reports, generated status tables, broad audit sidecars, or commit/push solely because an intermediate theorem changed; wait until the paper closes, a genuine proof milestone needs checkpointing, or the user explicitly asks for those artifacts. Treat the configured review source as a closed review surface, not a scratch file. By default this is PaperInterface.lean, but large papers may set status.json review_surface.source_file to AuditInterface.lean so PaperInterface.lean remains a compact human-facing entrypoint while the full row-level dashboard and LLM-as-judge declarations live in the audit surface. Every declaration exported from the configured review source must be classified in status.json review_surface.include_names, review_surface.assumption_names, or review_surface.auxiliary_names. Use auxiliary_names only for proof-facing helpers intentionally excluded from statement review, and never to hide a named paper theorem or a non-source premise. If a helper theorem needs a ...Certificate, ...Model, ...Semantics, ...Bridge, ...Package, ...Inputs, ...Process, or ...Consequences premise that is not itself derived from prior Lean code, keep it in ProofInterface.lean/MainTheorems.lean unless it is a reviewed row or a validated assumption/proof boundary. During active proof work, after a configured review-source edit run targeted checks for the changed declarations and premises; do not enter the full dashboard/sidecar workflow solely because the review surface changed. At closeout or user-requested post-validation, run python3 scripts/review_dashboard.py --paper <paper-folder> --precheck or the paper-specific machine-status audit; a clean statement-judge sidecar alone is not evidence that hidden premises or unreviewed helpers are absent. Before creating a paper-local definition, record, theorem family, or reusable EconCSLib/ primitive for a common proof seam, do a dependency and shared-library context load. Search imported upstream libraries first: Mathlib/ for mathematical structures and theorems, Cslib/ for computer science and runtime notions, and Optlib/ when it exists in the workspace or Lake manifest for optimization-specific APIs. Prefer those definitions and results over creating local replacements. If an upstream API almost fits, add a thin bridge lemma or source-facing notation around it; only introduce a new library primitive after recording why the upstream API is not adequate. For overlapping EC, game-theory, social-choice, mechanism-design, optimization, or proof-pattern seams, also scout the potential upstream Lean sources listed in docs/UPSTREAM_LEAN_SOURCES.md, currently including elazarg/GameTheory, alexfleetcommander/lean-proofs, and gametheoryinlean/EconCSLib. Treat those as scouting sources unless toolchain, license, API stability, and dependency approval have been checked. If you use or port material from any upstream source, cite it with repository URL, file/module path, commit or release when available, license status, and a short description of what was reused; place that provenance near the resulting Lean code or in the paper/formalization plan, and cite it in human-facing paper text when the reuse affects the manuscript. Search EconCSLib/ next for the domain noun and proof shape: equilibrium/best-response/a.e. exception, threshold/cutoff, CDF/quantile/PIT/tie-breaking, finite mixture, Gaussian/admissions/testing, LP/certificate, ranking/social choice, auction, or large-deviation. Open the most relevant shared files and reference notes before adding local scaffolding. If a reusable API exists, import and specialize it. This check belongs in the initial outside-of-Lean plan for every paper and again whenever a proof loop starts building wrappers around a standard concept. Also search related paper folders, especially completed or recently active papers in the same domain, before adding paper-local machinery. Many reusable algorithmic layers first appear inside a paper folder before being promoted to EconCSLib/; do not reinvent a simulator, runner, trace generator, dynamic process, checker pattern, certificate, or source-model constructor until you have searched sibling papers for the same domain nouns and declaration shapes. If two papers need the same machinery, elevate the common core into the shared library or route the current paper through the existing reusable paper layer as an interim step, rather than creating parallel incompatible APIs. Record in the outside-of-Lean plan which related paper folders were checked and why the chosen API is the one to build on. If the user, notes, or repository history suggest a specific same-domain paper already built the machinery, pause implementation and inspect that paper plus its imports before adding new declarations. For continuous equilibrium work in particular, check EconCSLib.Foundations.Optimization.ChoiceEquilibriumAE, StrategicEquilibrium, and the admissions/testing probability modules before defining a local equilibrium or distributional interface. For continuous optimization or geometry work, assume mathlib probably already has the basic objects: norms and distances on finite products, WithLp/PiLp, inner-product and finite-dimensional spaces, Frechet/scalar derivatives, convexity/concavity/extrema, projections, Holder inequalities, and special function derivative rules. Search and reuse these before writing formula-level norm, derivative, convexity, projection, or argmax APIs in EconCSLib/. The outside-of-Lean plan must contain a short "shared-library reuse checkpoint" before any substantial proof campaign: list the shared declarations or modules inspected, including relevant mathlib/cslib/optlib candidates, potential upstream Lean sources from docs/UPSTREAM_LEAN_SOURCES.md, the API chosen, and any near-miss that was intentionally not used. Include citation/provenance for any upstream material used or ported. If that checkpoint is missing, add it before continuing. If a proof loop starts creating several local wrappers around a standard notion, pause and update this checkpoint instead of continuing the wrapper stack. A reusable concept should enter the paper proof through the shared API unless the plan explains the source-specific obstruction. In particular, do not use a syntactic recursive dependency scan as the primary proof-debt test. Lean already knows the transitive proof dependencies of a closed theorem: #print axioms must report only approved standard foundations such as propext, Classical.choice, and Quot.sound. Use the expanded #check/dashboard premise audit for visible theorem hypotheses, and use source-shaped library/API hygiene to prevent paper formulas from being hidden inside reusable definitions. The formula audit must be recursive: if a paper-facing theorem uses a library definition or theorem whose parameters, fields, or body encode a source displayed formula, the LLM-as-judge workflow must inspect the expanded formula or a proved paper-local equivalence to it. This audit must include paper-local structures as well as reusable library definitions. For every source-semantics record, add a brief field provenance table in the paper plan, handoff, validator ledger, or status notes before calling the row fully formalized. If the desired theorem should follow from paper assumptions but currently follows only because a record field states the needed fact, the correct next step is to refine the source model or prove a constructor from primitive assumptions, not to let the record field pass through the assumption judge as ordinary source text. The source-record audit is not satisfied by a natural-language list of fields. It must be generated from code that parses the review rows, recursively follows record/certificate/source-model types, and feeds those row and field types back through Lean. If the helper misses a local pattern, patch the helper or the repository audit before accepting the LLM result. The LLM judge should see the source text, Lean #check output, dependency path, and field provenance, and it must answer the narrower question: is this mathematical source statement proved by earlier Lean declarations, or is it merely assumed by a source field? Do not allow "the library definition says it" to substitute for source-formula validation. Ordinary source-visible theorem conditions such as positivity, measurability, or ordering hypotheses should be validated by the statement/assumption judges, but they are not the same thing as global proof debt. If a paper theorem cannot be derived without an extra geometric/model premise, do not force that premise through the source-assumption judge just to keep the headline theorem. Expose the exact missing formula as a record-free predicate, prove the strongest no-hidden-premise alternative (for example conclusion ∨ ¬ missing_formula), and separately prove any exact restricted theorem whose extra condition really discharges the formula. The paper report and statement judge should mark the restricted theorem as a conditional boundary rather than a match to the unrestricted source theorem. The hardened repository audit is standard-based, not function-name-based. It rebuilds declaration indexes each run, follows paper-local aliases for visible premises, asks Lean for transitive axioms, scans reusable library declarations for certificate/source-boundary APIs, rejects reusable Assumption or Hypothesis declarations, rejects paper/source provenance wording in EconCSLib/*.lean, and checks generic code/docs for concrete paper IDs, citation prefixes, or paper theorem-number labels. Put paper metadata in paper-local files or data config; keep EconCSLib/, audit scripts, and generic workflow docs paper-neutral. If a citation-like term is truly an established algorithm/domain name, record that as a data-configured allowlist entry rather than a code exception. This audit reduces hidden-premise and generic-code drift, but it still does not prove source formulas correct by itself; do the outside-Lean formula sanity pass and derive formula-bearing claims from primitives whenever possible. Shared-library comments and docstrings are part of this generic surface: do not describe reusable results as "Theorem 1", "Lemma 2", or by a paper ID even when the result was extracted for a paper. Use paper-neutral mathematical language such as "finite-product likelihood factorization" and leave the paper-number crosswalk in the paper folder, final report, or status metadata.

Unless told otherwise, you do not have a time limit; keep going until you reach the requested stopping condition or a clean theorem/compile boundary. Run the full post-paper checklist, review-dashboard/audit workflow, and polished FINAL_VALIDATION_REPORT.md update only when the paper is genuinely finished or the user explicitly asks for post-validation. For intermediate progress on an unfinished paper, use targeted Lean builds and a short status/handoff update instead of spending tokens on the full audit/report cycle. Do not run scripts/audit_repository.py --paper <paper> --paper-closeout for routine progress on a paper that is still partially formalized, conditional, or known to have remaining library/proof-boundary work, unless the user explicitly requests closeout/post-validation or the next action is a public PR/release handoff. In-progress checks should normally be limited to the edited Lean targets, JSON/line-count sanity checks, placeholder scans, and optional row-scoped LLM-as-judge checks for newly changed statements, assumptions, or source-record fields. Defer dashboard prechecks and full sidecar/report regeneration until the paper is actually done or the user requests post-validation.

Do not confuse "keep going" with broad exploration or with optimizing for the fastest next small lemma. Default to a top-down completion plan for the whole paper. Start from the named paper results that remain unclosed, identify the source-model or library layer that would discharge each visible certificate or conditional premise, and order the work by the shortest route to full paper-level closure. Use small theorem batches as the execution unit only after that overall route is clear, and choose those batches because they remove a paper-facing obstacle on the completion path. Avoid adding local helper wrappers merely because they are easy unless they visibly reduce the final theorem assumptions or turn a documented source-model gap into a proved bridge.

Once the top-down route is clear, move in tight compile/proof loops: identify the current paper-facing theorem seam, make a coherent batch of edits, run only the requested or necessary targeted build, and patch the compiler's concrete line errors. Avoid rereading large files after you already know the relevant structure; use rg for exact declaration names and narrow line windows around compiler diagnostics. If an active proof batch edits shared EconCSLib/ library code, still stay in the targeted-build loop: build the touched library module or namespace root and the active paper root that imports it. Do not run a broad/full repository build merely because a shared library file changed while the paper is still in progress. Save broad builds for natural stopping points: the paper is complete or being handed off, you are about to commit/push a significant integration batch, preparing a public PR/release, or the user explicitly asks for a broad integration check. Do not treat a fresh clean worktree build as part of the closeout requirement when it would trigger a cold dependency or mathlib build. Closeout should use the active warmed worktree for targeted Lean builds plus the status/dashboard and repository audit checks. A temporary clean worktree is acceptable only for cheap committed-state checks such as generated metadata, git diff --check, or status-sync validation, or when CI/public release work explicitly requires it and the needed dependency cache is already available. Do not run concurrent lake build commands in the same worktree: Lean cache writes can race on .olean/.ilean outputs and produce spurious missing-file failures. Prefer one targeted Lean build at a time, especially in shared multi-agent sessions. On Ubuntu-based systems where shell calls print Failed to create stream fd: Operation not permitted before otherwise normal output, prefer noninteractive command execution with no TTY and no login shell when the tool supports it. In this Codex environment that means setting tty=false and login=false on exec_command. Treat the warning as environment noise only if the command's exit code and real output are clean.

When another agent will pick up later, spend tokens on durable artifacts rather than chat: a paper-local handoff note, audit/report links, exact declaration names, validation status, and next command. Future agents should start from those files instead of reconstructing context from conversation history. When reporting Codex token usage for a paper, workflow, or publication table, avoid file-level overcounting. Parse only ~/.codex/sessions/**/*.jsonl; ignore prompt history files and plugin/test fixtures. In each rollout file, the first session_meta is authoritative; later embedded session_meta records may come from summarized context and must not overwrite the file's identity. For unique-session counts, build a parent graph using source.subagent.thread_spawn.parent_thread_id first and forked_from_id second, then collapse to root session trees. Exclude guardian/auto-review rollouts (source.subagent.other = "guardian" or model codex-auto-review) from human formalization token tables unless explicitly reporting tooling overhead. Report top-level/root-only usage separately from subagent-inclusive actual API usage; do not mix a root session count with all-descendant token totals without saying so. Subagent and resumed rollout files can embed a copied parent transcript after the first session_meta; those copied records often include parent token_count events and must not be charged again. For each rollout, find the first own turn marker whose turn_id shares the session id's leading timestamp group, then compute usage as the cumulative total_token_usage after that boundary minus the last cumulative total_token_usage before it. Cross-check that delta against summed last_token_usage records after the same boundary. Cached input tokens are already included in input tokens, so compute uncached input as input - cached; charge reasoning tokens only through the output-token row. Do not dedupe repeated parent/resume/subagent prompt context out of a billable-usage estimate merely because a human regards it as repeated work: each descendant model request still sends input tokens, and prompt caching only moves matching prefixes to the cached-input rate. Replayed context in resumed or subagent sessions is real API usage when it appears in the rollout's own post-boundary usage logs, but if the goal is a human-facing "unique work" estimate, label that separately instead of presenting it as raw billable usage. For financial reconciliation, prefer the OpenAI Costs/Usage dashboard or Costs API over local log reconstruction. Sanity-check local counts against known scale. In the June 5, 2026 workshop audit, 492 rollout files collapsed to 7 non-guardian root session trees. The naive file-level sum over embedded transcripts reported about $58k; the corrected post-boundary, subagent-inclusive non-guardian estimate was about 6.05B total tokens and $4.6k, with subagents contributing about $775. If a future all-session estimate is an order of magnitude larger than the top-level estimate, inspect for embedded parent transcript token events before publishing the table. When the latest green endpoint is a source-sequence, source-certificate, or analytic boundary rather than the actual paper distribution/object, say that plainly in the private handoff/plan and public status/final report. Name the exact identification bridge still missing; do not let a compiled certificate wrapper read like the paper theorem is fully closed. For a pause of several days or longer, create or refresh a paper-local START_HERE_NEXT_AGENT.md that is shorter than the full handoff: current validation commands, shared-worktree caveats, the exact active proof seam, strongest reusable endpoints, and what not to work on next. Link or reference it from the private paper plan/status surfaces so a future agent has one obvious startup path. Keep this handoff private by default; link it from the audit/final-validation report only during a paper-done or user-requested post-validation pass. For a week-scale pause after a long proof push, also create a dated paper-local handoff such as HANDOFF_YYYY-MM-DD_WEEK_PAUSE.md and make START_HERE_NEXT_AGENT.md point to it first. That week-pause note should name the exact current theorem seam, the strongest bridge theorem to use next, the closed layers future agents must not redo, the files intentionally touched, and the validation command set. Keep it concise enough to be read before opening large theorem files. If the latest green declarations are support endpoints rather than closed paper results, say so explicitly in the handoff and do not over-mark the DAG. If a paper is being paused for a stronger future model, say that explicitly in the private handoff/plan and in the front repository status entries. Name the three or fewer exact proof seams that remain and the strongest public wrapper or certificate for each. Do not leave vague optimistic status such as "one bridge remains" when multiple paper-level proof campaigns are still open. When a remaining seam is a large family of repetitive row/table identifications, package those facts into a source-shaped structure and expose a single packaged bridge before stopping. Handoffs should point future agents at the package as the proof target instead of asking them to rediscover a dozen flat premises. Do not overclaim the packaged bridge as closing the source model; say exactly which row-identification package is still unproved. When bounded, Pareto, or other tail-heavy recommendation proofs duplicate the same exact power-law finite-optimality argument, extract the FOC core into a generic theorem parameterized by the marginal exponent, target exponent, and exact backward/forward marginal formulas. Keep the distribution-specific files as thin instantiations, and leave the source theorem rows partially formalized or conditional until the probability/order-statistic derivation supplies those exact or asymptotic marginals. Use formalized with caveat only if the final theorem is closed but intentionally differs from the source statement. Do not derive a scaled first-difference/drop hypothesis merely from a value or loss asymptotic such as A - h(q) ~ C q^(-η). That asymptotic alone does not control finite differences without a regularity/monotonicity theorem strong enough for the source. If the proof needs (q+1)*((A-h q)-(A-h(q+1)))/(A-h q) -> η, expose it as an explicit scaled-drop hypothesis or prove a separate source regular-variation lemma. For concrete bounded order-statistic laws, prefer a direct source-specific mean-table route when it is available. An exact gamma-ratio formula for fixed ranks can prove both the value/loss asymptotic and the scaled-drop law internally, then feed the existing scaled-marginal certificate without exposing scaled_drop to callers. Keep the reusable gamma-ratio asymptotic in the library and the paper-shaped mean table in the paper unless another paper needs the same table. When a concrete iid source table is proved pointwise/top-k equal to a synthetic mean table that already has asymptotic certificates, add or reuse a small library-level certificate transport lemma rather than replaying the asymptotic proof. For top-k order-statistic sources, the reusable pattern is to prove the expected-order-statistic mean sequence equality, lift it to top-k sums, and transport ScaledMarginalLimitCertificate through eventual marginal equality.

Reserve formalized with caveat for cases where the Lean theorem adds something on top of the paper statement, such as an extra assumption, restriction, corrected statement, or indispensable source mismatch. If Lean also proves that a broader arbitrary abstraction is false but the paper-facing source theorem is closed, mark the paper theorem formalized and record the broader abstraction as a scope note or out-of-scope failed generalization, not as a caveat on the paper result. Use conditional for an incomplete proof boundary: a wrapper still takes an explicit certificate, witness, imported theorem, shortcut predicate, or paper-model hypothesis that should be derived from the source assumptions. Do not call this a caveat merely because Lean has not yet connected the paper's own assumptions or appendix derivation. A caveat means the final theorem differs from the source statement; a conditional status means the source statement may be faithful but some derivation remains undischarged. Use partial_boundary in assumption-provenance JSON for a visible external, library, analytic, runtime, solver, or theorem-import boundary that remains undischarged. This can be the top-level judgment for an assumption_* declaration as well as an individual premise judgment. Do not downgrade it to documented_caveat unless the source statement itself is false, missing a needed non-source condition, or intentionally repaired in the Lean endpoint. Use documented_additional_assumption for a non-source condition that a human has approved as an additional-assumption note while keeping the paper status formalized, such as an endpoint restriction that is recorded in the validation report under additional assumptions. Use the following anonymous classification examples when deciding status and report language:

Situation	Classification	Public/report language
The printed theorem is false as stated, or Lean proves only a corrected/sign-repaired/constant-repaired endpoint that changes the source claim.	Real caveat; usually formalized with caveat if the repaired endpoint is closed.	"Paper issue/caveat: the source statement appears to need ; Lean proves the repaired statement."
The paper/source model already implicitly or explicitly assumes the domain condition, such as positive capacity, more objects than slots, interior parameters, finite support, no ties, or a nondegenerate witness needed for an exact rather than at-most statement.	Not a caveat. Treat as a source theorem condition or source-model condition; use paper_condition, source_text, or human_verified_source_implicit in assumption/provenance sidecars.	"Additional/source condition: the theorem is stated with ." Keep main_caveat blank if fully proved.
The user approves an extra non-source restriction while still calling the paper formalized, such as an interior-quality condition needed for a strict inequality where boundary cases are equality.	documented_additional_assumption, not documented_caveat, unless the user/source review says this is a paper error.	"Additional assumption: strict is proved under ; record it under additional assumptions, not caveats."
The source has a likely typo or finite-bound slip, but Lean proves the main asymptotic/source theorem through a corrected intermediate statement and the correction does not change the public theorem endpoint.	Source-quality note or proof-strategy deviation, not a paper caveat.	Put it under mathematical typos/source notes; keep status formalized and main_caveat blank.
An appendix/intermediate lemma is globally false as printed, but Lean proves the named theorem or main-text result by a different source-valid route, and also records the exact corrected local condition plus counterexample.	Source note, not a status caveat, unless the false lemma is itself the paper-facing target being claimed as-is.	Keep status formalized; write a short math note with the paper statement, actual Lean statement, counterexample, whether the condition appears elsewhere in the source, and how downstream theorems avoid or use the repair.
The source uses private data, empirical plots, implementation measurements, or descriptive program/class instantiations not needed for the mathematical theorem target.	Out of Lean theorem scope, not a caveat and not an additional assumption.	"Empirical/descriptive material is out of theorem scope." Do not list as remaining proof debt.
Lean currently assumes a solver theorem, convergence theorem, process law, runtime bound, certificate, source-record field, or bridge predicate that should be proved from paper primitives.	Proof/library boundary: partial_boundary, conditional, or partially formalized until proved.	"Full formalization requires proving ." Do not call it a caveat unless the final theorem statement itself differs from the paper.
A converse, bridge lemma, or source derivation is missing but looks provable from the current source assumptions.	Missing proof debt.	Either prove it, or mark a proof boundary. Do not call it a caveat merely because it is not proved yet.

For a user-approved axiom boundary, keep the axiom in the paper folder's Assumptions.lean or another paper-local assumptions file, give it a precise assumption_* name, and validate it as partial_boundary. Do not put paper-specific axioms in reusable EconCSLib/, and do not hide paper formulas inside a generic axiom that the recursive audit cannot identify. Do not use formalized with caveat for source-quality notes, poor OCR, or an audit observation that does not change the closed paper-facing theorem. Put that note in the final report and leave the status formalized. For such source notes, do not use dag_caveat styling or a caveat legend in the dependency DAG. Keep the named theorem/lemma node in its ordinary formalized style, mention the correction in concise paper-facing language, and put the detailed statement/counterexample in the final report or a focused math note. When a fully proved endpoint exposes a standard regularity condition needed to interpret a source formula (for example continuity/positivity needed for a Laplace-principle reading), classify it as a validation note if the user/source review accepts that reading and the Lean theorem does not leave proof debt. Record the condition in Assumptions.lean and the assumption sidecar with paper_condition, source_text, or human_verified_source_implicit premise judgments as appropriate; do not mark it partial_boundary or documented_caveat unless it is actually an undischarged theorem import or a source-statement repair. When the paper itself defines a convention that selects, erases, normalizes, or packages terms, do not re-label that convention as a caveat merely because an alternative raw mathematical object would differ. Close the source-shaped statement, record the convention in an agent-facing audit note if future agents are likely to confuse it, and keep the public status and human verdict focused on whether the paper-facing theorem is closed. For generated status files, keep main_caveat blank on clean formalized papers. Do not put provenance summaries such as "axiom audit clean", "assumptions source-matched", "human verified", or "no hidden premises" in a caveat field. Those are validation/report notes, not caveats. Use main_caveat only for a real source discrepancy, corrected statement, indispensable non-source assumption, or explicit remaining boundary; otherwise let the public table be sparse. Before finalizing a DAG, generated status surface, validation report, or a README edit explicitly requested by the user, audit every formalized with caveat row. Run a focused grep such as rg -n "formalized with caveat|Formalized with caveat|dag_caveat|Caveat:" over the changed public paper/report/status files, then classify each hit. If the issue is an unfinished theorem, external theorem import, runtime layer, analytic derivation, missing library component, or other proof boundary that does not change the final paper statement, use partially formalized or conditional and describe the remaining boundary. Keep formalized with caveat only when the closed Lean endpoint intentionally differs from the paper because of an added non-paper assumption, a corrected/repair statement, or a real source mismatch. If any named source endpoint still exposes an explicit certificate, witness, external theorem, or paper-model hypothesis that has not been derived from the paper's primitive assumptions, the whole paper is partially formalized, even if most theorem infrastructure compiles. It may still be public, but the DAG, generated status surfaces, and final report must all name the exact remaining certificate or external-library boundary. If a paper-facing theorem genuinely needs a source assumption, expose that assumption as a first-class declaration in paper-local Assumptions.lean rather than as an arbitrary theorem hypothesis. Name it assumption_*, paper_assumption_*, or source_assumption_*, list it in status.json review_surface.assumption_names, and validate it in assumption_match_llm.json with an independent source-assumption judge. A premise is allowed to remain in a formalized endpoint only if it is routed through that assumption ledger and the judge confirms it is an actual paper/source model assumption. Capacity equations, threshold identities, density normalizers, selection-mass formulas, row packages, and certificate fields are proof obligations unless the paper explicitly assumes them. Use the strict prompt sidecars when doing this validation. lean_to_tex_llm.json should record prompt_version: "lean-to-tex-v3-strict-context-free-semantic-inputs" and preserve every binder, hypothesis, domain, named predicate/wrapper application, direction, and conclusion in the translation; it must not turn a named premise into a theorem label, source-like phrase, or proof-route summary. Each row needs the current lean_statement_sha256; missing digests are stale audit evidence, not optional metadata. All model/agent audit sidecars are fail-closed. A blank scaffold, parse error, missing file, missing current prompt_version, missing current digest, missing validator/model identity, missing timestamp, stale source inventory, stale dashboard surface, unrecognized judgment, failed run, or item without an explicit success verdict is an alarm and does not count as audit evidence. The only passing state is a current sidecar whose version, digests, validator metadata, and recognized success judgment match the current Lean/source inputs. Do not convert a missing or failed judge run into a warning merely because Lean builds; Lean proves the encoded statement, while these sidecars audit whether the encoded statement and visible assumptions match the paper. At public-facing closeout, require an explicit current review_surface_llm.json pass even for small dashboards. The 30-row threshold is an early workflow prompt for broad human review, not an exemption from final review-surface evidence. statement_match_llm.json should record prompt_version: "statement-match-v3-semantic-full-statement" and reject omitted source subparts, extra non-source hypotheses, hidden strengthening inside named predicates, formula-level changes, broad aggregates, source-row packages, certificate/replay/process/bridge packages, and any input whose semantics does not match a paper primitive or a Lean-derived consequence of paper primitives. The statement judge must inspect named predicates/wrappers semantically; phrase overlap and source-looking Lean names are not evidence. Each item needs current Lean, paper, and TeX statement digests. For assumptions, assumption_match_llm.json should record prompt_version: "assumption-provenance-v3-semantic-exact-premise-source". Every exact -- audit-premise: entry needs its own premise_judgments row with either a source location, a Lean-derived provenance judgment, or an explicit partial-boundary/not-source finding; a declaration-level judgment alone is not evidence. For source-record provenance, source_record_match_llm.json should record prompt_version: "source-record-v2-semantic-boundary-inputs". The judge must classify every boundary-shaped visible theorem input and every recursive field from source_record_audit.json; a replay/certificate/process/bridge/source-row input cannot be approved unless the sidecar gives specific source evidence, a Lean constructor/derivation from primitives, an approved external boundary, or an unresolved finding. Do not count old unversioned source-record sidecars as current. A source_record_match_llm.json entry classified as approved_external_boundary is not compatible with a fully formalized paper endpoint unless that endpoint is explicitly outside the claimed proof surface. It is valid evidence for a partial/conditional row only after the same boundary appears in status.json, the DAG, and the final validation report. If a source-record audit separates bare witness data from a proposition-valued validity or replay predicate, treat the bare witness as possible source-model data and the validity/replay/process-preservation predicate as proof debt until it is derived from paper primitives or recorded as the intentional partial boundary. Remember the visibility limit of the LLM assumption lane. It sees configured Assumptions.lean declarations and exact -- audit-premise: rows; it does not automatically certify arbitrary structure fields, library definition bodies, or helper theorem premises excluded from the review surface. If a source formula is encoded inside a record field or library definition, recursively inspect that field/body or prove a paper-local equivalence before calling the premise derived. If a theorem premise is outside the reviewed/assumption/auxiliary classification, treat that as an audit failure, not as a harmless helper. Check the expanded Lean signature, not only the source text of the wrapper. Unused proof arguments and broad row bundles can print as anonymous top-level arrows such as SomeRows ... -> theorem_conclusion, with no binder name for a regex to catch. Premise checks must classify the head of each visible anonymous premise type and either discharge it, route it through a named Assumptions.lean declaration with -- audit-premise: comments, or mark the endpoint partial/conditional. Prefer exposing the smallest component source assumptions and constructing broad row bundles internally; do not leave a single aggregate PublicRows/SourceRows premise as the paper-facing provenance boundary when its fields are separately reviewable. Keep the expanded dashboard cache current before using it as evidence: after changing PaperInterface.lean aliases or theorem signatures, run python3 scripts/review_dashboard.py --paper <paper-folder> --refresh-cache. The expanded dashboard statement is the visible review surface for ordinary scalar theorem conditions such as positivity, interval membership, or displayed paper inequalities. It is not enough for certificate/source-row/external boundary packages: those must still be constructed internally, exposed as validated paper assumptions, or marked partial/conditional. For analytic or algorithmic theorem boundaries, first construct the concrete source-model record from visible paper primitives, then prove a bridge from that record plus the theorem-shaped external axiom to the endpoint consequences. Avoid axiomatizing the endpoint consequence package itself, because that hides whether the paper's source semantics actually feed the external theorem. Do not rely on "source row" wrappers or theorem parameters to smuggle formulas into a closed proof. A displayed formula, defining equation, threshold equation, normalization, selection-mass identity, distribution law, recurrence, or capacity condition counts as derived only when Lean proves it from the source model primitives or it is listed as a source assumption and validated at premise granularity. If such a formula is merely supplied to the theorem, the endpoint is conditional/partial no matter how faithful the statement text looks. This rule applies to every formula, not only admissions cutoffs or normal integrals: signs, constants, denominators, support/domain restrictions, normalizers, mixture equations, recurrence steps, equilibrium inequalities, objective decompositions, and probability-law identities all need either a Lean derivation from primitives or explicit source-assumption provenance. This applies through the reusable library as well as paper-local files. A library theorem may take an explicit certificate, witness, or formula package; that is a good API because Lean forces callers to provide it. A paper-facing row is closed when its expanded statement no longer exposes such a premise and #print axioms on the row reports only approved standard foundations. Do not mark a row partial merely because its proof calls internal library lemmas with certificate-shaped names when those certificates are constructed by closed Lean theorems. Do not bake paper-source displayed formulas into EconCSLib/ definitions or implicit instances to make the call site look unconditional; make source formulas explicit parameters/certificate fields or keep them in the paper folder. If a reusable definition itself contains a formula that came from one paper, the library audit cannot prove the formula correct by naming convention alone. Make the library definition paper-neutral and expose the paper-specific identification as a caller-supplied theorem/certificate or a paper-local derivation. This keeps transitive dependencies honest: all source-dependent facts used by a paper-facing theorem must either appear in that theorem's expanded premise/provenance surface or be constructed internally from proved primitives. After editing reusable library code, run python3 scripts/audit_repository.py --library-only --library-premise-audit. This fails source-shaped reusable API names, hidden proof-boundary section variables, axiom/opaque placeholders, and guarded debug commands, and reports direct certificate-boundary APIs as informational findings. The library parser covers theorem, lemma, def, abbrev, structure, class, and inductive declarations; do not assume a proof-boundary structure is invisible to the audit just because it is not a theorem. If the audit flags a source-shaped reusable name, either rename it to a paper-neutral abstraction, make the source formula an explicit argument, or move it back to the paper folder. Use --info-limit -1 when you need the complete library-boundary inventory. CI should use --info-limit 0 so only actionable errors/warnings appear in logs. When private GitHub Actions fails but gh cannot read logs because local authentication is stale, reproduce the workflow commands locally before guessing at the failure: scripts/sync_paper_status.py --check, the library-premise audit, and the relevant lake build. Run the full repository audit only when the failure came from the manual closeout workflow path or the user explicitly asks for closeout validation. Treat a clean local reproduction as the basis for a scoped CI fix, and report that remote logs were unavailable. Keep CI fast by separating metadata/workflow churn from proof changes. A skill-only commit should not run full Lean CI; configure workflow paths-ignore for skills/** and commit proof-affecting changes separately. Use GitHub Actions concurrency with cancel-in-progress: true for Lean CI so superseded pushes on the same branch do not burn a full build. In the workflow, run fast source-only checks such as scripts/sync_paper_status.py --check and the library premise audit before leanprover/lean-action; that fails status or provenance drift before the expensive Lean build starts. Keep the full repository closeout audit behind workflow_dispatch, not routine push/PR CI, unless the branch is specifically being promoted or released. Do not block your own work by watching GitHub CI unless the next action actually depends on the result, such as merging a PR, cutting a public release, or diagnosing a known failure. For routine pushes, confirm that the run started or was intentionally skipped, record the run if useful, and keep working. Treat suffix-named structures such as ...Certificate, ...Oracle, ...Window, ...Package, ...Process, ...Regularity, and ...Invariant as proof-boundary evidence even when they are not named hcert. Do not keep these as namespace/section-level variables in reusable code; pass them explicitly to each theorem/definition that consumes them so callers cannot inherit the premise silently. Generic data predicates such as feasible : α → Prop or move : α → α → Prop may remain section variables when they are just model parameters, not proof evidence. Apply the same visible-premise rule inside the paper folder. If a paper-facing theorem, its expanded #check statement, or a direct paper-local alias target still takes a certificate, hidden hypothesis, source-row equation, or proof-boundary premise, that premise must be derived, routed through Assumptions.lean, or marked partial/conditional. If a helper constructs the certificate internally and the final paper-facing theorem no longer takes it as an input, the certificate is discharged; confirm that with #print axioms rather than a lexical dependency scan. Do not use axiom, constant, opaque, or unsafe declarations to stand in for the missing derivation unless the user explicitly approved one named theorem-shaped external boundary axiom and the paper is reported as conditional/axiom-boundary. Even then, do not use an endpoint-consequence axiom when a concrete source model plus an external theorem statement would expose more of the real proof obligation. Do not leave those proof obligations as the default proof shape. If an explicit certificate, row package, or extra hypothesis is introduced to unblock a build, treat it as a temporary checkpoint: immediately name the closure lemma that would derive it from the source model, attack that lemma before moving to new paper results, and keep the downstream theorem partial/conditional until the certificate is either discharged internally or promoted to a validated paper-assumption declaration. The normal proof loop should reduce the number of visible certificates and extra hypotheses, not accumulate them. For a final formalized paper, scripts/audit_repository.py should not report hidden-premise, source-row, opaque-alias, broad-aggregate, stale-LLM-sidecar, or missing-source-provenance findings for that paper's review surface. If the global audit reports unrelated active-paper warnings, filter to the paper under review and make the final claim only for papers whose own warnings are clean or explicitly classified as non-theorem packaging notes. If a certificate/interface structure is constructed internally and the final paper-facing theorem no longer takes it as an input, that certificate is discharged. Do not imply additional certificates are needed; for fully formalized papers, status comments may be empty. If a named paper theorem is closed but a downstream corollary or application that uses it is still conditional, split the status/DAG entries. The named paper theorem should stay green with its actual statement; the conditional application should get its own row or node. Do not let a harder follow-on endpoint make the source theorem look unformalized.

In EconCSLib, paper-local papers/<Paper>/status.json files are the source of truth for paper status, compact human_summary notes, human-review row counts, PaperInterface.lean metadata, review-surface slices, and artifact paths. After changing any of that metadata, run python3 scripts/sync_paper_status.py at a status milestone. That command regenerates the detailed papers/status.json, the compact human-facing papers/human_status.json, docs/PAPER_STATUS.md, and the status table in site/index.html. Do not hand-edit those generated status outputs. README files are human-owned prose surfaces, not generated status surfaces by default. Humans may edit them directly, but LLM agents must not edit, regenerate, migrate, copy, or reformat any README.md file unless the user gives express README-edit permission in the current task. sync_paper_status.py only refreshes paper-folder README entrypoints with --sync-readmes --readme-edit-permission; agents should use those flags only after explicit README instructions. The sync script defaults to tracked paper status files so untracked draft scaffolds do not pollute generated CI-facing tables; ordinary CLI checks and repository audits must not parse or enforce README content, because humans can edit README prose directly. Keep any README lint, quality check, or migration as an explicit opt-in maintenance command rather than a default CI gate. use --include-untracked only when intentionally syncing a new untracked paper scaffold. During routine proof iteration, do not run the status sync just because Lean LOC changed or a small proof seam was added; defer generated table/doc refreshes until a named paper result closes, a status note changes, a final report/handoff is prepared, or the user explicitly asks. If docs/site/table text is wrong, fix the paper-local status.json and rerun the sync script at that milestone; if README prose needs to change, wait for explicit README instructions. If a generated table needs display-only publication wording that differs from local provenance, use papers/catalog.json publication_overrides and leave paper-local source_version fields as the source/provenance record. If stale paper-local documentation or status is distorting the proof plan, causing closed work to be rediscovered, or could lead a human to stop the right proof campaign from an obsolete status belief, update the smallest non-README handoff/status fields immediately, and ask before editing README prose. Still defer repository-wide generated docs/site/table refreshes until the next real milestone unless those generated files are the misleading decision source. Keep sync_paper_status.py metadata-only and fast by default. It should not import dashboard code, run Lean previews, refresh LLM sidecars, or perform closeout checks unless an explicit opt-in flag such as --dashboard-audit is used. CI should run scripts/sync_paper_status.py --check as an early source check; if that step times out or fails before Lean, first suspect stale generated status or an accidental slow import in the sync path, not a proof failure. Use human_summary for the short public-facing note in generated tables. Formalized papers should usually have an empty summary; add text only for a reader-relevant source-version, proof-route, or caveat note. Human-review counts mean saved dashboard rows by a human reviewer over the curated source-facing review surface: reviewed_rows / total_rows. Do not use raw PaperInterface.lean declaration counts as human-facing dashboard totals when proof-support endpoints can be excluded with review_surface.include_names, assumption_names, or auxiliary_names. Agent source audits, validation reports, and compile checks do not increment human review. Website status tables should expose human review and row-local LLM-as-judge statement translation, not paper-level source coverage. Keep paper-level source-inventory coverage in validation reports, audit JSON, and docs/PAPER_STATUS.md; do not surface it as a public website table column. For a partial or conditional public entry, make human_summary one concise sentence: name the paper-facing results already closed and the exact remaining external/library/model certificate. Avoid Lean declaration names, helper-layer names, route history, and process words; a reader should understand the status from the source theorem labels and the mathematical boundary alone. If status.json includes human_summary_review.status = "human_approved" or "human_written", preserve the summary verbatim unless a human explicitly asks for that summary to be edited. Automation may require a nonempty summary for non-formalized papers, but it should not rewrite human-written or human-approved prose merely to shorten, polish, or normalize it. When doing an all-public-paper audit or syncing public status into the paper or website, derive the paper list from the active public checkout's tracked paper-local status.json files, papers/human_status.json, or the sync script output. Do not rely on a manually remembered list of "public papers"; selected public partials are easy to omit, and private/in-progress papers are easy to leak. Run the aggregate status sync in the checkout whose outputs will be committed, because private and public aggregate tables intentionally differ. If the command is run from the private incubator, still derive the public-paper audit set from the sibling public checkout. A broad private papers/status.json loop is useful for incubator triage, but failures on private-only papers are not public-release blockers unless those papers are intentionally being moved into the public repo. If the user asks for DAG regeneration, commit, or push at the next milestone, treat the milestone as a green named theorem seam plus the relevant targeted builds and hygiene checks, not as every helper alias. At that milestone, refresh only the affected DAG/status artifacts, inspect the rendered DAG if it changed, stage an explicit path list, commit once, and push without adding a routine rebase unless the user asked for one or a true publication/library milestone requires it. Do not churn status metadata during tight proof loops. Treat status syncs as publication/checkpoint work, not as a per-build or per-proof maintenance step. Update paper-local status.json and run the sync only at coherent milestones: new scaffold intake, a theorem/status row changing, a review-surface change, a final report/handoff/publication pass, or an explicit user request. For ordinary proof edits, formula wrappers, small library lemmas, and compiler-fix iterations, rely on targeted lake build checks and update status once the batch has a stable boundary. This includes mechanical metadata such as line_count, declaration_rows, review_rows, total_rows, and review-slice lists: do not chase those counts after each interface helper or proof wrapper. Let them be temporarily stale during active development and reconcile them in a single pass at the next real review, report, commit, publication, or handoff boundary. If stale documentation or status metadata is actively distorting the proof plan, causing the agent to redo closed work, or likely to make a human shut down the right proof campaign based on obsolete status beliefs, update the smallest paper-local docs/status fields immediately. This is a proof-planning fix, not routine documentation churn; keep it narrow and defer generated aggregate syncs unless the changed field is the aggregate source of truth for the current decision. Keep broader human-facing document churn low for the same reason. During an active proof session, do not refresh READMEs, DAGs, final-validation reports, website tables, or public status summaries for every helper lemma or small interface wrapper. README files require express README-edit permission in the current task even at such a boundary. Batch non-README edits for real session boundaries, publication/checkpoint milestones, explicit user requests, or roughly once-a-day progress rollups. Short private scratch notes or paper-local handoffs are still appropriate when they materially help the next proof step; the constraint is on outward-facing documentation churn, not on useful working memory.

When a proof is blocked, think outside Lean as needed, patch the mathematical argument yourself, and then implement the patched proof in Lean. Do not stop at identifying the gap unless the target theorem is false or the needed assumption is mathematically indispensable.

If a paper proof is imprecise, think hard outside Lean to create a precise proof strategy, implement that strategy in Lean, and record the issue in a paper-local handoff, proof plan, status note, or README only with express README-edit permission in the current task. Carry it into the paper's final report only during the paper-done or user-requested post-validation pass. If a paper's printed finite constant appears wrong or under-justified, separate the exact finite claim from its downstream use. Prove and expose the corrected finite bound with the constant Lean can justify; document the sharper printed constant as a source deviation or conditional sharp bridge only if the exact finite result is itself a named target. If later paper results only need a vanishing/asymptotic bound such as O(1/N), route them through the corrected bound and say plainly that downstream consumers are unaffected by the finite constant discrepancy. Even when such a finite claim is a named theorem, lemma, appendix result, or preliminary proposition, do not let an inessential sharp constant block the paper's main theorem path. Prove the strongest corrected version justified by the source and Lean, expose it under a name that signals the correction, and document exactly how it deviates from the printed statement. Treat the printed constant as an open sharp variant only when a downstream result genuinely depends on that exact constant.

When the right proof strategy is unclear, think deeply outside Lean before editing. If a written scratch argument would help, create a short .txt, .tex, or .md sketch in the paper folder; keep it only as detailed as needed to unlock the Lean proof. Do not create a sketch when it would be ceremony rather than useful proof planning. After the strategy is clear, execute it in Lean and keep moving.

If a proof loop has produced several wrappers, adapters, or public aliases without shrinking the visible theorem assumptions, stop before adding another layer. Write or update a short outside-Lean plan that names the current target declaration, the theorem application that should close it, and classifies each remaining visible premise as a source assumption, a derivable row/lemma, a definitional surface mismatch, or a real semantic gap. Prefer proving the missing row-identification lemma or choosing the right concrete source surface over adding more wrappers. Resume Lean only after the plan names the next small build target and why each exposed premise should be discharged, bundled, or kept. For proof-facing certificates, "kept" is a temporary decision, not the default end state: either prove the certificate constructor now, expose the premise as a validated source assumption, or mark the exact source theorem partial. Do not start a new theorem while the current theorem still has an easy-to-state undischarged certificate or row hypothesis. Treat wrappers as proof progress only when the final paper-facing theorem type gets closer to the paper statement: fewer visible certificates, fewer unproved row hypotheses, or a more faithful source surface. If an already-stronger compiled endpoint exists under a secondary name, rewire/promote the public paper-facing alias before adding new helper layers. Use #check or a temporary scratch theorem to inspect the actual theorem type; do not infer remaining work from long declaration names or README prose alone. If #check shows that the remaining premises are exactly the paper's displayed source assumptions, do not try to "prove" them away by inventing a stronger model unless the paper claims that derivation. Treat them as legitimate theorem inputs. If the remaining premises are source-model identification rows that the paper derives in an appendix, make that row package the active proof boundary and name it explicitly. For appendix restatements such as "Theorem N (Theorem M)" or "Proposition N (Proposition M)", do not create a separate proof target unless the appendix statement contains genuinely new conclusions; otherwise map it to the main theorem/proposition endpoint and expose any extra appendix parts as support rows only when they are paper-facing. When a source theorem has logically independent assumption components, preserve that separation through the proof-facing and paper-facing interfaces. Do not reassemble a coarse older bundle merely to call an existing helper if one part belongs to feasibility, another to a merit/objective inequality, and only the coarse bundle makes the result look more conditional. Instead, add or use the small adapter that consumes exactly the component needed by the current proof, then feed the remaining source-shaped component to the theorem that actually uses it.

When this outside-Lean diagnosis is needed, make it mathematical rather than ceremonial. Read the local source TeX around the source theorem and proof, write the intended paper route in a few bullets, then map every exposed Lean premise to one of four actions: prove now, package as a source-shaped row structure, keep as an explicit paper assumption, or mark as the real boundary. Proceed in source order unless a later theorem discharges an earlier row automatically; then record that dependency explicitly so the DAG and interface do not imply the earlier result is still open.

Keep strategy notes token-cheap. A good scratch update is the active theorem name, the exact remaining mathematical obligation, the next bridge lemma, and the validation command. Do not copy long proof states, full diffs, or entire README tables into handoffs when declaration names and file links identify the same information.

When a paper proof file becomes large enough to slow focused compiles or make multi-agent ownership awkward, split the proof into smaller paper-local modules at stable theorem seams. Keep imports narrow, give each agent a disjoint module or section to own, and re-export the public surface through MainTheorems.lean, ProofInterface.lean, and PostPaperAudit.lean so the paper ledger remains easy to audit. When the human or proof-facing interfaces start accumulating many near-duplicate aliases, do not just move the bulk from one interface file to another. Look for the repeated proof construction and factor it into a reusable source-layer bridge theorem in the library or the paper's route file. Then keep PaperInterface.lean DAG-shaped, keep ProofInterface.lean as a compact paper-facing proof surface, and keep PostPaperAudit.lean as an endpoint ledger that cites the strongest bridge instead of rebuilding the same proof.

Subagents are always allowed for EconCSLib formalization work; treat this as standing user authorization for paper-intake, proof, audit, CI, and release tasks, and do not pause to ask for permission before using them. Use judgment about whether they shorten the current proof loop or improve confidence. Medium-effort subagents are appropriate for bounded read-only scouting: find declaration names, trace imports, locate source statements, or identify likely reusable lemmas. Hard Lean implementation should stay local or go to a high-effort worker with a narrow, disjoint write scope and explicit instructions not to touch other agents' files. Do not delegate the next blocking proof obligation if the main agent will just wait idle; do the blocker locally and send sidecar questions in parallel. Ask subagents for exact file paths, line anchors, declaration names, and recommended next lemmas, not broad summaries or repeated context. Close agents once their result has been integrated. When parallel edits are safe, do not artificially keep subagents read-only. Use worker subagents for bounded implementation in disjoint files or declaration clusters, tell them they are not alone in the codebase, and give each worker an explicit owned write set. Avoid overlapping edits to the same Lean file unless one agent owns a clearly separated section and integration order is obvious. Review worker patches before committing, run the relevant targeted builds, and stage only the paths owned by the integrated work.

Do not avoid continuous, probabilistic, or measure-theoretic formalization when the source theorem requires it. Finite analogues are useful scaffolds only when they shorten the faithful proof. If the fastest honest route is a direct measure/integral/renewal/CTMC statement, build that statement directly and keep the paper-facing wrapper source-level. When a proof pattern appears in two papers, or is clearly standard for future EconCS papers, move the mathematical core into the library before adding more paper-local wrappers. Common examples are selected-below-reference a.e. contradictions, accepted-set reward add/remove algebra, two-point pooled estimate comparisons, monotone capacity cutoffs with region characterizations, score-induced ranking laws, and ranking-law pushforwards from continuous random utility models. Keep theorem-numbered names in the paper file as thin adapters over those shared declarations. For continuous strategy/type-space games, treat strategy, equilibrium, best-response, uniqueness, policy-optimality, and indifference-boundary claims as almost-everywhere statements under the relevant type or information law by default, not as pointwise statements. Use a pointwise statement only when the paper explicitly needs pointwise behavior, the state space is genuinely finite/discrete, or the pointwise result is a stronger helper that is immediately bridged to the paper-facing a.e. theorem. If indifference cutoffs, support boundaries, or off-support types are null events, state the theorem a.e. and prove separate boundary-null/no-atoms lemmas rather than adding artificial pointwise tie behavior. Load references/proof-foundations-probability.md for measure-zero/boundary-null routes and references/proof-mechanism-design.md for Gaussian strategy-game a.e. equilibrium patterns.

When Lean exposes a contradiction or apparently false source statement, do not immediately mark the paper theorem false. Pause the Lean loop briefly: reread the source PDF/TeX around the exact theorem and proof paragraph, think through the intended mathematical statement outside Lean, write a short paper-local proof plan, and then implement the repaired route. If the source really appears to assert the false statement, surface that issue to the human before rewriting the theorem status; otherwise treat the correction as a faithful formalization repair and continue. Common repairs include replacing an over-strong pointwise claim by a law-level or almost-everywhere statement, adding a missing nondegeneracy/support assumption, separating a displayed formula from a derivation-corrected formula, or weakening an auxiliary abstraction while preserving the paper-facing theorem.

When source model assumptions are ambiguous, search beyond the local PDF before deciding whether a Lean field is a paper convention or an extra certificate. Look for public TeX/source archives, author-hosted PDFs, conference and journal versions, and source repositories. Record when no public TeX/source is found. Later versions may clarify conventions such as anonymity, tie-breaking, or masked-vector models, but do not silently switch the paper target to a later version. If the later version becomes the source of truth, update the paper identity, theorem inventory, numbering, DAG, status rows, and final report together. Update README prose only with express README-edit permission in the current task.

Keep theorem-specific proof tactics out of this always-loaded file. Use the reference routing table at the end: CTMC/reward-rate details live in references/proof-foundations-probability.md; dynamic-game/PBE certificate details live in references/proof-mechanism-design.md; market and social choice details live in references/proof-markets-social-choice.md. Do not present a finite source-event, finite schedule, trace/replay, or strict-realized-profile equilibrium endpoint as a full continuous type-distribution PBE theorem. Such endpoints can be useful source-facing partial progress, especially when they expose the named strategy, exact trace, and outcome/payoff equality, but the full source theorem remains partial until the continuous type law, belief consistency, global PBE semantics, and