Friction check: Formal-only gates have distinct admission and warrant limits
Note: kb/notes/unformalized-improvements-need-a-pre-formal-stage-in-the-loop.md Central claim (one sentence): In loops over externally interpreted theories, a formal-only gate's symbolic input language imposes an admission limit distinct from its oracle's warrant limit; upstream translation or alternative formal prototypes can move candidates past admission, but proof inside the surrogate still does not by itself establish source fidelity or world fit.
Filter
Verdict: SURVIVES
One coherent arrangement satisfies all of those properties at once: the gate directly accepts only symbolic candidates; an outer translator or prototype process can present a surrogate or a family of surrogates; and separate work still remains to show that any admitted surrogate matches the source theory and the world. Lower formalization cost changes where revision happens, not the distinction between admission and warrant.
Signal — thinnest joints
- “The gate's input language therefore bounds direct submission, not the semantic reach of the loop around it.” — UNSUPPORTED — A translator can feed the gate a surrogate, but that alone does not show the surrounding loop reaches the same semantic candidate rather than a replacement chosen by the translator. The note needs a criterion for when surrogate generation preserves candidate identity strongly enough for “reach.”
- “Either route can restore reach.” — UNSUPPORTED — Resolving ambiguity into one determinate surrogate may discard live alternatives, and emitting a family or disjunction preserves them only syntactically unless the loop can evaluate correspondence among those variants. The move from admissibility to restored reach is asserted faster than shown.
- “Partial specifications, competing formal models, and conjecture-and-counterexample processes can also preserve alternatives and support revision after formal representation.” — THIN — This is plausible, but the note does not show which alternatives these media preserve, how they avoid premature commitment, or what criticism operation inside them plays the role that prose revision played a sentence earlier.
- “If the dependency's meaning or boundary is unsettled, the loop needs a way to criticize those choices before fixing one revised surrogate.” — THIN — Unsettled meaning shows that interpretation work remains, but not that it must occur before a surrogate is fixed rather than through iterative surrogate proposals plus external evidence. The note needs to say what failure mode makes pre-fix criticism architecturally necessary here.
- “When the candidate language preserves the relevant alternatives and the oracle returns discriminating counterexamples, formal iteration can help settle the concepts rather than merely encode a settled result.” — THIN — Discriminating counterexamples can help choose among formal variants, but the note does not show that this process settles the underlying concepts rather than selecting among already-imposed projections of them.
For the human
Look first at the jump from “a translator or formal prototype can present something admissible” to “the surrounding loop has restored semantic reach”; that missing concretization weakens both the translation section and the later claims about revision inside formal representations.