Nucleus GraftingVerified Quantization-Aware NN Compression
When a neural network is quantized to INT8 for deployment, the set of representable activation values forms a finite Heyting algebra. The ReLU gate on this lattice is a nucleus operator — extensive, idempotent, and meet-preserving — and this structure necessarily introduces an irreducible information gap that decomposes additively into quantization, gate, and reconstruction components.
What happens to information when neural network activations are quantized? We show the answer is algebraic: the quantization gate is a nucleus on a Heyting algebra, and the Hossenfelder no-go theorem guarantees that a non-Boolean nucleus creates an unavoidable boundary gap. This gap decomposes additively, the gate component dominates (5–6× quantization), and bitwidth monotonicity is provable: coarser quantization means larger gap.
- • qRelu(z, q) = max(q, z) — proved extensive, idempotent, meet-preserving on {-128, ..., 127}
- • Product lattice non-Booleanity — canonical incomparable pair witness a=[0,1], b=[1,0]
- • Additive gap decomposition — total = quantization + gate + reconstruction (hAdditive)
- • Bitwidth monotonicity — activationFixedSet_mono: higher zero-point = fewer fixed vectors = larger gap
- • Non-Boolean boundary — graftBoundaryNucleus is never Boolean, connecting to Hossenfelder no-go
- • 3 model architectures — MLP, CNN, and autoencoder (NBA)
- • 65,536-pair exhaustive verification — zero nucleus axiom violations per layer
- • Gate dominance — gate component is 5–6× the quantization component
- • Bitwidth monotonicity confirmed — INT8 > INT16 > FP16 gap across all models
- • 74–96% gap optimization — via fp16_threshold_p10 method
- • α,β-CROWN bounds — neural network verification via auto_LiRPA
A mathematically principled theory of quantization loss. The gap decomposition tells you where information is lost (gate >> quantization) and the monotonicity theorem tells you how much you lose at each bitwidth. The optimization results show the gap is largely recoverable.
First verified connection between Heyting algebra nuclei and neural network quantization. The activationFixedSet_mono lemma and bitwidthFamily construction provide a template for formalizing other quantization-aware architectures.
Formal Verification Certificate
Sorry-free formalization with 2-round hostile adversarial audit. All findings remediated. Silver-tier TieredCertificate.
Nucleus Grafting • Lean 4 + Mathlib • Apoth3osis Labs