Governed human-agent research loops for mathematical physics: preregistration, locked checkers and formal proof as the operating system of AI-assisted discovery (Paper I: the method)

We describe, in operational detail, the method used in a three-week research programme in which one human principal investigator directed two large-language-model research agents on an open-ended problem in mathematical physics: whether a single positive-geometry structure can fix a dimensionless Standard-Model quantity with zero fitted parameters. The paper is about the approach, not the physics. Work is cut into small units ("rungs"), each passing through a fixed loop: question, first principles, Lean 4/Mathlib definitions, simulation, predictions and refutation criteria written before any run, a preregistration pushed alone and hashed, locked and hash-pinned checkers tested on planted and deliberately broken cases, blind targets, seeded manifests that keep negative results, and a review with a steelman critique. Every claim carries one epistemic tag (Lean-proved, paper-proved, simulated, cited, conjecture, speculation). Locked files are superseded, never edited, and history is fast-forward only. An exploration budget and a failure-mode taxonomy counter the greedy drift of an autonomous agent, and a convention-invariance rule makes every no-go final only after a re-check in a proved-equivalent convention. From the repository itself we report counts of commits, preregistrations and reviews, with no review preceding its preregistration, and a Lean library at 1,378 theorems with zero non-standard axioms. A pilot tests whether Lean statements say what the prose claims. We close with threats to validity, a steelman critique of agentic research, and an outline of Paper II, which reports the physics evidence.