{"id":"ae566b28-9d5b-4bd3-bd9e-65df2f72f103","arxiv_id":"2607.23390","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"partial","parameter_count":3,"one_line_summary":"For a fixed low-bit residual library, the distance to the closed relaxed reachable set is an exact structural floor that pure depth approaches at O(1/D), while write-back arithmetic can reverse the gain and accuracy matching needs D=Θ(L).","lead":"Depth can stand in for missing numerical precision in residual neural computation only when the operation library, execution arithmetic, and routing model allow it. The paper gives a resource theory that separates structural floors from finite-depth cost and from hardware that can freeze updates.","discovery_kind":"unification","skeptic_critique":{"model":"moonshotai/kimi-k3","headline":"The theorems appear conditionally sound; the common verified execution tube is the principal bridge that may fail for deployed attention systems.","rationale":"This is the same load-bearing condition identified by the reader. The proof chain uses it exactly where expected: balanced switching controls schedule discrepancy, Abel summation and Gronwall propagate field variation, and the arithmetic and integrated resource theorems assume common-tube schedulewise defects. I do not see an internal inconsistency in those deductions. The Lean artifact strengthens the exact discrete arithmetic core, but it does not verify the continuous neural tube, and the DistilBERT experiments are diagnostic rather than a sound enclosure. Thus the concern is external applicability rather than a demonstrated correctness failure. The reader’s CONDITIONAL verdict already prices this obligation, so no verdict adjustment is warranted.","tokens_in":58397,"tokens_out":9642,"duration_ms":102967,"concrete_test":"For one declared pre-normalized Transformer residual block and low-bit library on a compact input set, compute a sound differential-inclusion enclosure of all ideal relaxed/mixed/pure prefixes using interval/CROWN or MILP bounds, then add exact integer range propagation for write-back and carry arithmetic. Choose K with positive margin and Kρ; interval-bound Jacobians to obtain B, Lz, Lt/Vt and verify ηG, ρ, saturation, and no-overflow on Kρ across several depths. A D-independent certificate discharges the concern for that deployment; tube escape or D-growing bounds means the master law fails as stated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Assumption 1 is not a mild regularity condition. It simultaneously asserts a forward-invariant tube for every measurable relaxed control, mixed/pure Euler state, interpolation segment, and—through Theorems 6, 8, and 29—every implemented finite-arithmetic prefix, together with uniform field, Lipschitz, and temporal bounds. In attention blocks, QK products make Lipschitz constants state-range dependent, LayerNorm contributes sensitivity through its normalization radius, and wrapping or overflow can leave a tube that was invariant only for ideal arithmetic. If no fixed K and enlarged Kρ with D-independent constants exists for the declared architecture, C_syn/D is not a valid synthesis radius and the master-law and D=Θ(L) conclusions do not apply. This is not an internal proof gap: the paper states the hypothesis and calls its audit mandatory. It is, however, the least secure step from a conditional resource theory to a practical replacement law.","agreement_with_reader":"agree"},"referee_report":{"model":"moonshotai/kimi-k3","summary":"The paper develops a target-specific resource theory for when low-bit residual depth can replace numerical precision. A depth-D student is modeled as a pure schedule over a declared low-bit residual-field dictionary on a fixed horizon, with the state lifted to the full input-indexed map. The distance from the target to the closed relaxed reachable set is identified as the exact structural floor; pure schedules approach it at O(D^{-1}) under bounded-variation time dependence and O(D^{-ϑ}+D^{-1}) under ϑ-Hölder dependence (Theorems 3, 5). Execution arithmetic is shown to change the phase: full-state write-back contributes a Dρ_z certificate term with an exact scalar freeze result (Proposition 7), while increment error feedback telescopes the carry (Theorem 8) and admits a bit-exact common-lattice realization with explicit register widths (Proposition 9). A fixed, D-independent binary teacher has a closed-form optimal error Θ(D^{-1}) (Theorem 10), lifted to residual-ReLU and nonuniform two-token attention realizations (Proposition 12, Theorem 13), yielding D_match = Θ(L) for coherent first-order comparators (Corollary 15). Learned codebooks add a metadata resource with upper, packing, and allocation laws (Theorems 18, 19, 57); state-dependent routing is treated by a transversal-event small-gain theorem (Theorem 23). A primal–dual stack (HJB, support, affine, occupation-measure/SOS) yields feasible/impossible/unresolved decisions (Corollary 28). Companion software (QReplace) and","tokens_in":58705,"tokens_out":9442,"duration_ms":361140,"significance":"If the results hold, the paper supplies a unifying conditional framework that cleanly separates library geometry, synthesis depth, metadata, execution arithmetic, and routing — resources that the literature often collapses into a nominal bit width. Several strengths deserve explicit credit: (i) an exact closed-form fixed-teacher optimum with a nonasymptotic envelope (Theorem 10), making the first-order depth price sharp for one fixed target rather than only minimax; (ii) a Lean 4 artifact with hash-locked build logs and claim-level axiom audits kernel-checking twelve discrete-core statements, plus exhaustive executable verifiers for the attention converse and common-lattice arithmetic; (iii) a certified nonlinear matrix-valued accuracy-matching depth (D_match = 8 = 2L) proved by rational piecewise-affine bounds, with a prospective falsifiable prediction (calibrated D=9 vs certified 8) that was checked; (iv) an explicit evidence hierarchy and trust-boundary discussion that is more disciplined than typical for this area. The component tools (relaxed controls, sigma–delta feedback, occupation measures, hybrid transversality) are mature, and the paper says so; the contribution is the t","major_comments":[{"comment":"The common synthesis tube is the load-bearing bridge for the master law (1) and for every QReplace verdict, and it carries a bootstrap risk the manuscript should address more directly. Assumption 1 simultaneously asserts forward invariance of K for all measurable relaxed controls, all mixed/pure Euler states and interpolation segments, and — via Theorems 6, 8, and 29 — all implemented finite-arithmetic prefixes, together with uniform B and L_z on the enlarged tube K_ρ. For attention blocks, the QK-product Lipschitz constant is state-range dependent (§9.2.2 bounds scores through B_Q, B_K), so the constants that define the tube are valid only on a tube whose existence is part of the hypothesis. The paper resolves this constructively for the contractive soft-threshold class (§9.1, Eq. (197) gives an explicit invariant ball), but the Transformer specialization provides only componentwise err","section":"§3.2 Assumption 1; §9.2–9.3; Theorems 6, 8, 29"}],"minor_comments":[{"comment":"The main text flags that primal–dual equality requires a 'closed-image qualification detailed in Appendix A; that qualification is not automatic.' Please clarify in the main text that this qualification affects only the no-duality-gap statement, not the validity of dual lower certificates: Theorem 25 is proved directly by monotonicity along trajectories, so Corollary 28's 'certified impossible' verdicts do not depend on strong duality. As written, a reader could over-discount the decision rule or, conversely, over-credit the SOS hierarchy.","section":"§8.5, Theorem 27"},{"comment":"The phrase 'causal validation of the theory's central distinction' is stronger than the design supports. The coherent-target arm (depth-D Euler refinement converging to the depth-32 refinement of the same field) is essentially standard Euler convergence and is expected a priori; the informative arm is the direct-target divergence. The 4-bit study uses three QAT seeds, so the Student-t intervals have two degrees of freedom, and the layer-1 hidden-map interval crosses zero (reported, but only mid-paragraph). Please temper the causal language, state what outcome would have falsified the mechanism, and note that the fitted slopes (−1.16, −0.86) come from five depth points.","section":"§10.8"},{"comment":"Notation drift: the appendices use C_{fh,b} and C^{unif}_{fh} where the main text uses C^{end}_{syn} and C^{unif}_{syn} (e.g., Theorem 30 vs. Theorem 3; Theorem 53 vs. Theorem 18). Please harmonize or add the correspondence to Table 3. Similarly, Φ_L(T) is defined twice (Eq. (14) and after Eq. (270)), and Eq. (65) uses u = D^{-1} in the main text but x = 1/D in Appendix A.2.","section":"Appendix A vs. main text"},{"comment":"QReplace is described in §1.4 as returning five outcomes (certified feasible, certified impossible, conditionally feasible, diagnostically promising, unresolved), while Corollary 28 defines a three-way decision. Please state the mapping between the two lists and which outcomes are proof-backed versus heuristic.","section":"§1.4 vs. §8.7"},{"comment":"The write-back term Dρ_z is a worst-case certificate envelope; the only exact freeze result is scalar (Proposition 7). The text acknowledges this, but the 'phase diagram' framing of Figure 2(a) may be read as asserting realized U-shaped behavior in general architectures. A sentence clarifying that no multidimensional lower bound realizing the Dρ_z growth is known would calibrate Claim 3.","section":"§4.2, Figure 2(a)"},{"comment":"The α_k√q/2 term assumes a coordinatewise uniform activation grid in a q-dimensional Euclidean state; please state this explicitly, since the surrounding development is in the lifted Banach space Z.","section":"Eq. (36)"},{"comment":"A substantial fraction of the citations are 2025–2026 arXiv preprints (e.g., Chakrabarti et al. 2026; Park et al. 2026b; Zhao et al. 2026). Please indicate which are peer-reviewed and pin versions, since several novelty-boundary comparisons depend on them.","section":"References"}],"recommendation":"minor_revision","confidential_remarks":"This is a single-author, monograph-length manuscript with a very large appendix apparatus; the editor may wish to consider format fit and whether the QReplace/QReplaceLean supplements will be archived with the paper. I could not verify the 2026-dated citations or the Lean build logs from the text alone; spot-checks of the core proofs (Theorems 3, 8, 10; Lemma 2; the LayerNorm/softmax bounds in §9.2) were internally consistent. The AI-assistance disclosure is present and appropriately scoped. My one substantive reservation is the tube hypothesis flagged in the major comment; the authors are transparent about it, so I regard the requested revision as a calibration of claims rather than a defect in the proofs."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The one thing worth knowing: this is a real theory paper, not a slogan paper. It defines the structural floor as distance to the closed relaxed full-map reachable set of a declared low-bit library, proves pure schedules approach it at O(D^{-1}) (BV) or O(D^{-ϑ}+D^{-1}) (Hölder), shows full-state write-back can add a Dρ_z freeze while increment error feedback keeps a bounded carry and a common-lattice identity, and gives a fixed-teacher converse that forces D=Θ(L) for coherent first-order comparators. That package is new as a target-specific resource law even though the ingredients (relaxed controls, sum-up rounding, sigma-delta, hybrid transversality, occupation measures) are mature and honestly cited.\n\nWhat it does well is scope and evidence hygiene. Constants are explicit; appendices carry the proofs; Lean is claimed only on the discrete core (freeze, conservation, registers, decision implications, teacher/attention algebra), not on the whole continuum theory; pretrained DistilBERT work is labeled diagnostic; the feasible/impossible/unresolved rule is the right interface before training. The write-back vs error-feedback phase diagram and the exact binary-teacher optimum are the parts I would actually reuse.\n\nSoft spots, in proportion. Assumption 1 (common verified tube with uniform bounds for ideal, mixed, pure, and implemented prefixes) is load-bearing. Attention Lipschitz constants and LayerNorm sensitivity are state-range dependent; overflow can leave an ideal tube. The paper says the audit is mandatory and does not pretend otherwise, so this is a conditional-theory boundary, not a circular proof. Pretrained evidence is thin by design. Master-law constants are library- and tube-dependent—as they must be. None of that sinks the math under the stated hypotheses.\n\nWho it is for: people who already think in residual flows, unrolling, PTQ arithmetic, or MoE routing and want a common language for when depth can and cannot buy precision. Not a drop-in recipe for arbitrary Transformers without the tube and arithmetic checks.\n\nI would send it to referees. Engage if you work on quantized residual systems; skim the synopsis and §§3–5,8 if you only need the decision rule.","headline":"Conditionally sound resource theory that cleanly separates structural floor, pure-depth synthesis, arithmetic phase, and pre-training certificates; the tube hypothesis is the real bridge to practice, not a hidden proof gap.","tokens_in":59482,"tokens_out":564,"would_cite":true,"duration_ms":13768,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.5","headline":"Depth can replace missing numerical precision only relative to a declared low-bit library, horizon, execution arithmetic, and routing model—and a structural floor no amount of depth can cross.","keywords":["quantized neural networks","depth–precision tradeoffs","residual networks","relaxed controls","error feedback","structural floor","mixture-of-experts routing","reachability"],"falsifier":"Find a fixed target and declared low-bit residual library whose structural floor is zero, with coherent first-order high-precision error, yet whose best pure low-bit schedules either stay bounded away from the floor as depth grows or match the high-precision accuracy with depth growing much slower or much faster than linear in the comparator depth—under the paper’s execution and tube assumptions.","tokens_in":59376,"feed_emoji":"📉","tokens_out":1098,"duration_ms":20629,"temperature":0.7,"pith_summary":"This paper asks when stacking more low-bit residual steps can stand in for the numerical precision a network is missing, for a fixed input–output map. It treats a quantized residual network as a pure schedule that picks fields from a declared low-bit operation library over a fixed horizon, and characterizes the infinite-depth limit by relaxed controls. The distance from the target map to the closed relaxed reachable set is an exact structural floor: no optimizer and no extra depth can remove it for that library. Pure schedules approach the floor at a first-order rate under ordinary time regularity, but execution arithmetic can reverse the story—full-state write-back can freeze residual updates—while increment error feedback keeps a bounded carry and an exact lattice conservation law. For coherent high-precision comparators with first-order error, matching accuracy forces student depth to scale linearly with teacher depth. Primal and dual certificates can mark a design feasible, impossible, or unresolved before training.","feed_headline":"Depth replaces precision only up to a hard structural floor","feed_subtitle":"Low-bit residual depth hits a library-specific limit; bad arithmetic can freeze updates entirely","key_machinery":"The structural floor E_Ω,∞(F★): the distance from the target full map to the closed relaxed reachable set of the declared low-bit dictionary family. It separates what the library can express from what finite pure depth, metadata, arithmetic, and routing cost; pure schedules approach it by balanced switching / online simplex rounding, and verified primal–dual bounds turn the floor plus finite-resource radii into feasible / impossible / unresolved decisions.","core_discovery":"For a fixed target map and a declared low-bit residual library, the exact asymptotic limit of infinite low-bit depth is the distance from the target to the closed relaxed reachable set generated by that library. That distance is a structural floor no pure schedule can cross. Finite pure depth approaches the floor at rate O(1/D) under bounded-variation time dependence (and a Hölder-adjusted rate otherwise), but only when residual increments remain numerically visible; full-state write-back can add a growing penalty and freeze updates, while increment error feedback replaces that growth by a bounded carry. When a coherent high-precision comparator also has first-order error and the floor is ze","pith_inferences":["Quantization toolchains could add a pre-training screen that brackets the structural floor and rejects libraries whose dual bound already exceeds the tolerance.","Hardware paths that quantize the full residual state each microstep are in a different phase from increment-carry designs; kernel choice may matter as much as nominal bit width.","The same floor-plus-radius logic could grade looped or unrolled blocks: only refinements that stay coherent with a shared residual horizon earn a depth–precision exchange.","Unresolved certificates become a research queue of their own—pointing at which bound (floor, arithmetic, or route) must tighten next rather than treating failed training as non-representability."],"forward_implications":["Before training, a dual lower bound above the tolerance certifies that no depth or optimizer can hit the target with that library.","Full-state activation write-back can make deeper low-bit nets worse; preserving residual increments (e.g. error-feedback carry) is required for depth to help.","Accuracy matching against a coherent first-order high-precision teacher forces low-bit depth on the order of teacher depth when the floor is zero.","Learned codebooks must be charged as metadata separate from schedule depth; logarithmic metadata bits can keep codebook error commensurate with first-order synthesis.","Hard routing only keeps a first-order depth law under isolated transversal events and a small-gain route–state loop, not under a frozen positive margin alone."],"fun_headline_variants":["Low-bit depth hits a hard floor no schedule can cross","Infinite residual depth still can't beat the library floor","Depth replaces precision only inside a declared operation library","Structural floor bounds what low-bit residual depth can achieve","Relaxed reachable set sets the exact limit of quantized depth"],"cache_read_input_tokens":49280,"weakest_assumption_plain":"Everything ideal and implemented must stay inside one verified tube where the residual fields stay bounded and Lipschitz, so the theory does not cover attention or normalization that blow up, or arithmetic that overflows that tube.","fun_headline_variants_meta":{"raw":{"variants":["Low-bit depth hits a hard floor no schedule can cross","Infinite residual depth still can't beat the library floor","Depth replaces precision only inside a declared operation library","Structural floor bounds what low-bit residual depth can achieve","Relaxed reachable set sets the exact limit of quantized depth"]},"model":"grok-4.5","effort":"low","cost_usd":0.003657,"raw_usage":{"total_tokens":1260,"prompt_tokens":867,"num_sources_used":0,"completion_tokens":60,"cost_in_usd_ticks":36568000,"prompt_tokens_details":{"text_tokens":867,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":333,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":867,"tokens_out":60,"duration_ms":5859,"temperature":1.0,"reasoning_tokens":333,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-30T23:29:41.500477+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Find a fixed target and declared low-bit residual library whose structural floor is zero, with coherent first-order high-precision error, yet whose best pure low-bit schedules either stay bounded away from the floor as depth grows or match the high-precision accuracy with depth growing much slower or much faster than linear in the comparator depth—under the paper’s execution and tube assumptions.","supporting_citations":[],"review_version":1}