Skill

Research method

These are one project’s rules, earned over a research programme that pairs written documents with a machine-checked library; each is contestable, a project adopts them by installing this skill and keeps what fits, and the incidents behind them stay in that programme’s log, which is not public.

Review

• A structural pass and a correctness pass find disjoint defect classes; a section is reviewed only after both.
• The citation discipline applies inward: open the exporting statement before citing it, even when it sits three paragraphs up in the same file.
• A correction reaches every summary site — the headline, the abstract, the registry, the companion prose — not only the detailed site where it was found; the project binds the list.
• A scope qualifier sits on the claim, not on the sentence’s conclusion.
• A negative-coverage sentence (“nothing in this work does X”) is a claim about every document at once; its counterexample is usually a companion’s own headline result under a hypothesis — and every landing re-reads such sentences for the landed result’s kind, since no gate does.
• A sentence found false of the artifact is corrected by the session that finds it, at its exact size, in that session; it is never put to the project’s owner as a choice. The owner decides scope and significance; whether a false sentence stands is not a decision. A project whose instructions file says the owner is asked before any correction has opted out, and the session then puts the sentence, its evidence and the correction to them instead.
• Crediting the work with settling a NAMED external result requires reading that result’s primary source first — its quantifiers, its resources and the author’s own caveats; a partial match names the special case proved and the gap.

Evidence

• A counting or closed-form claim gets its planted-defect probe in the same round it is made.
• Unverified code is not evidence; a numerical check a reader would need is an argument for checking it mechanically, not for shipping the script.
• Suspect the bound, not the witness: a residue that keeps coming out wrong is a fact about the bound until the bound has been pushed.
• A row or a remark about a checked artifact is written from the landed artifact, never from the design record that commissioned it.
• A record paraphrase can name the wrong referent; agreement between two citations is not verification — open what they point at.
• A whole-tree count (declarations, guards, modules) is a tree-derived figure: recomputed by a check at every occurrence, stated in the fewest places, never copied into a memory.
• A declaration name in a document is a claim that the declaration exists with that statement; a document never names a declaration in order to say it does NOT exist, since the check that resolves names cannot tell assertion from denial.

Before pricing a target

• Check what structure the target already carries before pricing a replacement into it.
• A label or category tag is a filing address, not a statement.
• An item’s own pointer can be the stale thing, or born wrong.
• Existence is the cheap half: check what CONSUMES the object before pricing its existence.
• Checking a target’s inputs is not checking what the project already derives from them.
• An equivalence proved about a hypothesis does not discharge it.
• When a bill misbehaves, ask of each term who holds it and whether it is a count or a clock.
• A parking reason can be priced against the wrong object; the cheapest check is the document’s own definition.

Changing the target honestly

The freedom is of route: on a wall, change the statement, the definition, the object or the currency to reach the goal. These invariants keep that honest.

1. The original question stays on record. Beside the result, write the statement before, the statement after, why, and whether the original is now settled, still open or refuted. An original open is never deleted by a change; it is answered, re-parked with the new reason, or marked refuted.
2. A change is not a settle. A result proved after a change is registered as a result about the changed statement; its status label, its verification row and every summary site name that statement, and no sentence claims the original was settled unless the change is shown equivalent or stronger.
3. Weakening is disclosed where a reader looks first. A change that adds a hypothesis, narrows a class or swaps a currency is carried at the headline, the abstract, the status label and the contributions, not only in an appendix row.
4. Every consumer is swept in the same session. A changed definition or statement reaches every document, registry entry and docstring that cites it before the commit; the project binds the audit that checks this.
5. Evaluation is fixed before the result. Probes, sweep sets, kill criteria and named hypotheses fixed for a round are not altered after seeing its result; changing them opens a new round with its own record. A probe that now passes because the statement moved is re-derived against the moved statement and says so.
6. A change that drops the interesting property is a finding, not a route. When the provable form loses what made the question worth asking, record “the natural statement is unreachable or false; the provable form is X” and keep the natural statement open.
7. No change to please a check. A statement is never weakened because a cited result lacks a mechanical proof, and never strengthened in prose beyond what the artifact proves; a named hypothesis with a citation is the honest form.

With a prover

Where the project pairs its documents with a machine-checked library, these rules decide which statement is proved next and when a target changes; the prover session’s own mechanics — the handoff, the landing, the sweeps — are the formal plugin’s.

• Statement-first: the statement is designed from the document’s actual text, opened, never from memory.
• Ties among formal targets are ordered by: what a document needs; statement readiness; the kind of effect on the document; elaboration risk; then how many rows move and how big the piece is.
• Check computability of what a construction reads before commissioning it; a search over an infinite object is a wall, not a target.
• A generic piece and a specific piece of one bundle carry the same quantification; a bundle lands sink-first — the composite statement nothing in the bundle depends on, with its predecessors’ statements as hypotheses, read back before any predecessor is proved — and each predecessor is computed at its edge parameters before dispatch.
• A refute-first computation at the smallest parameters precedes every handoff; a theorem with two or more hypotheses is commissioned with a non-vacuity witness beside it.
• A wall names its kind: expressivity (the statement cannot be expressed), elaboration (the prover cannot handle the term), missing-upstream (a needed library result is absent), misstated (the statement was wrong); a wall fitting none is a new kind, recorded.
• On a wall, change the target under the invariants above; another attempt that restates the object is tried before the wall is recorded as such.
• A repair loop against a failing build is bounded: three attempts, then stop and report the wall honestly with its error blocks trimmed to what matters.