review_job_id: 8415
review_pair_id: 21085
note_path: kb/notes/unformalized-improvements-need-a-pre-formal-stage-in-the-loop.md
criterion_path: kb/instructions/critique-note.md
model_partition: codex
runner: /root/closing_job_8415
runner_model: gpt-5.4
runner_effort: xhigh
result_kind: report
outcome: null
completed_at: '2026-08-26T17:07:02+00:00'
Critique: Formal-only gates have distinct admission and warrant limits
Note: kb/notes/unformalized-improvements-need-a-pre-formal-stage-in-the-loop.md Central commitment: A formal-only gate's inability to directly read a theory is a limit distinct from its inability to warrant an admitted surrogate, and adding translation can broaden loop reach without making surrogate fidelity or world fit self-validating. Critique mode: claim Attack outcome: partially lands
Strongest case against it
The strongest objection comes from a formalist systems view: once a loop includes any translator, generator, or meta-representation layer, "admission limit" is not a distinct theoretical boundary but a restatement of how the loop was modeled. A proof gate never evaluates "the prose theory itself"; it evaluates formal candidates produced upstream. On that view, the real issue is whether the composite search space and oracle encode the right semantics, not whether an extra-form theory was directly admissible to one component. Program synthesis from natural-language specs, causal-model search, and families of formal surrogates already let revision continue after formalization, so the note risks reifying a gate-relative syntax fact into a deeper loop-level limit. Read that way, the file's older "pre-formal stage" framing looks overstated: no special pre-formal stage is needed, only some revisable surface somewhere in the loop.
How the note engages it
Partially engaged. The note answers most of the objection: the opening section defines admission as relative to the gate's input language, the translation section explicitly says loop-level semantic reach can exceed direct submission, and "Revisable candidate surfaces need not be pre-formal" rejects any privilege for natural language or any universal pre-formal requirement. The surviving issue is sharper object-language discipline. The note still slides between "candidate for the surrounding loop" and "candidate the formal gate can directly evaluate," which leaves room for a skeptic to say the first boundary is only bookkeeping unless that distinction is named more explicitly.
Constructive findings
- Distinguish "proposal candidate for the larger improvement loop" from "directly evaluable candidate for the formal gate" the first time "candidate" appears.
- State explicitly that admission limit is gate-relative and diagnostic, not a fourth global bottleneck on the whole loop.
- Reconcile the stale file slug with the note's narrower argument, or add one sentence noting that the claim does not require a pre-formal stage and only requires some revisable surface before commitments are fixed.
Secondary objections (optional)
- The Gödel-machine example is apt, but the prose-versus-program contrast can mislead readers into treating surface form as the core issue when the deeper constraint is warranted translation into evaluable consequences.
- The DiscoverPhysics ingest is already carefully limited, but because it does not establish the full rubric it adds little pressure to the main claim and could be cut without weakening the note.