Premise decomposition: Reaching unformalized improvements needs a pre-formal stage somewhere in the loop

Note: kb/notes/unformalized-improvements-need-a-pre-formal-stage-in-the-loop.md Register: claim Central commitment (one sentence): An improvement loop can reach an externally interpreted theory whose concepts are not yet settled enough for a faithful final formalization only if, somewhere before formal representation, it has a stage able to criticize, revise, and reject that theory; moving translation upstream or making formalization cheap cannot remove the stage.

Premises and counterexamples

1. For an improvement that begins with unsettled concepts, mere reachability requires a pre-formal component able to criticize, revise, and reject it; direct generation and later formal selection cannot suffice. — DEFEATED — Consider a scheduler-model grammar that permits capacity to depend on any observed load signal: a generator enumerates formal models, and an exact trace oracle retains the model in which another process's load predicts failures. The initially unsettled “shared resource” improvement is reached without any component criticizing, revising, or rejecting it before formal candidates exist; rejection occurs only after generation. — GLOBAL — instance
2. An externally interpreted theory's concept boundaries must stabilize before any formal representation can carry those concepts in a form that supports criticism and revision. — DEFEATED — In Angluin's L* learner, the latent state partition of a black-box system is unsettled while the learner repeatedly proposes formal automata and uses counterexamples to split and revise the represented state classes. A person can read each automaton as a nonbinding behavioral theory of the system, yet concept stabilization happens through a sequence of already-formal conjectures. — GLOBAL — instance
3. To count as reaching an unformalized improvement, the loop must preserve the identity of the prose-born candidate through translation; independently discovering an extensionally equivalent formal theory does not count. — DOUBTFUL — A causal-structure search over scheduler traces can introduce an unnamed latent common cause and thereby recover the predictive content of “failures come from an unrepresented shared resource” without ever consuming that prose candidate. Whether this is the same improvement or a replacement depends on a candidate-identity rule the note leaves open explicitly. — GLOBAL — instance
4. Every route that translates one unsettled natural-language theory into formal candidate space must resolve its ambiguity through a pre-formal stage that can reject the source, rather than preserve the ambiguity for formal evaluation. — DEFEATED — A translator can mechanically emit a formal disjunction of fixed_capacity, time_varying_capacity, and capacity_dependent_on_other_load, rejecting none; a trace checker can then eliminate alternatives after the disjunction already has assigned symbolic consequences. The interpretive choice is deferred into formal candidate selection, so translation need not instantiate the required pre-formal rejection-capable stage. — GLOBAL — instance
5. A gate whose input language is exclusively programs and proofs cannot directly admit a natural-language theory that has no encoding in that language. — HOLDS — Treating the text as an uninterpreted byte string admits the string but not its theoretical content; giving the gate a human or language-model interpreter changes the gate, while giving it translated axioms supplies a formal surrogate rather than the unrepresented theory.
6. Turning a genuinely ambiguous natural-language theory into one single, determinate formal surrogate necessarily adds semantic choices that the source does not entail. — HOLDS — A controlled language with fixed semantics would avoid the ambiguity but falls outside the premise, and a disjunction or family of translations postpones the choice rather than producing one determinate surrogate; no case was found in which one fixed surrogate preserved mutually incompatible source readings without selecting among them.
7. A proof or check of consequences inside a formal surrogate does not by itself establish that the surrogate faithfully captures the externally interpreted source theory or the world it describes. — HOLDS — Exhaustive checking over a finite observation interface can establish behavioral equivalence on that interface, but the interface, measurements, and adequacy criterion already encode correspondence commitments; the internal proof remains conditional on those mappings rather than proving them from the external theory alone.
8. Even when artifact construction, proof generation, and checking become cheap, an unsettled theory's concepts cannot be settled by a formal conjecture-and-counterexample cycle, so cheap formalization can shorten but never eliminate the pre-formal interval. — DEFEATED — An exact active-automata-learning setup cheaply constructs a formal state-machine conjecture, receives a counterexample from the target system, and refines the state partition until the behavioral concepts stabilize; all criticism and revision occur after the first formal representation. Cheap formal iteration is the concept-settling stage in this bounded case, not merely a downstream consumer of already settled concepts. — GLOBAL — instance

For the human

Look first at premise 2: formal conjecture-and-counterexample learning provides a scoped case in which externally read concepts stabilize through already-formal theories, so the claimed temporal boundary needs a narrower domain than “unsettled concepts.”