>_PROJECT.NUCLEUS_GRAFTING

Nucleus Grafting
Verified Quantization-Aware NN Compression

Original Research | Hossenfelder No-Go Connection | March 14, 2026

Overview

When a neural network is quantized to INT8 for deployment, the set of representable activation values $\{-128, \ldots, 127\}$ forms a finite lattice. The ReLU gate $\text{qRelu}(z, q) = \max(q, z)$ on this lattice is a nucleus operator on a Heyting algebra — extensive, idempotent, and meet-preserving. This means the gate necessarily introduces an irreducible information gap: the Hossenfelder boundary is non-Boolean, and the gap decomposes additively into quantization, gate, and reconstruction components.

We formalize this connection in Lean 4 (21 theorems, 4 modules, 298 lines, 0 sorry) and validate it empirically across MLP, CNN, and autoencoder architectures with exhaustive 65,536-pair nucleus axiom verification, bitwidth monotonicity confirmation, and 74–96% gap optimization.

Modules

4

Lean 4 files

Theorems

17

Machine-verified

Lines

298

Proof code

Sorry

0

Zero gaps

Models

3

MLP, CNN, Autoencoder

>_VERIFICATION.SEAL

Formal Verification Certificate

Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.

17 THEOREMS VERIFIED4 MODULES0 SORRY2 HOSTILE AUDITS

Nucleus Grafting • Lean 4 + Mathlib • Apoth3osis Labs

>_KEY.MATHEMATICS

Key Definitions & Results

Definition: Nucleus Operator

R : L \to L \quad\text{is a nucleus if:}\quad \forall x,\; x \leq R(x) \;;\quad R(R(x)) = R(x) \;;\quad R(x \wedge y) = R(x) \wedge R(y)

A closure operator on a Heyting algebra that preserves finite meets. The fixed-point subobject $L_R = \{x \mid R(x) = x\}$ is again a Heyting algebra.

Theorem: ReLU Gate is a Nucleus

\text{qRelu}(z, q) = \max(q, z) \quad\text{satisfies all three axioms on } \{-128, \ldots, 127\}

Verified by exhaustive enumeration (65,536 pairs) and proved in Lean 4 via max_min_distrib_right.

Theorem: Gap Decomposition

\Delta_{\text{total}} = \Delta_{\text{quant}} + \Delta_{\text{gate}} + \Delta_{\text{recon}}

The total information gap decomposes additively. Gate component dominates at 5–6× the quantization component. Formally enforced by hAdditive in GapDecomposition.

Theorem: Bitwidth Monotonicity

z_1 \leq z_2 \implies \text{Fix}(z_2) \subseteq \text{Fix}(z_1) \implies \text{gap}(z_1) \leq \text{gap}(z_2)

Coarser quantization (higher zero-point) means fewer fixed vectors and larger gap. Empirically confirmed: INT8 > INT16 > FP16 gap across all 3 models.

Corollary: Non-Boolean Boundary

\neg\,\text{isBoolean}(\text{graftBoundaryNucleus}(z)) \quad\Longrightarrow\quad \text{boundaryGap}(\emptyset) \neq \emptyset

The grafted nucleus is never Boolean — connecting to Hossenfelder's no-go theorem: a non-Boolean boundary necessarily has a nonzero gap.

>_PROOF.BLUEPRINT

Proof Modules

Each module can be expanded to show its definitions (mathematical notation) and verified theorems. Click to expand.

>_CORRESPONDENCE.TABLE

Lean Theorem ↔ Mathematics ↔ Empirical Evidence

Every formal theorem has a mathematical statement and corresponding empirical verification from the 5-phase experiment pipeline.

Lean Theorem	Mathematical Statement	Empirical Evidence
qRelu_extensive	$q \leq \max(q, z)$	0 violations / 65,536 pairs (all 3 models)
qRelu_idempotent	$\max(\max(q,z),z) = \max(q,z)$	0 violations / 65,536 pairs
qRelu_meet_preserving	$\max(\min(a,b),z) = \min(\max(a,z), \max(b,z))$	0 violations / 65,536 pairs
qRelu_fixed_iff	$\max(q,z) = q \iff z \leq q$	128/256 fixed points at zp=0
productWitness_exists	$\exists (a,b) : a \not\leq b \wedge b \not\leq a$	Canonical: a=[0,1], b=[1,0]
activationFixedSet_mono	$z_1 \leq z_2 \Rightarrow \text{Fix}(z_2) \subseteq \text{Fix}(z_1)$	INT8 > INT16 > FP16 gap (all models)
graftBoundaryNucleus_not_boolean	$\neg\,\text{isBoolean}(R_z)$	Non-trivial boundary at every layer
componentUpperBound_eq_total	$q + g + r = t$	Phase 3: gap decomposes additively
bitwidthFamily_gap_positive	$\forall k, \exists a, \text{gap}(k,a) > 0$	Phase 4: positive gap at INT8, INT16, FP16
certificate_gap_nonzero	$0 < t$	All models: total gap > 0
observedBoundaryGap_nonneg	$0 \leq \text{observedGap}$	All gap measurements nonneg
latticeSpacing_pos	$0 < \text{scale}$	All quantized layers have scale > 0

>_DEPENDENCY.GRAPH

Module Dependencies

Hover over a module to trace its imports. Solid lines show direct dependencies; dashed lines show transitive imports from the HeytingLean upstream library.

Upstream Foundation Axioms Bridge Certificateimportstransitive

>_VERIFIED.C

Verified C Artifacts

Faithful C11 transpilation. Compiled with gcc -std=c11 -Wall -Wextra -Werror (0 warnings). 7 self-test suites pass.

C

nucleus_grafting.h

Core types and qRelu interface | from Types+DiscreteLattice

DOWNLOAD

C

nucleus_grafting.c

Exhaustive INT8 nucleus verification | from DiscreteLattice+Types

DOWNLOAD

C

main.c

Test harness (7 suites, all pass) | from Tests

DOWNLOAD

>_SAFE.RUST

Safe Rust Artifacts

Zero unsafe, standalone crate. cargo build (0 warnings) + cargo test (11/11 pass).

Rs

Cargo.toml

Crate manifest | from Crate

DOWNLOAD

Rs

src/lib.rs

Module re-exports (4 modules) | from Crate

DOWNLOAD

Rs

src/types.rs

LayerQuantParams, GapDecomposition, activationFixedSet | from Types

DOWNLOAD

Rs

src/discrete_lattice.rs

qRelu axioms, ProductWitness, INT8 characterization | from DiscreteLattice

DOWNLOAD

Rs

src/boundary_connection.rs

DiscreteGateMeasurement, BitwidthFamily | from BoundaryConnection

DOWNLOAD

Rs

src/certificate.rs

NucleusGraftingCertificate with gap assertions | from Certificate

DOWNLOAD

>_PROVENANCE

Provenance Chain

1

Mathematical Theory

Original research connecting Hossenfelder's no-go theorem to quantization theory. INT8 activation lattices are Heyting algebras; ReLU gates are nucleus operators.

2

Lean 4 Formalization

4 modules, 17 theorems, 298 lines. Kernel-verified by Lean 4 + Mathlib. 2 rounds of hostile adversarial audit. Zero sorry/admit. All findings remediated.

3

Empirical Validation

5-phase experiment pipeline across MLP, CNN, and autoencoder architectures. 65,536-pair exhaustive verification. Bitwidth monotonicity. 74–96% gap optimization. α,β-CROWN neural network verification bounds.

4

Verified C + Safe Rust

C11 transpilation (gcc 0 warnings, 7/7 tests). Rust crate (0 unsafe, cargo test 11/11 pass).

Nucleus GraftingVerified Quantization-Aware NN Compression

Overview

Formal Verification Certificate

Key Definitions & Results

Definition: Nucleus Operator

Theorem: ReLU Gate is a Nucleus

Theorem: Gap Decomposition

Theorem: Bitwidth Monotonicity

Corollary: Non-Boolean Boundary

Proof Modules

Lean Theorem ↔ Mathematics ↔ Empirical Evidence

Module Dependencies

Verified C Artifacts

Safe Rust Artifacts

Provenance Chain

All Projects

Hossenfelder No-Go

Research

Nucleus Grafting
Verified Quantization-Aware NN Compression