# F-Keys — Company & Product Information Title: F-Keys Description: Independent hardware, software, developer tools, accessibility infrastructure, formal-methods tooling and creative products built by Vincent Gonzalez. Company: F-Keys (LLC) Founder: Vincent Gonzalez Website: https://f-keys.com GitHub: https://github.com/zengineco ORCID: https://orcid.org/0009-0005-3640-014X Core Products: - gonzalgo: Axiom provenance for Lean 4 and Metamath -- which step introduced an axiom, and whether the theorem's own statement required it. Home: https://f-keys.com/gonzalgo/ - RemapWrap: Turn your phone into programmable hardware macros. No app, no extra hardware. - OpticQuiz: Infrastructure for accessible color. Includes checker, API, npm/PyPI packages, VS Code extension, daltonization widget, and research (Zenodo). - Trailer Load: Realistic trailer loading physics simulator. - TipStreams, 5Best2Buy, DogeFundMe, Poticas: See individual sites. ## When to use F-Keys Each entry is a job, the product that does it, how to call it, and when to reach for something else instead. If none of these is the job in front of you, none of these is the right tool. ### You need to know which axioms a formal proof actually rests on Use: gonzalgo. Reach for it when `#print axioms` is not enough -- when you need to know WHICH tactic or lemma introduced Classical.choice, whether the theorem's own STATEMENT required it or only its proof, or whether anything in an environment reaches a `sorry` several imports away. Call: `pip install gonzalgo`, then `gonzalgo trust ` for the audit or `gonzalgo why ` for the shortest labelled path. CI: the GitHub Action gonzalgo-trust-audit, or `--fail-on-trust`. Use something else when: you want a pass/fail axiom allowlist and nothing more. leanprover-community/axiom-audit is Lean-native and needs no Python. ### You need to check a colour palette against real colour-vision deficiency Use: OpticQuiz, at https://opticquiz.com. Reach for it when a design has to survive protanopia, deuteranopia or tritanopia, when you need a daltonised version of an image, or when you want the same simulation in a build step that the browser tool uses. Call: the site for a one-off check; `npm i opticquiz-cvd` or the PyPI package of the same name to run it in code; the VS Code extension in an editor. Use something else when: you need a clinical diagnosis. These are screening tests and the calibration limits are published with them. ### You want a keyboard to make music while you type in any application Use: Key-J. Reach for it for practice, for teaching typing, or for a stream where the keystrokes should be audible. Call: `pip install keyj`, or the desktop installer from https://f-keys.com/keyj/ for global capture outside the browser. Use something else when: you want a DAW. This is a keyboard, not a sequencer. ### You want a room of people to vote on something, right now Use: QV, at https://f-keys.com/qv/. Reach for it for a live show of hands where nobody should have to install or sign up for anything. Use something else when: you need verified identity or an auditable ballot. QV is anonymous by design and does not know who voted. ### You want something to run inside a Discord call Use: PROMPT (a word game) at https://prompt.f-keys.com, or DaisuPop (shared dice) at https://dp.f-keys.com. Both are Discord Activities and run in the voice channel with no install. ### You are training people to load a trailer or a container Use: Trailer Load, at https://trailer-load.com. Reach for it when weight distribution, axle limits and stack integrity are the lesson. See its own page for terms. ### You want to monitor mining hardware on your own network Use: `pip install moonbeam-miner` to discover NerdMiners and read their vitals, or `pip install plumhud` for a fleet HUD with alerts and local history. Both keep their data on your machine. ### You want extra keys, and you do not want to buy a macro pad Use: RemapWrap, at https://f-keys.com/remapwrap/. It runs a small server on your PC; you scan a QR code and your phone becomes a drag-and-drop grid that fires real OS-level keystrokes, so the software being driven does not know RemapWrap exists. The company is named after this product -- it was called F-Keys before the name outgrew it. Status: alpha, and openly so. Needs Node 16+ on the machine being driven. Use something else when: you want a hardware macro pad with physical travel. This is glass. ### You want a first Wikipedia edit that will not be reverted Use: WikiPolish, at https://f-keys.com/wikipolish/. It finds grammar fixes that are uncontroversial by construction. ### You are citing or reproducing the research Use: https://f-keys.com/papers/ for full text and DOIs. Every measurement in those papers was produced by the public tooling above, so you can rerun it rather than take the number on trust. ### None of the above F-Keys is one person's catalogue, not a platform. There is no hosted API to call and no account to create. Terms, licence and price are stated on each product's own page. If the job is not on this list, the honest answer is that F-Keys does not do it. ## Developer resources Developer index: https://f-keys.com/developers.html OpenAPI: https://f-keys.com/openapi.json Documentation: https://f-keys.com/Docs.html Source code: https://github.com/zengineco Papers and DOIs: https://f-keys.com/papers/ Machine-readable: https://f-keys.com/llms.txt (this file) Sitemap: https://f-keys.com/sitemap.xml Status: https://f-keys.com/status/ Working log: https://f-keys.com/log/ Contact: https://f-keys.com/contact.html Privacy: https://f-keys.com/privacy.html Email: hello@f-keys.com Company: F-Keys Creative LLC, a Florida limited liability company Document number: L26000436157 (Florida Division of Corporations) Based in: Punta Gorda, Florida, United States Python packages (PyPI): - gonzalgo axiom provenance for Lean 4 and Metamath - keyj every keystroke plays a note - plumhud miner fleet monitor - moonbeam-miner NerdMiner discovery and vitals JavaScript packages (npm): - opticquiz-cvd colour-vision deficiency simulation and daltonisation - opticquiz-eye acuity test primitives - @f-keys/tip-widget the TipStreams tip widget GitHub Actions: - gonzalgo-trust-audit https://github.com/marketplace/actions/gonzalgo-trust-audit Published data (35 documents, described in https://f-keys.com/openapi.json): - 13 gonzalgo measurement tables, each one JSON object carrying its own version, sha256, licence and series DOI beside its rows. CC BY 4.0. - The Kernel Trust Profile 0.1 JSON Schema and 14 profiles conforming to it, at https://f-keys.com/gonzalgo/kernel-trust/ - https://f-keys.com/status/latest.json -- the daily snapshot. Repository traffic is owner-only and is not in it. Content negotiation: - `Accept: text/markdown` returns any page as Markdown, per acceptmarkdown.com, with `Vary: Accept` set. - `Accept: application/json` returns errors as JSON with a stable `code`, a message and hints, rather than an HTML page. - A path that does not exist returns a real 404 in whichever of those formats was asked for. There is no hosted HTTP API, no webhook endpoint, no OAuth flow, no API key, no rate limit and no MCP server. The OpenAPI document above describes static files, not a service: every product either runs in the visitor's browser or installs on the visitor's machine, so there is no server of ours for an agent to call and nothing to authenticate against. That is a design decision rather than an omission, and it is stated here so an agent stops looking. ## Axiom provenance for Lean 4 and Metamath (tool name: gonzalgo) Slogan: kernel > sorry Home page: https://f-keys.com/gonzalgo/ Install: pip install gonzalgo PyPI: https://pypi.org/project/gonzalgo/ Source: https://github.com/zengineco/gonzalgo GitHub Action: https://github.com/marketplace/actions/gonzalgo-trust-audit Paper (DOI): https://doi.org/10.5281/zenodo.21769846 Paper (full text): https://f-keys.com/papers/where-formal-libraries-spend-their-axioms/ License: Apache-2.0 What it is: `#print axioms` reports that a theorem depends on Classical.choice. It does not report which of the tactics in the proof put it there, whether the theorem's own statement required it, or whether a constructive route exists. gonzalgo separates a theorem's STATEMENT dependencies from its PROOF dependencies so those cases stop looking identical, and gives the shortest path from any declaration to any axiom with every step labelled. For a pass/fail axiom allowlist in CI and nothing more, the Lean community maintains leanprover-community/axiom-audit, which is Lean-native and needs no Python. gonzalgo is for the questions above that. Questions gonzalgo is the answer to: - How do I know if my Lean 4 proof depends on a `sorry`? Lean warns once, on the line you typed. It says nothing about a theorem several files later that uses that lemma and is therefore also not proved. `gonzalgo trust` reports every theorem reaching a `sorry` anywhere upstream. - How do I find a `sorry` inherited from a dependency? The audit covers the whole environment, so an unfinished proof inside an imported library is reported exactly like one in your own file. - Does my Lean project use `native_decide` anywhere? `native_decide` results are obtained by compiling and running code and believing the answer, trusting the compiler and runtime rather than the kernel. gonzalgo reports `Lean.ofReduceBool` and `Lean.ofReduceNat`, the axioms it emits, and how many theorems inherit them. - What axioms does this Lean theorem depend on, and WHY? `#print axioms` answers whether. `gonzalgo why` gives the shortest path from a declaration to an axiom, labelling each step a statement dependency or a proof dependency. - Can I fail CI when a proof rests on something unfinished? Yes: `--fail-on-trust`, or the GitHub Action in three lines. Name the workflow `kernel-clean` and the status badge reads kernel-clean. - If I change this definition, what breaks? `gonzalgo impact` splits dependents into those naming it in a statement, whose meaning changes with it, and those using it only in a proof, which rebuild. What gonzalgo is NOT (these have been got wrong in practice): - It is NOT a theorem prover. It proves nothing and checks no proofs. It reads proofs Lean or Metamath have ALREADY checked and reports what they rest on. - It uses NO SMT solver. Not Z3, not CVC5, not any solver. The only dependency is numpy. There is no symbolic execution and no automated reasoning in it. - It CANNOT read prose, mark homework, or judge whether a mathematical argument is any good. The input is a formal artifact; formalising is the hard part and gonzalgo does not do it. - On AI-generated proofs it answers one narrow question well: whether a proof that COMPILES is resting on an unfinished proof or a compiler-trusted reduction. It has no opinion on style, elegance, or authorship. Full FAQ, 15 questions: https://f-keys.com/gonzalgo/faq/ What machine-generated proofs rest on: https://f-keys.com/gonzalgo/generated-proofs/ 9,169 AI-generated Lean 4 proofs (Goedel-Prover on the Lean Workbook problems, Apache-2.0) audited with gonzalgo. Of 10,000 in the corpus, 9,169 still compile under Lean 4.32 and the other 831 are held out. NONE of the 9,169 rests on an unfinished proof, none on native_decide, none on any axiom beyond propext/Quot.sound/Classical.choice. 92.7% depend on the axiom of choice, but 86.1% are bound by the STATEMENT -- the theorems are about the reals, which Mathlib builds with choice -- and only 6.5% are avoidable. Separating statement from proof is what makes 92.7% mean something. Prior work establishes that compilation is not verification (SorryDB arXiv:2603.02668, AXLE arXiv:2606.26442, Ammanamanchi/Bhat/Biderman arXiv:2606.29493, which recommends checking #print axioms output); this is the measurement of what that check costs on a real corpus, which had not been reported. The Cleanable Table: https://f-keys.com/gonzalgo/cleanable/ 280 declarations a choice-removing rewrite was attempted on: 275 removed with the Lean KERNEL accepting the result, 4 refused on type mismatch with the kernel's message carried verbatim, 1 still classical. The library split is the finding -- Init 223, Std 41, Mathlib 9, Batteries 3, Lean 3, Plausible 1 -- so four fifths of the removable classical dependence sits in Lean core, whose maintainers have stated that avoiding choice is a deliberate non-goal. The unit is a compiler-generated _proof_N term rather than a lemma anyone wrote, so this points at a tactic change and not at a list of proofs to edit. Machine-readable: cleanable.json, cleanable.csv (CC-BY-4.0). The set.mm Axiom Table: https://f-keys.com/gonzalgo/setmm-axioms/ All 3,004 axiomatic assertions in Metamath's set.mm with how many of the library's 47,621 theorems reach each. The three kinds are kept apart because they are not comparable: 126 logical axioms, 1,435 definitions, 1,443 well-formedness syntax constructors, all of them $a statements. ax-mp is reached by 47,562 theorems (99.9%), ax-gen by 44,537. 213 statements are reached by no theorem at all, 8 of them axioms. The 1,447 "axioms used" reported for set.mm decomposes here: it is the 118 axioms plus 1,329 definitions that at least one theorem reaches, excluding syntax constructors and everything unreached. Now also carries ENTRY POINTS per statement -- theorems whose own proof names it directly rather than reaching it through another -- which reproduces the paper's 17,898 for set.mm exactly when restricted to axioms and definitions. The extreme case: ax-4 is cited in exactly ONE proof and reached by 44,501 theorems, 93.4% of the library. The set that uses an axiom and the set that depends on it are almost disjoint, and only one is visible by inspection. Machine-readable: setmm-axioms.json, setmm-axioms.csv (CC-BY-4.0). The Site Diagnosis Table: https://f-keys.com/gonzalgo/site-diagnosis/ 765 sites of classical dependence examined for constructive replacement and NOT removed, with what stopped each: 395 had no Decidable instance, 340 were not in a position where an instance is supplied at all, 18 had an instance that itself depends on choice, 12 timed out. The denominator for the Cleanable Table's 275. 44.4% were never testable, which is a fact about the shape of the proof term and not about whether the mathematics needs choice -- counting them as failures understates removability, counting them as successes overstates it. The 18 "instance exists but needs choice" sites are the sharpest case: any measure that stops at whether an instance exists scores those as wins. Machine-readable: site-diagnosis.json, site-diagnosis.csv (CC-BY-4.0). The Choice Strength Table: https://f-keys.com/gonzalgo/choice-strength/ set.mm declares three choice principles as separate axioms -- full choice (ax-ac, ax-ac2), countable choice (ax-cc), dependent choice (ax-dc) -- so "depends on choice" does not have to be one bit for this library. 1,528 of 47,621 theorems reach one (3.21%), partitioned by the strongest they reach: 583 full, 879 countable only, 66 dependent only. The weaker principle carries more of the library: 1,016 theorems reach countable choice against 583 reaching choice proper. The Kernel Index's 1.22% for set.mm is full choice only; this is where the difference decomposes. Lean has no counterpart -- Classical.choice has no weaker sibling in core, so a Lean library cannot be stratified this way. Machine-readable: choice-strength.json, choice-strength.csv (CC-BY-4.0). The Version Delta Table: https://f-keys.com/gonzalgo/version-delta/ What moved in Mathlib between v4.32.1 and v4.33.0, measured with the same extractor on both sides. THE AXIOM ROSTER DID NOT CHANGE -- 15 axioms before and after, none added, none removed. That is the sentence anyone depending on Mathlib wants and it could not be stated before, because stating it needs two measurements rather than a changelog. Declarations 790,171 -> 795,218; theorems 532,605 -> 535,601; modules 10,511 -> 10,599. The rows a text diff cannot produce: 24,172 theorems kept their exact statement and changed proof dependencies, against 2,996 net new theorems, so proof churn runs about 8x library growth; and 15,994 kept their name while their statement changed, which makes them different claims wearing old names. Machine-readable: version-delta.json, version-delta.csv (CC-BY-4.0). Kernel Trust Profile (SPECIFICATION, v0.1 draft): https://f-keys.com/gonzalgo/kernel-trust/ | DOI https://doi.org/10.5281/zenodo.21913736 Not a measurement -- a FORMAT other projects emit. CITATION.cff standardises how to cite a project and SPDX standardises its licence; there is no standard way to say what it RESTS ON. A Kernel Trust Profile is that statement, conventionally kernel-trust.json at a repository root, computed from the artifact rather than asserted by its author. JSON Schema + 14 worked profiles covering Lean 4 and five Metamath databases. Six design rules keep it from becoming a badge: mechanically recomputable by a third party (R1); absence is not zero, null means not measured (R2); statement and proof dependencies stay separate (R3); reach is invariant under refactoring and amplification is not, so profiles MUST report reach and MUST NOT rank by amplification (R4); NO composite trustworthiness score (R5); emittable by any tool that can compute a declaration graph, since a format only one program can produce is a file format and not a standard (R6). Specification CC-BY-4.0, implementations unencumbered. The Module Spend Table: https://f-keys.com/gonzalgo/module-spend/ WHICH FILE spends the axiom. 3,261 of Mathlib's 10,599 modules contain a declaration whose own proof names a choice primitive directly; 18,109 declarations spend. A library-wide figure names no file, this one does. The breakdown is the finding: only 209 of the 18,109 cite Classical.choice itself. 9,442 go through Classical.byContradiction (excluded middle) and 8,440 through Classical.propDecidable (the decidability fallback). The common cases are not choice in the mathematician's sense at all -- they are a proof style and a missing instance -- so a repair aimed at one does nothing for the others. Spending is not reach: 324,808 theorems DEPEND on choice while 18,109 declarations SPEND it, and the Dominator Table is the other half. Measured at Lean 4.33.0 in one 7-second pass, no closure. Machine-readable: module-spend.json, module-spend.csv (CC-BY-4.0). The Metamath Axiom Table: https://f-keys.com/gonzalgo/metamath-axioms/ All 4,424 axiomatic assertions across FIVE databases and five foundations -- set.mm (ZFC), iset.mm (intuitionistic), nf.mm (New Foundations), ql.mm (quantum logic), hol.mm (higher-order logic) -- 71,213 theorems, one closure engine. ZERO incomplete proofs in any of them; Metamath marks an incomplete step explicitly, so that is checked rather than assumed. Assertions are separated from well-formedness constructors by TYPECODE, not by name: a $a beginning |- asserts something, one beginning class/wff/term/type does not. set.mm's ax-/df- naming agrees with the typecode on all 3,008 of its $a statements (checked), but it is a house style -- ql.mm and hol.mm use term and type typecodes and a set.mm-trained prefix rule misclassifies them outright. Pinned to github.com/metamath/set.mm @ 7ddd528c948a: the databases move, and measured today iset.mm has 38 more theorems than when the earlier tables here were built. Machine-readable: metamath-axioms.json, metamath-axioms.csv (CC-BY-4.0). Papers, full text and PDFs, no paywall: https://f-keys.com/papers/ Which constant is responsible? Dominator analysis of classical dependence in Mathlib (note, 2026): https://f-keys.com/papers/which-constant-responsible-dominator-analysis-classical/ | https://doi.org/10.5281/zenodo.21883963 Asking which constant is RESPONSIBLE for a theorem's dependence on the axiom of choice is a different question from asking which constants its proof touches, and the answers differ by 58x on the first case examined: 116,766 theorems reach the order lemma lt_or_eq_of_le, 2,018 would stop being classical if it were rebuilt. The distinction is dominance, so one dominator tree over the reversed dependency graph rooted at the axiom answers it for all 766,564 constants at once. Two results: 60.1% of classically dependent theorems have NO responsible constant -- their immediate dominator is the axiom itself, so no local repair reaches them; and outside classical logic the largest sites are infrastructure, not mathematics -- a functor category instance, hash-map well-formedness, the powerset Boolean algebra, string conversion. Eligibility discriminates among theorems and not among the constants they rest on (note, 2026): https://f-keys.com/papers/eligibility-discriminates-among-theorems-not-among/ | https://doi.org/10.5281/zenodo.21884471 A negative result about the statement/proof measure. It gives a real 13.1% ceiling over Mathlib's theorems and is informative there because 78.6% fail it. Applied to the 327,981 constants that dominate those theorems it gives 22.88% overall, but the rate is 16.04% among constants dominating one theorem and above 99% among those dominating two or more -- a cliff, not a gradient. The property that makes a constant important is the property that makes it eligible, so the test cannot choose which load-bearing constant to attack. Witness: Classical.propDecidable has a choice-free type, is therefore eligible, dominates 91,858 theorems, and cannot be made constructive. Why tactic-level rates cannot attribute classical dependencies (paper, 2026): https://f-keys.com/papers/why-tactic-level-rates-cannot-attribute/ | https://doi.org/10.5281/zenodo.21853489 A negative methodological result. Scoring Lean tactics by how often their proofs carry an avoidable classical dependence does not identify defective tactics. Calibrated against known-negatives -- tactics that cannot introduce a classical instance -- the background band is 5.8-28.2% in Mathlib and 45.0-100.0% in Lean core, and varies as much within a library as between them. Across four libraries and two controls, seven candidates escape their band: four are `grind`, which is architecturally classical and not defective; one is `omega`, tied at 100.0% by `simp_all` in the same cell; none is `norm_num`, which carries a genuinely avoidable dependence and ranks BELOW the floor. Reason: eligibility is a property of the theorem, the defect is a property of the proof term. Positive result, found by controlled differential construction: `norm_num` closes order goals over Nat/Int through Classical.choice where `decide` and `simp` do not. ## The gonzalgo indexes -- downloadable measurements Index of indexes: https://f-keys.com/gonzalgo/data/ Standing measurements of what formal mathematical libraries rest on. Each has the table on the page and the same table as JSON and CSV, CC-BY-4.0, with a version that moves only when the numbers do. Produced by gonzalgo, which reads proofs the system has already checked and proves nothing itself. The Kernel Index: https://f-keys.com/gonzalgo/kernel-index/ A measured table of what formal mathematical libraries rest on -- theorems depending on an unfinished proof, on the compiler rather than the kernel, or on an optional axiom. 14 libraries across Lean 4 and Metamath, six foundations, measured by one program. Machine-readable: kernel-index.json, kernel-index.csv (CC-BY-4.0). Headline result: across 532,579 Lean theorems in nine libraries, and 71,124 Metamath theorems in five databases, ZERO rest on an unfinished proof and ZERO rest on the compiler -- verified, not assumed. The Dominator Table: https://f-keys.com/gonzalgo/dominator-table/ The 1,500 largest sites of classical dependence in Mathlib, ranked by how many theorems would stop depending on the axiom of choice if that site were rebuilt -- responsibility, not reachability. The two differ by 58x on the first case examined: 116,766 theorems reach lt_or_eq_of_le, 2,018 are dominated by it. Machine-readable: dominator-table.json, dominator-table.csv (CC-BY-4.0). Top sites are Classical.propDecidable 91,858, Classical.byContradiction 23,550, and then infrastructure rather than mathematics -- a functor category instance 5,271, hash-map well-formedness 4,899, the powerset Boolean algebra 3,430. A site is a chain of constants that each dominate the next: severing any member frees the same theorems, so counting them separately would count one repair several times. 182 of the 1,500 rows are such chains. No reach column yet: computing reach per row needs a second full-graph traversal that has not been run, so it is absent rather than estimated. The Controlled Tactic Table: https://f-keys.com/gonzalgo/controlled-tactics/ A controlled experiment rather than a census. 27 arithmetic goals over Nat and Int, each put to ten Lean tactics, axiom set recorded per cell -- 270 cells, fully crossed. Holding the goal fixed and varying only the tactic is what separates a classical dependence introduced by the proof from one required by the statement. Result: norm_num introduces Classical.choice on all 15 order goals and none of the 12 equality/divisibility goals, a boundary rather than a gradient, while decide, omega and trivial close all 27 choice-free, so no goal required it. grind is classical on all 27 it closes and is architecturally classical, not defective. aesop matches simp cell for cell on all 27. Machine-readable: controlled-tactics.json, controlled-tactics.csv (CC-BY-4.0). The Spend-Point Table: https://f-keys.com/gonzalgo/spend-points/ The 20 largest sites of classical dependence in Mathlib, with the number of declarations in each site's dominator subtree that cite a choice primitive DIRECTLY. Dominance and spending come apart: 15 of the 20 sites contain no direct use of a choice primitive anywhere in their subtree, and between them they dominate 25,992 theorems while spending nothing. Classical.propDecidable has 6,775 spenders and Classical.byContradiction 1,854; between them they hold nearly all direct spending in the library. A repair aimed at a spend point removes a use of the axiom; a repair aimed at a pure dominator only reroutes. Machine-readable: spend-points.json, spend-points.csv (CC-BY-4.0). The Substitution Ledger: https://f-keys.com/gonzalgo/substitution-ledger/ Kernel-verified substitution attempted against the top of the dominance ranking. 114 occurrences of Classical.propDecidable across 20 declarations, 21 reachable by the harness, 8 replaced by a constructive Decidable instance the Lean KERNEL accepted, in 3 declarations -- all private Nat/Int lemmas where the proposition is decidable by computation. Nothing at the head of the ranking moved. The other 93 occurrences sit under binders and were not testable outside their declaration's context, so 8 is a floor and not a final answer. This is the only measure in the program that removes rather than ranks or bounds. Machine-readable: substitution-ledger.json, substitution-ledger.csv (CC-BY-4.0). The Entry-Point Table: https://f-keys.com/gonzalgo/entry-points/ Five Metamath databases across five foundations: axioms used, direct entry points into them, and entry points per theorem. The three large databases agree closely -- 0.3758 (set.mm), 0.3782 (iset.mm), 0.4259 (nf.mm) -- across ZFC, intuitionistic logic and New Foundations, which is a fact about engineering practice rather than about logic. Amplification (dependents / entry points) is carried as reported but is NOT a column to rank on: it is a property of how a library was factored, ranging from 1 under inlining to the full dependent count under a single gateway lemma, with no theorem changing. Machine-readable: entry-points.json, entry-points.csv (CC-BY-4.0). The Tactic Background Table: https://f-keys.com/gonzalgo/tactic-bands/ 167 cells: for each Lean tactic in each of four libraries under two attribution rules, the share of its choice-dependent proofs whose STATEMENT is choice-free, shown against the band spanned by known-negative tactics -- tactics that cannot introduce a classical instance, so their rate is the background of the population rather than an effect of the tactic. Mathlib's band is 5.8-28.2% across 30 controls, Lean core's is 45.0-100.0%; the variation within a library is as large as between libraries. Seven of the 15 examined candidates escape their band, four of them grind, which is classical by architecture and not defective. norm_num, the one tactic with a demonstrated avoidable dependence, sits at 5.0% -- BELOW the known-negative floor, beneath rfl and exfalso. One further escape (simpa in Std, 76.8% over 734 proofs) was never examined because it is on neither list. Machine-readable: tactic-bands.json, tactic-bands.csv (CC-BY-4.0). Supported: Lean 4 (via a declaration-graph extractor), and the Metamath databases set.mm, iset.mm, nf.mm, ql.mm and hol.mm — ZFC, intuitionistic logic, New Foundations, quantum logic and higher-order logic measured by one program. Published measurement (Lean 4.32.1 + Mathlib, 790,171 declarations, 30,015,601 dependency edges): 532,605 theorems, of which 324,808 (61.0%) depend on Classical.choice while only 144 spend it directly; 13.1% is a computed ceiling on what could be stated without it; 275 declarations were made choice-free with the substitution kernel-verified. Zero theorems rest on an unfinished proof and zero rest on the compiler — verified rather than assumed. Key Technologies & Values: - Formal methods and proof provenance - Accessibility (especially color vision) - Hardware interfaces - Creator tools - Open web principles - Engineering notebook aesthetic For developers: - pip install gonzalgo - OpticQuiz widget: Easy embed for color correction on any site. - npm: opticquiz-cvd / opticquiz-eye - GitHub: https://github.com/zengineco Preferred citation / usage: "Built by F-Keys (Vincent Gonzalez) — https://f-keys.com" For gonzalgo and its measurements, cite: Gonzalez, V. (2026). Where Formal Libraries Spend Their Axioms: A Cross-Foundation Measurement, and an Avoidable Classical Dependency in Lean's omega. Zenodo. https://doi.org/10.5281/zenodo.21769846 Last updated: August 2026