David Gary

Modern optimizers (Adam, Muon, Shampoo, SOAP) differ mostly in how much curvature structure they estimate: a diagonal, a spectral norm, a Kronecker factor, or a full matrix. More structure gives a better preconditioner but adds estimation noise, and which rung to use is decided by convention. This project treats the choice as a decision problem over the lattice of matrix subalgebras. It gives an exact variance penalty for each rung, proves that the cost of estimating an eigenbasis stays O(1) as the eigengap closes, and finds an adaptivity phase transition at the BBP threshold from random matrix theory. In a rank-one spiked-Wigner model of the curvature estimate, an oracle-shrunk estimator is profitable everywhere above the threshold, and that side is proved. Below it, isotropic Muon-style preconditioning is asymptotically minimax optimal, so within that model no estimator does better in the worst case over spike directions. That half is proved modulo an imported limit, and only for a spike-to-bulk ratio β/ρ up to about 0.69. A plug-in estimator only becomes profitable once the spike passes the threshold by a factor s** in (1, sqrt 3), which is 1.298 in the paper's parametrization. So the unprofitable window is specific to the plug-in estimator. The theory then turned into a method, the Geometry Ladder. It is an anytime optimizer that moves from trivial to diagonal to Kronecker to full, and it only promotes when a concentration bound certifies that the richer rung has earned its noise (with hysteresis so it doesn't thrash). On small MLPs the certified rule promoted three of four layers to the full rung in all five seeds (the fourth, an isotropic input layer, rightly stayed trivial), though no arm trained measurably faster. The most interesting result came from running it through its own pre-registered protocol on CIFAR-10 with ResNet-18, where it almost never promoted the wide convolutions that richer structure was supposed to help. Built on sketchy, a PyTorch library with Nystrom sketching, Hessian-vector-product and Gauss-Newton oracles, and Muon, all on a single RTX 3060.

• The threshold theory is proved and checked numerically, with one caveat below the threshold. It covers exact variance penalties for each preconditioner structure, an eigenbasis-estimation cost that stays O(1) as the eigengap closes, and the adaptivity phase transition at the BBP threshold. Above the threshold, an exact asymptotic gain formula (with an O(1/d) remainder) shows that shrinkage is profitable everywhere, and the plug-in edge appears exactly past s** = 1.298. The finite-dimension crossings for d = 8, 16 and 32 are 1.36, 1.34 and 1.33, decreasing toward it. Below the threshold, in a rank-one spiked-Wigner model of the curvature estimate, isotropic Muon-style preconditioning is asymptotically minimax optimal. That proof rests on an imported limit (E δ_d² → 0) and only covers a spike-to-bulk ratio β/ρ up to about 0.69. All ten pre-registered gates for the theorem check out numerically, and the oracle identity holds to machine precision. 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, though with a constant of 1/4 instead of 1.
• A low-rank curvature correction doesn't improve Muon on a CIFAR-10 ResNet, across two different mechanisms (all variants within about a point at a single seed, and slower). It isn't inert, though. On the same layers it redirects the Muon step by a median of 0.84 in relative Frobenius distance (range 0.65 to 1.06, where two unrelated directions would sit near 1.41). The same correction does help SGD on a convex problem. The paper scopes the negative to low-rank corrections in this vision setting, since concurrent work reports that Kronecker and full corrections beat Muon on transformers. Whether curvature structure is what separates the two cases is a hypothesis it motivates but doesn't test.
• I put the Geometry Ladder's promotion rule through a pre-registered test on CIFAR-10 with ResNet-18, and the result was negative. Over two seeds and 30 epochs, the ladder left all 13 preconditioned wide convolutions on the trivial rung in both seeds and only promoted on narrow downsample layers. That refutes the pre-registered hypothesis that the Kronecker rung would be where those layers settle. The ladder, fixed trivial and fixed Kronecker arms all landed within about a tenth of a point of each other. The one gap bigger than the noise went the other way: a fixed diagonal metric averaged 88.4% test accuracy against 89.6% with no preconditioning at all, and kept that sign on both seeds and on the tuning run. With two seeds that is suggestive but not settled. The wide-layer result is also confounded by a curvature reservoir shared with the forced-Kronecker arm. So the experiment shows that the certified selector rarely picks structure. It doesn't show that structure wouldn't pay.
• The paper's algebraic backbone is machine-checked 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 Lean coverage is narrower than that list might suggest. The GOE and Wick moment constants that the variance results reduce to enter as hypotheses, and Lean doesn't prove them. The probabilistic and asymptotic core (the chi-squared and total-variation computations, the BBP threshold, the minimax argument, and every large-dimension limit) isn't formalized in Lean.

Compositions of odd polynomials of degree d show up in Newton-Schulz-type iterations for the matrix sign function and the polar decomposition, in homomorphic comparison circuits, and in the orthogonalization step of the Muon optimizer (which uses d = 5). Once inside a basin the composition converges doubly exponentially. But the constants in that law, and the burn-in cost of reaching the basin from a small spectral gap, had only been known asymptotically or numerically. This manuscript pins those constants down. It gives an exact one-step law with rational two-sided bounds, a closed form for the second-order coefficient, and a depth-tax law that converts composition depth into effective polynomial degree. For d = 3 and 5 it also proves an exact log-periodic law for the Böttcher constant of the doubly exponential law as a function of the gap. Its modulation is exponentially small (too small to see at ordinary precision). Every numerical constant is certified by interval arithmetic, and the integer identities are kernel-checked in Lean 4 without Mathlib. An independent Julia implementation reproduces C_d for d ≤ 9, the burn-in gains g_3 and g_5, and Λ(½,3). A companion manuscript carries the same iterations into finite precision, with certified noise floors and precision ladders for bf16, fp16 and TF32.

• What the manuscript leaves open: the non-constancy of the periodic factor is shown numerically but not proved, and finite-depth two-sided effective-degree bounds are still open.
• The 16-page companion manuscript gives certified finite-precision envelopes for the same iterations. It includes noise floors, an exact recovery theorem with catch-up constant a_∞(d) = d binom(d−1, (d−1)/2) / 2^(d−1), precision ladders that need at most two steps per IEEE level, and GPU tensor-core experiments in bf16, fp16 and TF32.

Evaluation is supposed to be a fixed-n experiment: pick the sample size in advance, run it, and read the number. In practice nobody does that. You watch the number and stop when it looks good enough, which quietly voids the guarantee the number was supposed to carry. This project builds an evaluation that still holds up when you watch it. 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. The chance of a wrong verdict stays below α no matter when you stop, so you can check after every batch and stop as soon as the verdict comes in without losing anything. Matching sample-complexity bounds say what that costs. Two variants make it practical to deploy. A worst-slice test finds a broken subgroup without getting weaker as the number of slices grows, so detection pays no Bonferroni penalty. A frontier mode certifies which of K candidate compressions are ε-equivalent and returns the cheapest one, paying the expensive source-model cost once instead of K times. The audit runs it on eight architecture families under bitsandbytes and released GPTQ/AWQ checkpoints. The statistical pieces are specializations of known results, and the paper says that. The contribution is putting them together into a certifier that a practitioner can deploy.

• There are two variants built for deployment. 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 doesn't depend on G at a fixed worst-slice frequency. A fixed-n test pays a Bonferroni log G instead. In a synthetic sweep from G = 2 to G = 128 the two cross near G = 16, so the e-process is only the cheaper option above that. Certifying that every slice is equivalent (as opposed to detecting that one is broken) still pays a union bound, and the paper proves that cost can't be avoided. The frontier mode returns the cheapest epsilon-equivalent config from a menu of K compressions and shares each expensive source pass across candidates. On a three-config menu of released Qwen2.5-1.5B quantizations that saved 2.18x.
• The audit covers 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 certified NOT_EQUIVALENT (17 of 17), across all eight families and both bitsandbytes NF4 and released GPTQ and AWQ checkpoints. 8-bit was mixed and varied by model family and size, with some families certifying equivalent and others exceeding the 5% bar. Of 12 pairs, 4 certified equivalent, 3 certified not equivalent, and 5 were still undecided at the 4,000-token budget. Qwen2.5-3B int8 certified not equivalent while its 0.5B and 1.5B siblings stayed undecided.
• Matching upper and lower sample-complexity bounds for the Bernoulli discrepancy model share the leading constant as alpha goes to zero, and the oracle second-order term is proved to be a bounded constant. Its value is the renewal boundary overshoot, which measures 0.26 nats in simulation and stays flat across log(1/alpha) from 3 to 20. The plug-in adaptivity constant, worth 1.3 to 1.9 nats, is still open.

The Tracy-Widom distributions are calibration constants for a lot of modern statistics. Johnstone showed that the largest sample eigenvalue of high-dimensional Gaussian data is asymptotically Tracy-Widom under the null, and largest-eigenvalue tests calibrated by Tracy-Widom quantiles are now standard in principal component analysis and factor-number selection. The standard way to evaluate them, due to Bornemann, computes the defining Fredholm determinants by Nyström discretization. Its convergence theory is proven but non-effective (there are no computable constants), and the published digits are validated empirically by comparing methods. This manuscript makes the digits rigorous. It first shows that naively making the theory effective is hopeless, since the constant exceeds 10^169. Then it builds certified algorithms for F₂ and its density, and for the harder indefinite F₁ and F₄ cases. Every rounding is propagated through Arb ball arithmetic, so each printed interval follows mathematically from the cited theorems and the library's correctness. The paper ends with certified tables at fifteen levels for all three β, including the first certified quantiles.

• Certified here means the printed interval follows mathematically from the results proven in the paper, the cited theorems, and the correctness of the underlying ball-arithmetic library (Arb), with all rounding propagated rigorously.
• Nine property tests pass (trace identities, Weierstrass bracket, monotonicity, density against finite differences, outward rounding, and quantile invariants). An independent audit of the tables confirms monotonicity and the E₊E₋ cross-check at all 261 common grid points. The full table run takes 3.0 hours on 11 cores.
• Open problems the paper names: certified Tracy-Widom moments, general β through the Trogdon-Zhang ODE route, and other edge functionals such as Airy and Bessel gap probabilities.

Learned 3D bin packers handle constraints (no stacking on glass, orientation locks, unload order) by masking illegal placements at each step. That mask is the standard interface, and it works as far as it goes: every placement it allows is legal. What it can't promise is completability. A placement that is legal right now can still strand the items that come after it, and a per-step mask has no way to see that coming. Three theorems pin down where the boundary is. When the packer has recourse (it can always open another bin), dead ends can't happen and masking is enough. That's why the existing benchmarks, my own included, never ran into the problem. At fixed capacity that escape hatch is gone and dead ends do appear (shown with a machine-verified minimal counterexample), and the interface that would fix it requires deciding viability, which is strongly NP-hard. The empirical half builds the fixed-capacity benchmark the theory calls for, on instances that are provably packable. There the failure is severe, but it can be diagnosed and partly fixed: a learned viability critic recovers much of what the policy's own value head misses. This work grew out of Packomation.

• Randomizing declarative feasibility masks during training gives one constraint-agnostic policy that transfers across constraint sets. A lookahead head that picks 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.
• Matched-budget ablations rule out extra search as the reason for the advantage, and an online-PPO baseline at the same budget never clears the bar. So the gain comes from lookahead selection itself, and reinforcement learning in general doesn't explain it.
• As search guidance, the learned viability critic beats the policy's own value head by +0.218 [+0.188, +0.250] at the 9-item training size. It holds up under zero-shot transfer to 12 to 25 item instances (+0.115 pooled), and past that the edge shrinks with scale: +0.077 at 30 items, +0.055 at 35, and +0.008 by 40, which is inside seed noise. It also replicates zero-shot on a structurally different tight non-guillotine distribution, at +0.306 pooled (200 instances per cell, four critic seeds, up to +0.42 in one cell). 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.
• I re-measured that critic's AUC with a stricter protocol, and the number dropped. The original 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 class prior, the same four critics score 0.9752 ± 0.0018, against 0.9903 ± 0.0012 on their own validation folds. Calibration moves the same way: ECE 0.033 on the strict split against 0.021 in-split. The gap mixes split leakage, checkpoint selection and the class prior, and no run separates them. Instance-disjoint evaluation is the protocol this number needs.
• At rollout with no search, using the critic to restrict the mask itself raises success from 0.082 under plain rollout to 0.201, at one batched estimator call per step. The fair control is a lookahead with the same expansion and no critic (0.096), since expansion alone avoids one-step dead ends. The critic beats it by +0.105 [+0.085, +0.126]. Widening the shortlist to 16 lowers the greedy readout while the restrict-then-policy readouts hold, so the payoff comes from the interface itself, since more candidates don't help. The pooled effect is uneven across the grid: bigger in loose cells than in tight ones.

A theory and audit project (speccomp) on what makes a neural network layer compressible, and whether the usual training-free sensitivity heuristics actually measure it. The main finding is that training-free statistics (spectral spread, per-channel dynamic range, entrywise kurtosis) predict weight-space error for the compression method each one matches, but not output-space damage. Used for mixed-precision bit allocation, the data-free scores do worse than random, while HAWQ's data-dependent Hessian trace beats 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 covering round-to-nearest quantization, pruning and low-rank compression. Under GPTQ it ties HAWQ (WikiText-2 perplexity 60.5 against 60.1, one run per arm) while using one backward pass instead of an 8-probe Hutchinson trace. A Gauss–Newton analysis explains the gap, and its testable prediction about probe noise versus data alignment held up. The main claim survived a pre-registered confirmatory test on a 7-model, 5-architecture panel, with thresholds set before the confirmatory sweep and not changed after seeing the data. The pre-registered primary hypothesis did not survive, and that turned out to be the more useful half of the result. All numbers reproduce from the experiments directory, and everything runs on a single 12 GB GPU.

• 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) using one backward pass instead of an 8-probe Hutchinson trace. It also ranks ahead of it on all 11 cells of a 4-model sweep covering round-to-nearest quantization, pruning and low-rank compression. Uniform allocation beats both on the quantization cells, but only because rounding gives it 4 bits per weight against their 3.5. Held to 3 bits on OPT-350M it loses to every allocator, random included (GPTQ perplexity 115.4 against 76.5 for random and 60.1 for HAWQ).
• The pre-registered confirmatory test used a 7-model, 5-architecture panel of 168 shape-controlled cells, with correlations computed within each architecture and then pooled. The one-backward predictor (weight error times gradient RMS) 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 failure is the result worth reporting. The forward-only activation-RMS signal that beat HAWQ on a single model was worse across the panel (delta rho = -0.179), and forward-only activation statistics are the cheap default people usually reach for.
• 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 goes from 1 to 64, the Hessian score's correlation with output error climbs from 0.21 to 0.50, 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 remaining gap that the data-alignment term predicts. A second prediction, about per-method isotropy, only partly held. The fit was worst for low-rank as expected, but the stable-rank proxy was too crude to order the methods.

Frequency-domain PEFT methods (FourierFT, WaveFT, and wavelet LoRA variants) report gains and credit them to the transform basis. The idea is that a Fourier or wavelet basis captures structure that a plain low-rank update misses. That attribution had never been tested against a matched control, so this project builds one. A basis permutation is orthogonal and energy-preserving, so shuffling the basis order keeps the parameter count, sparsity support and effective rank fixed while destroying the structure the transform is supposed to exploit. Any gain the real basis has over its permuted version is structure. Running the control on FourierFT and a WaveFT-style wavelet adapter with RoBERTa-base on GLUE splits what the transform appears to contribute into three parts, and the basis is the smallest. Magnitude does most of the work, replicating what Zhang et al. (2025) found for LoRA initialization. The collapse people point to as proof that the transform is necessary only happens in one method. FourierFT's no-transform variant drops to the frozen baseline (CoLA MCC 0.000) because its scaling constant is calibrated to a normalized inverse FFT, so removing the transform without rescaling makes the update the wrong size by a factor near 768. Matching the magnitude alone recovers 70-87% of that collapse. The wavelet adapter doesn't need that correction since its inverse DWT is orthonormal, and its no-transform variant doesn't collapse on any of the three tasks (CoLA MCC 0.554 against 0.557 for the true basis). So the main evidence for the transform being necessary is a normalization artifact. Density (the high-rank sparse parameterization) is a real but small remainder, worth 0.026 on MRPC (the mean of accuracy and F1) and 0.072 MCC on CoLA. What's 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, with 90% intervals consistent with equivalence within about ±0.02), and permuting the wavelet basis is harmless on all three. There is one exception: FourierFT on RTE, where the true basis wins in 3 of 3 seeds by a mean 0.041 accuracy margin (paired p = 0.026). It doesn't survive multiple-comparison correction, and two other things keep it modest. The wavelet grid on RTE goes the other way, and a magnitude-matched independent orthogonal basis lands inside the permuted band. With three seeds, RTE is the one place the basis might carry real structure, but three seeds can't demonstrate it. A budget sweep on MRPC at 50, 200 and 1,000 Fourier coefficients per adapted projection keeps the true-minus-permuted gap within ±0.01, even at 50, the tightest budget, where a structural prior has the most room to help. Runs at 5,000 and 20,000 became unstable for both bases, so the claim rests on budgets up to 1,000. The project started as WaRA, a PyTorch library for wavelet-domain LoRA. The FourierFT arms here run on the official peft implementation, and the wavelet arm is a WaveFT-style adapter written for the study.

• I broke down FourierFT's apparent need for its transform on RoBERTa-base across MRPC, CoLA and RTE, with 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 rest is density, the ability of a transform to reach every weight coordinate, worth 0.026 on MRPC (mean of accuracy and F1) and 0.072 MCC on CoLA. The same controls on the WaveFT-style adapter back this up. Its inverse DWT is orthonormal, so its no-transform update is already magnitude-matched, never collapses, and leaves no density gap. This part replicates Zhang et al. (2025), "The Primacy of Magnitude in Low-Rank Adaptation" (NeurIPS 2025), and the paper credits it that way.
• On two tasks out of three, close to nothing is left for the basis. 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 90% intervals are consistent with equivalence within about ±0.02, though three seeds can't certify a tighter ±0.01 band. The one exception is FourierFT on RTE, where the true basis wins in 3 of 3 seeds by a mean 0.041 margin (p = 0.026). Two things temper that: the wavelet grid goes the other way there, and a magnitude-matched independent orthogonal basis lands inside the permuted band. No capacity threshold shows up across the 50, 200 and 1,000 coefficient budgets, including the tightest one, where a structural prior has the most room to help.
• A companion analysis on one fully fine-tuned SAM ViT-B update points the same way. The update's weight matrices sit inside their row-and-column permutation null on average (mean z = +0.14 over 48 layers, with 5 nominally significant at p < 0.05). The same model's patch-token activation grids, by contrast, beat their spatial-permutation null on wavelet low-frequency energy in all 60 image-by-block grids (mean z = +19.1). It's one model and one update, so it illustrates why a structured basis can do nothing in weight space and still make sense for activations, but it doesn't establish it.
• WaRA, the wavelet-domain PEFT library the project started from, includes weight-space and activation-space variants and a parameter-matched LoRA baseline.

An iOS app that scans a room or shipment and builds an optimized 3D load plan, for personal moves as well as freight and container loading. A local Expo native module bridges RoomPlan LiDAR scans and ARKit tap-to-measure for sizing items, with camera intake through react-native-vision-camera. Without LiDAR the app recommends rear dual-camera depth first, then Object Capture, then a TrueDepth hold-up for small items, and finally a marker-assisted estimate and a model prior. The packing core runs on a maximal-empty-space engine in TypeScript, next to classical 2D/3D heuristics (BL/BAF/BSSF/BLSF plus an NFDH shelf packer). Every 3D plan goes through an independent TypeScript verifier, which shares no code with the engine, before the re-ranker picks a plan. Freight mode adds pallet-first planning, container presets, load sequencing, a deterministic scorecard with a profile-aware re-ranker, and carrier handoff docs. For road trailers the verifier checks axle loads at every tandem slide notch, and the planner centers partial loads on the axle balance point. A browser dispatcher takes a load from intake to plan to BOL, CSV or EDI-856 manifest, and then to carrier handoff. The learned packer from the completability study above stays in research. I removed the app's ML path in September, since the service couldn't answer inside the client's own timeout. I also ported the verifier and the engine to Python, so the next policy is trained and scored against what the app ships. The FastAPI /plan endpoint is still live behind a bearer token, and with no servable checkpoint it serves a greedy bottom-left packer.

• Every dimension in a plan records where it came from. A pure arbitration module ranks the three automatic sources: an explicit capture the user did on that item (AR tap-to-measure, TrueDepth hold-up, rear-camera depth, or Object Capture) first, then an auto-matched LiDAR room feature, then a passive label-and-media estimate. It outputs the dimension source, the estimation confidence, the matched feature id, the sensor confidence and the capture asset together, so those fields can't disagree. Typed values outrank all three. On save, the intake form compares what's left in the fields against what the module resolved and marks the source as manual whenever they differ.
• Weights are estimated instead of required, because the safety and loadability kernels would score a weightless load a perfect 1.00. Intake multiplies a per-category bulk-density prior by the item's measured volume. I went with density because it held steadier than mass within a category across the demo fixtures. The two wardrobes come out at 75 and 76 kg/m3 while weighing 90 and 110 kg, and the two dining tables at 47 and 53 kg/m3 while weighing 45 and 75 kg. The priors are fitted to those fixtures and haven't been validated against real weighings, and nine of the twenty-six categories rest on a single observation. A test keeps them within 25% of every categorised demo row, so changing the demo data forces the priors to keep up. The inventory screen and the plan grade both show how many weights were estimated instead of entered.

Mybrary is a native SwiftUI app for macOS, built for a researcher and editor working on a historical journal collection of about 1,000 transcribed pages in 25 volumes. It indexes the collection where it already lives and never changes her files. Search combines keywords (SQLite FTS5) with search by meaning, using Qwen3-Embedding-0.6B vectors searched with Apple's Accelerate framework. Questions in English or French go to Qwen3.5-9B (or the 4B model on a slower Mac), which runs through llama.cpp on the GPU in a sandboxed helper process. A reranker (Qwen3-Reranker-0.6B) picks the passages, a grammar holds the model to an evidence-list answer format, and every quote is checked word for word against its passage before it's shown. When the reranker finds nothing close to a question, the app answers "not found" without running the model. The app never sends her text anywhere, and the network is only used to download the models. Her own work (notes, tags, collections and a registry of people and places) lives in the app's own database.

• The 64 answerable test questions were generated on my Mac by a local model from 74 of her pages across 24 volumes, plus 8 unanswerable ones, without her involvement. Retrieval is the main limit: the source page was among the 60 reranking candidates for 56 questions, and the reranker picked it for 54 of them. Reranking adds about 4.5 s a question and a 639 MB download, so it's only used once she has downloaded the reranker.
• On an M3 Pro, as a stand-in for her 16 GB Mac, the 9B model loaded in 4.2 s and used 5.7 GB of GPU memory in the trial on the same llama.cpp engine, and it writes about 22 tokens per second in the app. The whole collection embeds in about a minute. A full index takes about 20 s, and re-indexing an unchanged collection takes 0.4 s.
• Her files are never modified. The app runs in the App Sandbox, macOS holds her folder read-only except while copying in pages she adds (which never replace a file), a test checks that indexing never changes a file, and the helper that runs the models is granted no files at all. Saving a transcription in her own editor updates the index within seconds. Names are suggested on English pages only, by Apple's on-device tagger, so names on the few pages in French are added by hand.

Expanded Entropy is an Autopsy file ingest module that checks files for possible encryption using Min entropy instead of Shannon entropy. Autopsy's own detector uses Shannon entropy with a default threshold of 7.5 bits per byte, and its entropy test only covers files of unknown type of at least 5 MB (64 KB with a .db extension). At 6.0, the lowest threshold Autopsy allows, a Shannon test flags ordinary PDFs and SQLite databases. Min entropy only looks at the most common byte value, so a file reaches 6.0 only if no byte value makes up more than 1/64 of it. Ciphertext meets that easily, while a PDF with a few percent of padding bytes doesn't. The measures are ordered Min ≤ Rényi(3) ≤ Collision ≤ Shannon, so at the same threshold, switching from Shannon to Min can only remove flags and never adds one. The module reads each file once into a byte histogram, computes all four measures, and raises Autopsy's own Encryption Suspected result with all four values in the comment. No entropy measure can tell dense compression from encryption, so a second stage runs the Huffman-coded data discriminator from Garfinkel, Nelson, White and Roussev (DFRWS 2010) on the files the first stage flags. The earlier experiment behind the choice of Min entropy was my ITIS 5250 course project, and the paper in the repository covers the reasoning and the evidence in full.

• Autopsy's own entropy test only covers files of unknown MIME type that are at least 5 MB (by default also a whole multiple of 512 bytes, and from 64 KB for files with a .db extension), so as shipped it never sees a PDF or SQLite database that Autopsy has identified. PDFs, Office documents and Access databases get a separate password-protection check. By default this module measures every regular file of 1 KB or more that no hash set marks as known, which is where the choice of measure makes a difference. Min entropy at 6.0 is the default, and the settings panel can switch the measure, change the threshold and the Rényi order, cap how much of each file is read, or flag a file when any of the four measures trips.
• The second stage's thresholds come from encrypted data, as in the original method, but from a lot of it: 3,200 MB of AES keystream, cut at the score that 1 in 10,000 blocks fall below. It pools the four difference histograms into one cosine, which is less noisy than the original's smallest cosine over the shifts. A file is called compressed when at least two of up to four sampled blocks fall below the threshold, so an encrypted file with four sampled blocks is miscalled with probability under 1 in 10 million, and at most 2.5 in 10 million given the bound on the per-block rate.
• The paper is explicit about the limits. The second stage only recognizes Huffman-coded data, so headerless data coded another way (xz's range coder, for example) or stored without coding still looks random to it. For formats with a header, the module adds the file type Autopsy identified. Ciphertext with a long run of one byte value, like a zero-padded encrypted container or a file with a long plaintext header, can fall below the threshold under Min, and a flag-if-any option covers that case. The test collection is small and its obfuscated variants are synthetic, so the next step is a measurement on real case images with known encrypted content.