Premise decomposition: Formal-only gates have distinct admission and warrant limits

Note: kb/notes/unformalized-improvements-need-a-pre-formal-stage-in-the-loop.md Register: claim Central commitment (one sentence): For externally interpreted theories, a gate that directly reads only symbolic candidates imposes a distinct admission limit at its input language and a separate warrant limit after admission, because upstream translation can make a theory reachable without making internal proof sufficient to establish source fidelity or world fit.

Premises and counterexamples

  1. A gate whose direct candidate language is exclusively symbolic cannot directly evaluate the theoretical content of a candidate that is not expressed in that language. — HOLDS — Treating prose as an uninterpreted string or wrapping it inside a program admits a different candidate: bytes or an interpreter, not the prose theory as such.
  2. A candidate can satisfy a formal-only gate's representation requirements yet still fail its oracle because no proof or required evidence shows that adopting it is warranted. — HOLDS — A proof-gated self-modification loop can represent a rewrite as code while still lacking any proof under its fixed axioms that switching to it is better than continuing the search; representability and warrant come apart in the note's intended limiting case.
  3. Upstream translation or generation of formal surrogates can make a prose-born or otherwise non-symbolic theory reachable for the larger loop without changing what the gate directly admits. — HOLDS — The hardest case is an ambiguous source theory, but a translator can still emit one determinate surrogate or a family of surrogates; either way the gate still directly sees only symbolic candidates.
  4. When an ambiguous externally interpreted theory is translated into one determinate formal surrogate, some meaning-fixing commitment is made outside the gate's internal proof rather than justified by that proof. — HOLDS — A single surrogate can encode parameters or placeholders, but once it is determinate enough to be the thing proved, any unresolved source ambiguity has either been fixed upstream or intentionally carried as explicit alternatives rather than eliminated by proof.
  5. A proof or internal check over a formal surrogate establishes only consequences conditional on that surrogate's premises, not by itself that the surrogate faithfully captures the source theory's intended content. — HOLDS — A verified optimizer for the surrogate or an exhaustive theorem over it still depends on the earlier mapping from source commitments into surrogate premises.
  6. The same internal proof or check does not by itself establish that the surrogate's world-facing premises fit the external system or domain being modeled. — HOLDS — A scheduler model can be internally consistent and exactly implemented while still failing in deployment because an omitted shared resource makes one premise false.
  7. Lower artifact-construction, proof-generation, or checking costs can move more revision into formal candidate space, but those lower costs alone do not erase the separate need to justify translation fidelity and world fit. — HOLDS — Fast active learning or cheap theorem proving can refine formal conjectures earlier, but they still do not make an ambiguous source interpretation or an external capacity assumption true merely by being cheap to iterate.

For the human

No non-HOLDS premises surfaced; look first at premise 5, because if a surrogate's internal proof could by itself certify source fidelity, the admission/warrant split would largely collapse.