Excerpts from deposited papers, measurement write-ups and software documentation. Each one links to where it came from. The papers carry DOIs, so the deposited text cannot be changed after the fact, and the documentation links to the file in the repository.
Findings that turn on a quantity, and what the quantity is allowed to support.
Asking which constant a theorem's classical dependence is responsible to is not the same as asking which constants its proof touches, and the answers are far apart. 116,766 theorems reach the order lemma lt_or_eq_of_le; 2,018 would stop being classical if it were rebuilt.
It does not say how far each use travels, and the two are wildly different: 324,808 theorems depend on choice while 18,109 declarations spend it.
For Mathlib that is 13.1% of theorems, against a figure of 55% that circulates without a measurement behind it.
The result is a boundary rather than a gradient. norm_num introduces the axiom of choice on all 15 order goals (≤, <, ≥ over Nat and Int) and on none of the 12 equality and divisibility goals.
15 of these 20 sites contain no direct use of a choice primitive anywhere in their subtree.
What the work does not establish, written down where the result is.
It does not assert that tau(20) = 19448 or tau(21) = 29768; both remain open, and other constructions are not excluded.
For n = 6 an unstructured search converged back to Fejes Toth's own configuration and produced no improvement; that is reported as a negative result, not as evidence of optimality.
The method therefore constitutes a screening stimulus generator, not a measurement instrument, and cannot classify deficiency type or grade severity.
Unsupervised recovery of the figure/ground assignment itself was also attempted and fails: recall reaches 100% on ten plates while precision falls to 38 to 63% on the vanishing plates, with no confidence signal distinguishing successes from failures.
A library reaching 61% of its theorems with the axiom of choice has made a design decision, not an error.
Why a number is trustworthy, or why an earlier one is not.
Compile failures are held out of every figure here; a corpus targeting Lean 4.27 measured under 4.32 would otherwise report version drift as a property of the proofs.
A previous run over the same question returned 404 synthesis timeouts against this run's 12, and had no not-a-goal category at all, so nearly every site it could not clean was recorded as a time limit being hit.
Of 114 occurrences only 21 were testable at all. The rest occur under binders, where the proposition is not closed and cannot be handed to instance synthesis from outside its declaration.
Openings and load-bearing claims from the written papers.
This document does not explain Modulign.
Every classification system presupposes an observer.
The evidentiary problem of AI-generated content is not a disclosure problem.
not because any rule prohibits its admission, but because its address structure formally encodes the absence of the causal chain that observational authentication requires
Software documentation, including the parts a reader is entitled to be warned about.
keyj play installs a system-wide keyboard listener, which is the same machinery a keylogger uses.
If node is not installed the parity checks skip and say so, because a check that cannot run must not report success.
A tab in a tuning that does not exist comes back with .error set and no notes, rather than raising.
so the package and the page cannot answer differently
Dark grey on navy measured 2.64:1 where body text needs 4.5, and a person found that, not a build.
Three gates for defects a linter does not have an opinion about, because none of them is a syntax error.
Both halves matter: a gate that cannot tell those apart gets switched off.
The full list of deposited work is at /papers/, the measurements at /gonzalgo/, and the products at /portfolio. CVs: /cv/.