Section 3, “Quantised inference and deployment constraints”The proof needs nonnegative literal weights, bounded thresholds and Boolean states, not just a quantisation format
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
Quantised inference and deployment constraints. Low-bit inference motivates studying bounded numerical resources (Jacob et al., 2018; Dettmers et al., 2022). Our constant-witness proof additionally requires nonnegative literal weights, bounded thresholds and Boolean intermediate states. These are explicit mathematical assumptions, not properties inferred merely from a quantisation format. Standard signed linear layers and scale-adaptive normalisation are outside the theorem unless separately reduced to the permitted gates.
Generated from paper_jmlr.tex, lines 385–386.
2 Explain this
Low-bit inference is the practical motivation, but the theorem needs more than a low-bit format: nonnegative weights on Boolean literals, bounded thresholds and Boolean intermediate states. These are mathematical assumptions, not consequences of using INT8. Standard signed linear layers and scale-adaptive normalisation are outside the theorem unless reduced to the permitted gates.
3 How this is formalised
A statement of scope. The assumptions it lists are exactly the hypotheses of Theorem 2.4 and the validity condition of Definition A.1.
| Paper anchor | par-quantised-inference-and-deployment-constraints-p1 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 3, “Quantised inference and deployment constraints” |
| Claim | The proof needs nonnegative literal weights, bounded thresholds and Boolean states, not just a quantisation format |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 385–386; SHA-256 of the normalised block source 7b9c887654f17fed… |
| Depends on | Theorem 2.4 |
| Explanations | explain/c-rw-quant, formal/c-rw-quant |
| Build evidence | fresh isolated rebuild, audit report |
4 Lean statement and source
No Lean statement corresponds to this claim. This is interpretation or motivation, not a formal mathematical claim.
Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).