Frontier coding models may spend substantial capacity learning not only program behavior, but also accidental entropy in human repositories. Such repositories contain valuable signals: tests, incidents, migrations, edge cases, product judgment, and operational history. These signals are entangled with framework churn, naming drift, generated-source ambiguity, dependency rituals, CI dialects, weak proof routes, and human-oriented review customs. We propose agent-first canonical code, a proof-carrying substrate that rewrites routine product software into canonical behavior profiles, typed change algebra, proof lanes, constrained edit grammars, semantic patch cells, runtime negative memory, and proof-carrying change objects. The core hypothesis is that quotienting software by behavior equivalence under a declared oracle can collapse equivalent encodings into governed representatives with explicit evidence and proof obligations. The endpoint is amortized cost per verified correct change, including source, context, reasoning, tools, verification, security, provenance, review, failed loops, defects, and foundry cost under a common oracle. Reported reduction bands are hypotheses, not measured frontier results. The proposed limit is a No-Accident Horizon: removable accident decreases until residual novelty, evidence, governance, risk, and future optionality dominate. For supported routine-product distributions, this gives a defensible planning target near 100-fold all-in cost reduction, not a guarantee for all software. Preliminary QLoRA experiments on Qwen2.5-Coder-14B show that 64,088 canonical trajectories are learnable and suppress tested forbidden-language markers, but do not establish behavior preservation, scaling economics, or verified-change cost. The contribution is a falsifiable program centered on minimum functional description length and verified-change cost.

翻译：前沿编码模型可能耗费大量能力，不仅学习程序行为，还学习人类代码仓库中的意外熵。此类仓库包含有价值的信号：测试、事件、迁移、边界情况、产品判断及操作历史。这些信号与框架更替、命名漂移、生成代码歧义、依赖惯例、CI方言、弱证明路径及面向人类的审查规则相互纠缠。我们提出智能体优先的规范代码，这是一种携带证明的基板，可将常规产品软件重写为规范行为概要、类型化变更代数、证明通道、受限编辑文法、语义补丁单元、运行时负记忆及携带证明的变更对象。核心假说是：在声明预言机下通过行为等价对软件取商，可将等价编码坍缩为受治理的表示，并附带显式证据和证明义务。最终目标是在共同预言机下，每个经验证的正确变更实现摊销成本，涵盖源代码、上下文、推理、工具、验证、安全、来源、审查、失败循环、缺陷及铸造成本。报告中给出的缩减区间为假说，而非实测前沿结果。所提出的极限是“无意外地平线”：可移除意外降至残余新颖性、证据、治理、风险及未来选择性占主导地位为止。对于支持的常规产品分布，这提供了约百倍全面成本降低的可辩护规划目标，而非适用于所有软件的保证。基于Qwen2.5-Coder-14B的初步QLoRA实验表明：64,088条规范轨迹可被学习，并抑制了测试中禁用的语言标记，但未确立行为保持性、规模经济性或已验证变更成本。本贡献的核心是可证伪方案，聚焦于最小功能描述长度与已验证变更成本。