Friction check: 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 Central claim (one sentence): An improvement loop that can reach externally interpreted theories whose concepts are too unsettled to formalize must include, somewhere before formalization, a stage that can criticize, revise, and reject those theories; moving translation upstream or making formalization cheaper does not remove that need.
Filter
Verdict: SURVIVES
The claim asks a loop to retain formal or proof-governed acceptance, admit theories whose concepts are not yet formalizable, and keep those theories revisable before they become operative. One concrete arrangement can hold these properties at once: an upstream, nonbinding stage works on the unsettled theory, and only its stabilized parts enter the formal gate.
Signal — thinnest joints
- “An improvement whose concepts are not yet fixed enough to formalize is reachable only if some stage can criticize, revise, and reject it before it has a formal representation.” — UNSUPPORTED — Being not yet formalizable establishes that something must change before faithful formalization, but it does not establish a distinct stage equipped with all three operations. The note does not exclude refinement through partial symbolic models, experiment-driven model revision, or candidate generation that yields a stabilized concept before submission.
- “The translator must decide what the prose commits to, resolve ambiguity, choose a boundary, and often revise the claim — pre-formal criticism, relocated upstream.” — UNSUPPORTED — Interpretive choice establishes that translation is not transcription, but it does not establish adversarial criticism or a capacity to reject the candidate. A translator can silently choose one surrogate among several without performing the rejection-capable stage the central claim requires.
- “But ‘capacity depends on what another process is doing’ changes the concept, not its value.” — UNSUPPORTED — The example does not fix a representation sharply enough to force that distinction. Another process could require a new causal variable or functional relation, but it could instead change the value of an already time-varying or load-conditioned effective-capacity parameter.
- “Formalization cost has parts — translating concepts into a model, building the artifact, generating a proof, checking it — and when the last three fall, formal models enter the prototype stage earlier and rival specifications become easy to compare.” — THIN — Lower construction, proof-generation, and checking costs support earlier executable artifacts once translations exist. They do not make rival specifications easy to compare when correspondence to the source theory, comparison criteria, or world-facing evidence remain costly.
- “What natural language contributes is narrower: it exposes unsettled commitments before a faithful formalization exists.” — THIN — Natural language can state commitments before formalization, but the preceding discussion does not show that it exposes rather than conceals them, or identify what exposure mechanism is unavailable to diagrams, partial formalisms, or other nonbinding representations.
For the human
Look first at the jump from unavoidable interpretive choices during translation to an architecturally necessary, rejection-capable criticism stage; that missing concretization supports both the necessity and relocation claims.