Modern optimizers (Adam, Muon, Shampoo, SOAP) differ mainly in how much curvature structure they estimate: a diagonal, a spectral norm, a Kronecker factor, a full matrix. Estimating more structure buys a better preconditioner but pays for it in estimation noise, and the field picks a rung by folklore. This project asks when the trade actually pays, and answers it as decision theory over the lattice of matrix subalgebras: an exact variance penalty for each rung, a proof that the cost of estimating an eigenbasis is O(1) rather than blowing up as the eigengap closes, and an adaptivity phase transition at the BBP threshold of random matrix theory. In a rank-one spiked-Wigner idealization of the curvature estimate, and under an explicit spike-to-bulk condition near 0.69, isotropic Muon-style preconditioning is exactly asymptotically minimax optimal below that threshold, so within that model no estimator does better in the worst case over spike directions. Just above the threshold the picture reverses: an oracle-shrunk estimator beats the trivial rung at every signal level tested, so the unprofitable window belongs to the plug-in estimator rather than to the problem. The theory then becomes a method: the Geometry Ladder is an anytime optimizer that walks the lattice from trivial to diagonal to Kronecker to full, promoting only when a concentration bound certifies the richer rung has earned its noise, with hysteresis to prevent thrashing. Putting that method through its own pre-registered protocol is where the interesting result is: on convex problems, on MLPs, and on CIFAR-10 with ResNet-18, the certified rule almost never promotes the wide layers where richer structure was supposed to pay. Built on sketchy, a PyTorch library with Nystrom sketching, Hessian-vector-product and Gauss-Newton oracles, and Muon, all on a single RTX 3060.

• ●Result: Threshold theory, proved and numerically verified: exact variance penalties for each preconditioner structure, an eigenbasis-estimation cost that stays O(1) as the eigengap closes rather than exploding, and an adaptivity phase transition at the BBP threshold. In a rank-one spiked-Wigner model of the curvature estimate, and under an explicit spike-to-bulk condition near 0.69, isotropic Muon-style preconditioning is exactly asymptotically minimax optimal below the threshold. A companion non-asymptotic bound needs no imported random-matrix result and stays positive at every finite dimension for signal-to-noise up to 0.98, at a constant of 1/4 rather than 1.
• ●Result: Measured that low-rank curvature corrections are redundant with Muon's orthogonalization: on CIFAR ResNet layers the correction redirects the Muon step by a median of 0.84 in relative Frobenius norm, range 0.65 to 1.06, with no accuracy improvement, and the redundancy is structural. Concurrent Muon work from 2025 and 2026 reached the same conclusion independently.
• ●Result: The Geometry Ladder promotes between structures only when a concentration bound certifies the richer rung has earned its estimation noise, with hysteresis against thrashing, and it carries a proved oracle inequality and a no-thrashing guarantee.
• ●Result: Put that rule through a pre-registered test on real networks and recorded the negative. On CIFAR-10 with ResNet-18, two seeds, 30 epochs, the ladder left all 13 preconditioned wide convolutions on the trivial rung in both seeds and promoted only on narrow downsample layers, so the pre-registered hypothesis that the Kronecker rung would be a destination rather than a transient is refuted. Ladder, fixed trivial and fixed Kronecker arms all land within about a tenth of a point of each other. The one gap that clears the noise runs the other way: a fixed diagonal metric averaged 88.4% test accuracy against 89.6% for no preconditioning at all, keeping its sign on both seeds and on the tuning run. At two seeds that is suggestive rather than settled, and the wide-layer non-promotion is confounded by a curvature reservoir shared with the forced-Kronecker arm, so what the experiment shows is that the certified selector rarely selects structure, not that structure would not pay.
• ●Result: Machine-checked the paper's algebraic backbone in Lean 4 and Mathlib: ten sorry-free theorems covering the Cauchy-Schwarz positivity behind the adaptivity threshold, the point-mass floor used by the finite-dimension lower bound, the trace collapse behind the full-matrix variance penalty, the Kronecker multiplicity discount, and the closed-form zero-noise sign law. The scope boundary is explicit and narrower than it looks: the GOE and Wick moment constants those variance results collapse to enter as hypotheses rather than as Lean-proved facts, and the probabilistic and asymptotic core, meaning the chi-squared and total-variation computations, the BBP threshold, the minimax argument and every large-dimension limit, is outside Lean scope.

Write-up · 27-page draft paper with proofs appendix; closed-form constants numerically verified, core algebraic identities machine-checked in Lean 4 and Mathlib.

Evaluation is supposed to be a fixed-n experiment: fix the sample size in advance, run it, read the number. In practice nobody does that. You watch the number, and when it looks good enough you stop, which quietly voids the guarantee you thought the number carried. This project builds an evaluation that survives being watched. certify is an anytime-valid ε-equivalence test (a betting confidence sequence with a GROW-boundary e-process) that answers whether a compressed model stays within ε of its source, with a wrong-verdict probability that holds below α no matter when you stop, so an evaluator can peek after every batch, stop the moment the verdict lands, and lose nothing. Matching sample-complexity bounds say what that costs. Two specializations make it usable in deployment: a worst-slice test whose ability to detect a broken subgroup does not degrade with the number of slices, so detection pays no Bonferroni penalty, and a frontier mode that certifies which of K candidate compressions are ε-equivalent and returns the cheapest, paying the expensive source-model cost once rather than K times. An audit applies it to eight architecture families under bitsandbytes and released GPTQ/AWQ checkpoints. The statistical pieces specialize known results, and the paper says so plainly; the contribution is assembling them into a certifier a practitioner can actually deploy.

• ●Result: Anytime-valid by construction: the wrong-verdict probability stays below α however long the evaluation runs, so watching the number and stopping when the verdict lands costs nothing, where a fixed-n test would be invalidated by the same peek
• ●Result: Two deployable specializations. The worst-slice test tracks a product e-process over predictable slices, so its error stays at alpha for any number of slices G and its detection bound is independent of G at a fixed worst-slice frequency, where a fixed-n test pays a Bonferroni log G. In a synthetic sweep from G = 2 to G = 128 the two cross near G = 16, so the e-process is the cheaper instrument only above that; certifying that every slice is equivalent, rather than detecting that one is broken, still pays a union bound and the paper proves that cost unavoidable. The frontier mode returns the cheapest epsilon-equivalent config from a menu of K compressions and shares each expensive source pass across candidates, measured at a 2.18x saving on a three-config menu of released Qwen2.5-1.5B quantizations.
• ●Result: Audit of 29 model-and-method pairs across eight architecture families, 0.36B to 3.8B, at epsilon = 5% top-1 disagreement with alpha = 0.05. Every 4-bit pair certifies NOT_EQUIVALENT, 17 of 17, covering all eight families and both bitsandbytes NF4 and released GPTQ and AWQ checkpoints. 8-bit is neither uniformly lossless nor cleanly architectural: of 12 pairs, 4 certify equivalent, 3 certify not equivalent, and 5 stay undecided at the 4,000-token budget, with Qwen2.5-3B int8 certified not equivalent while its 0.5B and 1.5B siblings remain undecided.
• ●Result: Matching sample-complexity upper and lower bounds for the Bernoulli discrepancy model, sharing the leading constant as alpha goes to zero, with the oracle second-order term proved to be a bounded constant rather than a growing one. Its value is the renewal boundary overshoot, measured in simulation at 0.26 nats and flat across log(1/alpha) from 3 to 20; the plug-in adaptivity constant, worth 1.3 to 1.9 nats, is open.

Write-up · Draft paper, 16 pages with proofs appendix.

Learned 3D bin packers handle constraints (no stacking on glass, orientation locks, unload order) by masking illegal placements at each step. The mask is the field's standard interface, and it is sound as far as it goes: every placement it permits is legal. This study asks what it cannot promise, and the answer is completability. A greedily legal placement can still strand the items that come after it, and no per-step mask can see that coming. Three theorems locate the boundary exactly. When the packer has recourse (it can always open another bin), dead-ends cannot exist and masking is genuinely sufficient, which is why the entire prior benchmark regime, including my own, never noticed the gap. At fixed capacity that escape hatch is gone, dead-ends appear (shown by a machine-verified minimal counterexample), and the interface that would restore sufficiency requires deciding viability, which is strongly NP-hard. The empirical half builds the fixed-capacity benchmark the theory demands, on instances that are provably packable, and shows the failure is severe, diagnosable, and partly fixable: a learned viability critic recovers much of what the policy's own value head throws away. The packing engine this work grew out of ships in Packomation.

• ●Result: Constraint-agnostic packing: randomizing declarative feasibility masks during training yields one policy that transfers across constraint sets, and a lookahead head that chooses which of the next k buffered items to place raises the strict win rate over the best-of-four heuristic from 0.10 to 0.69 as constraints tighten, while staying 90-95% proven-optimal against a CP-SAT lower bound
• ●Result: Isolated where the advantage comes from: matched-budget ablations rule out extra search as the explanation, and an online-PPO baseline at the same budget never clears the bar, so the gain is lookahead selection rather than reinforcement learning in general
• ●Result: Three theorems locate the boundary of what a feasibility mask can promise: with recourse, dead-ends cannot exist and masking is sufficient; at fixed capacity they can, shown by a machine-verified minimal counterexample; and the interface that would restore sufficiency requires deciding viability, which is strongly NP-hard
• ●Result: Showed the gap is real rather than theoretical: on provably packable instances a masked packer's success collapses from 100% to near zero as the container tightens, placing 92% of items while finishing 5% of instances, and a CP-SAT cross-check confirms the instances themselves are easy
• ●Result: A learned viability critic beats the policy's own value head as search guidance by +0.218 [+0.188, +0.250] at the 9-item training size, survives zero-shot transfer to 12 to 25 item instances at +0.115 pooled, and replicates zero-shot on a structurally different tight non-guillotine distribution at around +0.20. Pushed further the edge decays with scale: +0.077 at 30 items, +0.055 at 35, and +0.008 by 40, inside seed noise. Measured on instance-disjoint held-out data the critic predicts completability at AUC 0.975 with a spread of 0.002 across four seeds, over 17,646 states from 150 instances.
• ●Result: Re-measured that critic's headline AUC under an honest protocol and the number moved. The in-split figure came from a state-level random permutation over a pool where sibling rollout states of one instance appear across three rollouts, scored on the same fold used to pick the training epoch, on class-balanced data. On 17,646 states from 150 fresh instances with the natural prior, the same four critics score 0.9752 plus or minus 0.0018 against 0.9903 plus or minus 0.0012 on their own validation folds. Calibration moves the same way, ECE 0.033 honest against 0.021 in-split. The gap is composite, mixing split leakage, checkpoint selection and the class prior, and no run separates them; instance-disjoint evaluation is simply the protocol this quantity requires.
• ●Result: Tested what the viability estimate is worth at rollout with no search. Taking its argmax over the policy's top-8 shortlist raises success by +0.104 [+0.078, +0.130] against a matched control that expands the same shortlist, drops the one-step dead ends, then picks by the policy's own logits, over 960 fixed-capacity instances; widening to a top-16 shortlist gives +0.108 [+0.067, +0.150]. The arms that implement the interface the theory actually prescribes, where the estimate restricts and the policy still decides, score only +0.026 to +0.043, inside the per-cell critic-seed spread, and a single hand-built feasibility feature matches them. The payoff is in ranking by completability, not in filtering by it. Both runs use one critic seed where the other headline numbers here average four, and the pooled effect is uneven across the grid, about +0.24 in the loose cells and at or below +0.08 in the tight ones.

Write-up · Paper drafted.

A theory-plus-audit research project (speccomp) on what makes a neural network layer compressible, and whether the field's training-free sensitivity heuristics actually measure it. The central audit finding is that popular training-free scores (Hessian trace as in HAWQ, heavy-tailed exponent α) predict weight-space compressibility but not output-space damage; used for mixed-precision bit allocation, they perform worse than random. A cheap one-backward empirical-Fisher gradient predictor does better. It ranks ahead of HAWQ's double-backward Hessian score on all 11 cells of a 4-model sweep spanning round-to-nearest quantization, pruning and low-rank compression, and ties it under GPTQ (WikiText-2 perplexity 60.5 against 60.1, one run per arm) for one backward pass instead of an 8-probe Hutchinson trace. A Gauss–Newton analysis explains the gap, and its falsifiable probe-noise-vs-data-alignment prediction held up in testing. The headline claim survived a pre-registered confirmatory test on a 7-model, 5-architecture panel, with thresholds proposed before the confirmatory sweep and never changed after seeing data. The pre-registered primary hypothesis did not survive, which is the more useful half of the result. All numbers reproduce from the experiments directory; everything runs on a single 12 GB GPU.

• ●Result: Established that the field's training-free sensitivity scores (Hessian trace, heavy-tailed α) predict weight-space compressibility but not output-space damage: used to allocate bits, they do worse than random
• ●Result: A one-backward empirical-Fisher predictor matches HAWQ's double-backward Hessian score under GPTQ on WikiText-2 (perplexity 60.5 against 60.1, one run per arm, no variance estimate) for one backward pass instead of an 8-probe Hutchinson trace, and ranks ahead of it on all 11 cells of a 4-model sweep spanning round-to-nearest quantization, pruning and low-rank compression. The blunt finding underneath: uniform allocation still beats both on every quantization cell, so the field's contest between sensitivity scores is being run below a bar that a trivial baseline already clears.
• ●Result: Pre-registered confirmatory test on a 7-model, 5-architecture panel, 168 shape-controlled cells with correlations computed within each architecture and pooled: the one-backward weight-error times gradient-RMS predictor beat the HAWQ Hessian by delta rho = +0.243 [+0.201, +0.285], winning on four of the five architectures and tying on the fifth (Bloom, 0.514 against 0.518). The pre-registered primary hypothesis failed, and that is the result worth reporting: the forward-only activation-RMS signal that beat HAWQ on a single model was inferior across the panel (delta rho = -0.179), and forward-only activation statistics are the cheap default the field reaches for.
• ●Result: A Gauss-Newton analysis explains the gap, and its sharpest prediction held on OPT-350M across 3 seeds on the quantization cells: as the Hutchinson probe count rises from 1 to 64 the Hessian score's correlation with output error climbs from 0.21 to 0.50 and is still short of the one-backward gradient's 0.57, so part of the advantage is probe noise that more probes remove and part is the residual gap the data-alignment term predicts. A second prediction, on per-method isotropy, held only partly: the fit was worst for low-rank as expected, but the stable-rank proxy was too crude to order the methods.

Write-up · Draft workshop paper.

Frequency-domain PEFT methods (FourierFT, WaveFT, and wavelet LoRA variants) report gains and credit the transform basis: a Fourier or wavelet basis is said to encode structure that a plain low-rank update misses. That attribution had never been tested against a matched control. This project builds one. A basis permutation is orthogonal and energy-preserving, so permuting the basis ordering holds parameter count, sparsity support, and effective rank fixed while destroying the structure the transform is supposed to exploit; whatever the real basis buys over its permuted null is structure, and whatever it does not is decoration. Running the control on FourierFT and WaveFT with RoBERTa-base on GLUE splits the reported gains into three parts, and the basis is the smallest of them. Magnitude does most of the work, and the collapse everyone reads as proof that the transform is necessary belongs to one method. FourierFT's no-transform variant craters to the frozen baseline (CoLA MCC 0.000) because its scaling constant is calibrated to a normalized inverse FFT, so dropping the transform without rescaling mis-sizes the update by a factor near 768; magnitude-matching alone recovers 70-87% of that collapse. WaveFT needs no such correction, since its inverse DWT is orthonormal, and its no-transform variant does not collapse on any of the three tasks (CoLA MCC 0.554 against 0.557 for the true basis). The field's headline evidence for transform necessity is a normalization artifact. Density, the high-rank sparse parameterization, is the real but small remainder, worth 0.026 accuracy on MRPC and 0.072 MCC on CoLA. What is left for the basis itself is close to nothing: a permuted Fourier basis is statistically indistinguishable from the true one on MRPC and CoLA (paired p = 0.91 and 0.67), and permuting the wavelet basis is harmless on all three. There is one exception and it is reported as one: FourierFT on RTE, where the true basis wins in 3 of 3 seeds by a mean 0.041 accuracy margin, paired p = 0.03. Two things keep it modest. The wavelet grid on RTE runs the other way, and a magnitude-matched independent orthogonal basis lands inside the permuted band. At three seeds this is the one place the basis may carry real structure, not a demonstration that it does. A budget sweep over 50, 200 and 1,000 Fourier coefficients per adapted projection, 1,200 to 24,000 adapter parameters, finds no crossover where structure starts to matter, including at the tightest budget where a structural prior has the most room to help. The project began as WaRA, a PyTorch library for wavelet-domain LoRA, which remains the instrument.

• ●Result: Decomposed FourierFT's apparent need for its transform on RoBERTa-base across MRPC, CoLA and RTE, 3 seeds each. Magnitude does most of the work: a no-transform update that differs only by a per-layer rescale to the transform's Frobenius norm recovers 82%, 87% and 70% of the collapse. The remainder is density, the dense reach a transform buys across every weight coordinate, worth 0.026 on MRPC (mean of accuracy and F1) and 0.072 MCC on CoLA. Running the same controls on WaveFT sharpened the result: its inverse DWT is orthonormal, so its no-transform update is already magnitude-matched, never collapses, and leaves no density gap.
• ●Result: What remains for the basis is close to nothing on two tasks of three: a permuted Fourier basis is indistinguishable from the true one on MRPC and CoLA (paired p = 0.91 and 0.67), and permuting the wavelet basis is harmless on all three. The single exception is FourierFT on RTE, where the true basis wins in 3 of 3 seeds by a mean 0.041 margin (p = 0.03), tempered by the wavelet grid running the other way there and by a magnitude-matched independent orthogonal basis landing inside the permuted band. No capacity threshold appears across the 50, 200 and 1,000 coefficient budgets, including the tightest, where a structural prior has the most room to help.
• ●Result: The control is exact by construction: permutations are orthogonal and energy-preserving, so they hold parameter count, sparsity support, and effective rank fixed while destroying the structure the transform is meant to exploit
• ●Result: A companion analysis on one fully fine-tuned SAM ViT-B update supports the account: the update's weight matrices sit inside their row-and-column permutation null across all 48 layers tested (mean z = +0.14), while the same model's patch-token activation grids beat their spatial-permutation null on wavelet low-frequency energy in all 60 image-by-block grids (mean z = +19.1). One model and one update, so it illustrates why a structured basis can be inert in weight space while being well motivated on activations, rather than establishing it.
• ●Result: WaRA, the wavelet-domain PEFT library the study is built on, ships weight-space and activation-space variants against a parameter-matched LoRA baseline

Write-up · Paper drafted, 12 pages.