JIT Speculative-Precision Dequantization (the τ-bowl)

Keep weights at a coarse code (Q4 / E_8 / Leech). Mask a tile up to higher precision only at the instant it is used, only where provably indistinguishable from the true high-precision op, and miss (recompute), never lie everywhere else. You don't need BFL's private undistilled weights — distillation/quantization is coarse-graining, the residual is recoverable, and you regrow the fidelity just-in-time with a proof each regrowth is admissible.

The one certified loop

distillation/quantization = coarse-graining in function space
  → the dropped residual is RECOVERABLE structure, not secret
  → keep the coarse code; SPECULATE the high-precision value per-op
  → ADMIT only under the Tukey-bowl gate (c = γ/2, redescend = miss-not-lie)
  → tighten the bowl with E_8 → Leech (lower second moment G ⇒ smaller residual)
  → draft on the leech-turbo stride 11 (coprime to the Leech field carrier)
  → never ship a wrong answer

The Tukey bisquare is the admission rule: with tuning constant c = γ/2, a residual inside the bowl gets full influence (admit), past c it redescends to zero influence (miss-not-lie). That is exactly the 2·τ ≤ γ premise of Gnosis/QualityMarginCacheAdmissibility.lean.

The two-level gate (the norm is the whole game)

The lattice quantization win (E_8/Leech) is an L2 / energy phenomenon; the classifier decision (argmax) is L∞ / sup-norm. Gating the wrong norm kills the lattice advantage. Measured (kv_cache_e8::bowl_gate_report, d=128 KV):

So E_8 is rejected by the sup-norm gate and wins 10–15× under the energy gate. The resolution is a two-level structure:

• Weight/KV space → gate in L2. A weight residual reaches a logit through an inner product ⟨τ, a⟩ ≤ ‖τ‖₂·‖a‖₂ (Cauchy-Schwarz). The sensitivity bridge is S = ‖a‖₂ (the activation energy) — the τ-bridge, not unknown.
• Logit space → gate in L∞. Argmax preservation = the existing sup-norm cert.

This is proved end-to-end:

• Gnosis/EnergyMarginBridgeAdmissibility.lean — squared Cauchy-Schwarz via the Lagrange identity (no sqrt): 4·‖τ‖²·‖a‖² ≤ γ² ⇒ −γ ≤ 2·⟨τ,a⟩ ≤ γ. propext-only.
• Gnosis/QualityMarginCacheAdmissibility.lean — 2·τ ≤ γ ⇒ argmax preserved.
• Gnosis/JitDequantAdmissibility.lean — the capstone composing both.

The speculator race (no single winner — a certified policy)

jit_speculator_race.rs races four truth-free drafters through the energy gate on ρ=0.9 AR(1)-correlated KV (train/held-out split), swept over cell coarseness:

• Fine cells → the geometric lattice-E_8 prior wins (100% certified accept vs centroid 50%); the residual is high-frequency rounding noise the trained head correctly learns it cannot predict (β ≈ identity on the cell).
• Coarse cells → the distilled head wins shipped error (RMSE 0.025 vs 0.032); its β migrates weight to the neighbours as the cell stops carrying the signal. Generalizes to held-out sequences. (train choo choo.)

effective_rmse (miss = exact recompute = 0 error) exposes "cheaters": a drafter with tiny effective error but ~0 accept just recomputed everything.

The serve-time keystone: truth-free admission

At inference there is no truth to measure τ. Two honest results (bench_truth_free_tau_estimators):

1. Per-tile estimators FAIL. Window-jackknife (corr −0.27) and committee disagreement (corr −0.22) both anti-correlate with the residual: disagreement marks where the model works, and the residual is irreducible noise — unpredictable per-tile by construction.
2. Conformal calibration SUCCEEDS. The residual quantile measured once on a calibration set transfers to fresh data within 0.2%: q=.95 → 5.23% measured lie-rate (target 5%). Admit a (speculator, step, layer) config iff 2·Q_q ≤ γ ⇒ certified serve-time lie-rate ≤ 1−q, no truth at inference.

Runtime: conformal_gate.rs (ResidualCalibration, conformal_admit); finite distribution-free core: Gnosis/ConformalCoverageAdmissibility.lean.

Distribution-free, proven (not assumed). On heavy-tailed (lognormal σ=0.8) residuals — the regime real quantized weights live in — conformal coverage holds (q=.99 → 0.99% lie vs 1% target) while a parametric Gaussian gate (μ+zσ) silently under-covers 3.4× (3.36% lie at q=.99). The Gaussian tail is too thin; conformal assumes nothing. This is the "distilled model looks fine but quietly lost fidelity" failure — and the conformal gate is provably immune.

The deployment headline. Per-layer conformal admission on a heterogeneous transformer (q=.99, γ=1.6): 66.7% of compute runs at coarse-code cost with a certified ≤1% quality-loss bound, and the outlier-heavy layers (ffn.down, embed — the LLM.int8 "outlier features" that wreck naive quantization) are correctly refused (miss-not-lie). The savings are honest because the refusals are certified, not guessed.

Carrying the bowl to FLUX: the basin/separatrix gate

For images there is no argmax — the decision is which basin of attraction (image mode). basin_gate.rs accumulates per-step masked-velocity residuals; the trajectory stays in the same mode iff the net accumulated displacement stays inside the distance to the separatrix.

• Cert: Gnosis/BasinSeparatrixAdmissibility.lean — Σ|δ_t| < R ⇒ net displacement < R ⇒ no separatrix crossing. propext-only.
• Demo (synthetic double-well, near-separatrix): ungated masking flips 44/400 (11%) trajectories into the wrong mode; the basin gate flips 0 at 99.9% accept — only recomputes the dangerous boundary steps.
• Plugs into the carrier's existing stride-11/E_8 …-r11 spectral-residual path (model_flux_txt2img). NOT run against the real flux-1-dev knot: dev-only / no-knot-run / no-cloud-build / no-deploy admission (see packages/inference-runtime/docs/unsound-flux-admission.md).

File map

The certified spine is 14 Lean modules, all Init-only (Rustic Church), every one [propext]-only or fully axiom-free (LeechTurboStrideCert, LatticeGLadder, LeechShellDecomposition carry no axioms at all), each independently verified (lake build + #print axioms + banned-token audit). The conformal permutation-averaging→probability step is now closed (it was finite counting, not measure — ConformalCoverageProbability.conformal_lie_rate_certified); the only remaining honest side-condition is TukeyBisquareGate's 0 ≤ c (the tuning constant is a genuine radius).

Validated on real admitted-model weights

src/bin/bowl-probe.rs runs the gate on the real Q8_0 token_embd_weight (151936×896) of the admitted qwen2.5-0.5b-instruct.knot — dequantized via the crate's verbatim Q8_0 block layout, behind an honesty sanity-gate that aborts rather than report numbers if the extraction looks wrong (proven: it aborted on K-quant-only tensors instead of faking). Findings transfer from synthetic to real:

• the real embedding is cell-filling (eff_dim 351/896, mean|corr| 0.029);
• E8Tail is +14.0% lower MSE than cubic — matching the theoretical edge exactly, on learned weights;
• the energy gate admits E8 100% vs cubic 50.4% (~2× more real tiles);
• conformal coverage roughly holds (q=.99 → 1.88% lie vs 1% target).

Honest caveat: conformal is slightly loose on the real embedding (1.88% vs synthetic's 1.23%) because embedding rows aren't perfectly exchangeable (rare-token rows carry heavier, clustered residuals) — on real weights, calibrate a touch more conservatively.

Real FFN weights too (3 quant formats). src/bin/bowl-probe-ffn.rs extends to the K-quant FFN layers via kquant_dequant.rs (Q8_0/Q5_0/Q6_K row-dequant, each verified against the crate's tested mat_vec_dispatch_batch — a wrong decode cannot pass). qwen2.5-0.5b layer 0:

Correction to the "outlier-feature" intuition: the FFN weights are cleaner than the embedding (conformal holds tighter, 0.74–0.82% ≤ 1%). LLM.int8 outliers live in activations, not weight matrices — so weight-tile gating behaves best on FFN; the embedding's rare-token rows were the real heterogeneity. The findings hold across all three quant formats on real admitted-model weights.

bowl-probe now exposes dev-model quality profiles:

Use sovereign targets:

pnpm run a0 -- run distributed-inference:build-bowl-probe
pnpm run a0 -- run distributed-inference:write-bowl-probe-admission-suite

For incremental work, use the individual profile/frontier targets:

pnpm run a0 -- run distributed-inference:bowl-probe-dev-fast
pnpm run a0 -- run distributed-inference:bowl-probe-dev-balanced
pnpm run a0 -- run distributed-inference:bowl-probe-dev-strict
pnpm run a0 -- run distributed-inference:write-bowl-probe-dev-fast-admission
pnpm run a0 -- run distributed-inference:write-bowl-probe-dev-balanced-admission
pnpm run a0 -- run distributed-inference:write-bowl-probe-dev-strict-admission
pnpm run a0 -- run distributed-inference:validate-bowl-probe-dev-admissions
pnpm run a0 -- run distributed-inference:write-bowl-probe-gamma-frontier-admission
pnpm run a0 -- run distributed-inference:validate-bowl-probe-gamma-frontier-admission
pnpm run a0 -- run distributed-inference:write-bowl-probe-aggregate-admission
pnpm run a0 -- run distributed-inference:validate-bowl-probe-aggregate-admission

The binary also accepts --matrix-type any|float|q8_0, --q-values, explicit --step, --gamma-multiplier, --format json, and --output <path>. The write targets persist JSON reports at:

• .a0/runs/jit-dequant/real/qwen2.5-0.5b-instruct.dev-fast.bowl-probe.admission.json
• .a0/runs/jit-dequant/real/qwen2.5-0.5b-instruct.dev-balanced.bowl-probe.admission.json
• .a0/runs/jit-dequant/real/qwen2.5-0.5b-instruct.dev-strict.bowl-probe.admission.json
• .a0/runs/jit-dequant/real/qwen2.5-0.5b-instruct.gamma-frontier.bowl-probe.admission.json
• .a0/runs/jit-dequant/real/qwen2.5-0.5b-instruct.aggregate.bowl-probe.admission.json

Each report includes an admission object for the runtime predicate finite && cell_filling && e8_mse_le_cubic && e8_energy_accept_ge_cubic && all_conformal_admit, plus the proof spine modules: Gnosis.QualityMarginCacheAdmissibility, Gnosis.EnergyMarginBridgeAdmissibility, Gnosis.BasinSeparatrixAdmissibility, Gnosis.JitDequantAdmissibility, and Gnosis.ConformalCoverageAdmissibility.

Current persisted qwen2.5-0.5b results:

The aggregate certificate intentionally does not turn the strict rejection into a failure. It treats dev-balanced as the local default gate and the strict gamma sweep as boundary evidence. Current frontier data selects a first admitted grid multiplier of 1.90 × and an exact conformal minimum of 1.8989613043934688 ×; the runtime-facing sidecar records this under runtimeMarginSelector with a comfortable default multiplier of 2.0 ×, a compact boundary window, and sourceSetSha256 over the constituent profile and frontier artifact hashes.

The strict rejection is useful: the lattice edge remains, but the conformal admission margin exposes the first quality boundary instead of rubber-stamping every profile.

The gamma frontier artifact tightens that boundary. On the strict 16k-row embedding probe with q=.95,.99, the exact conformal lower-bound multiplier is 1.8989613043934688 × cubic_l2_residual_scale; the grid sweep rejects through 1.85 × and first admits at 1.90 ×. Near the boundary, E8 acceptance jumps from 39.1% at 1.85 × to 99.2% at 1.90 ×, while cubic is still effectively closed (0.04%). This is the runtime dial: 1.90 × is the first certified frontier for this carrier/profile, and 2.00 × is the comfortable default.

Honesty rails

• Ground truth = the model's own high-NFE / true-precision limit, never "pro-like" (Sardis). The lattice win is L2, measured end-to-end, not assumed.
• Per-tile truth-free τ is provably hard (residual = irreducible noise); the deployable gate is conformal (per-config), not per-tile.
• FLUX is demonstrated on a synthetic field; the real-knot run is gated off.