42 papers · 8 project documents
Everything below is open access and every one of them carries a DOI. Full texts are served from this domain; the rest resolve to Zenodo. Ordered most recent first within each group.
Vince Gonzalez · ORCID 0009-0005-3640-014X · tooling at gonzalgo
Axiom dependence in formal libraries · Certified bounds in discrete geometry · Odd perfect numbers · Epistemology · The Modulign standard · Modulign in evidence and law · Modulign validation and protocol · Colour vision and accessibility · Food history and diaspora
What classical assumptions formal libraries actually rest on, and which constant is responsible.
About 70% of Mathlib's theorems transitively depend on Classical.choice , and that figure is read as the library's reliance on the axiom of choice. It is not. In Lean, Classical.choice is the single axiom from which excluded middle and decidability are also de…
The fraction of a formal library's theorems that transitively depend on a discretionary axiom — most often the axiom of choice — is increasingly reported as though it characterised a foundation. This paper measures that quantity across six libraries in four pr…
A machine-checked proof of a program's correctness is conditional on whatever the development assumes, and for deployed software that condition is the whole point. Four Rocq developments are censused with one source-level instrument: the CompCert verified C co…
A formal library's axiom count is routinely reported as a single number. This paper argues that the number conflates two populations which behave differently and answer different questions, and that the conflation is only visible from outside a single library.…
A formal library records which axioms each theorem depends on. Some of those dependencies are removable and some are load-bearing, and the difference is not visible from the dependency graph. Deciding whether an axiom is worth attacking by attacking it costs d…
norm_num closes (2 : ℤ) ≤ 4 through Classical.choice. decide and simp close the same goal without it, and norm_num closes (2 : ℤ) + 2 = 4 without it. The dependence enters through lt_or_eq_of_le : a ≤ b → a < b ∨ a = b, which is stated for a general PartialOrd…
Separating a theorem's statement dependencies from its proof dependencies bounds how much classical dependence a formal library could shed. Across Mathlib, 13.1% of theorems have a choice-free statement and a choice-dependent proof; nothing outside that band c…
A specification for declaring what a body of machine-checked mathematics rests on. CITATION.cff standardises how to cite a project and SPDX standardises its licence. Nothing standardises what it rests on — whether a theorem is standing on an unfinished proof s…
61.2% of Mathlib's theorems depend on Classical.choice. Asking which constant is responsible for that dependence is a different question from asking which constants a proof touches, and the two answers differ by a factor of 58 on the first case examined: 116,7…
A proof assistant reports which axioms a theorem depends on. It does not report which step introduced them, and a proof invoking several tactics offers no way to apportion the answer. The obvious approach is statistical: score each tactic by how often its proo…
A proof assistant can report which axioms a theorem rests on, but only one theorem at a time, and only whether rather than why. I measure axiom use across six libraries and two proof systems - the Metamath databases set.mm (ZFC, classical first-order), iset.mm…
Machine-checked upper and lower bounds for covering, packing and opacity problems.
In 1974 László Fejes Tóth posed the following problem: place n points in the plane so as to minimise the largest distance from a line meeting the unit-radius disc to the nearest point. Writing r_n for the optimum, he proved r_1 = r_2 = 1 a…
Cohn and Li (arXiv:2411.04916) improved the known lower bounds for the kissing number in dimensions 17 through 21. Each of their configurations fixes a large family of vectors and then adjoins further points indexed by a binary code, here called the added-vect…
Lebesgue's universal covering problem, posed in 1914, asks for the convex set of least area containing an isometric copy of every planar set of diameter 1. The known upper bounds descend through a ladder of constructions — the regular hexagon, Pál…
An opaque set for the unit disc is a set meeting every straight line that meets the disc; the infimum of the lengths of such sets is the beam detection constant, whose value is unknown. The best published upper bound, realised by a three-piece barrier of…
An opaque set for the unit disc is a set meeting every straight line that meets the disc. I report a formal verification, in Lean 4 with mathlib, that the three-piece Faber–Mycielski barrier is opaque. The main theorem barrier_isOpaque is proved with no …
Cohn and Li (arXiv:2411.04916) improved the known lower bounds for the kissing number in dimensions 17 through 21 by an odd-sign construction whose final ingredient is a binary code, here called the added-vector code, chosen inside a punctured extended binary …
For a connected vertex-transitive graph on N vertices with adjacency spectrum {(lambda_i, m_i)}, a closed walk based at a vertex is indecomposable (a "first return") if it revisits its base only on the final step. This note records that the first-return counts…
Congruence obstructions on the Euler prime of a hypothetical odd perfect number.
Let N=qkm2 be an odd perfect number in Euler form, so that q≡k≡1(mod4) and gcd(q,m)=1. Write d=(q+1)/2. We observe that d divides m2 for every admissible k, and deduce that q cannot be the Euler prime of an odd perfect number whenever the abundancy index force…
Formal accounts of knowledge, attestation and testimony.
Method-relative modal conditions on knowledge are standardly assessed against a similarity ordering over possible worlds fixed independently of the method: the specification restricts which worlds are quantified over, while the metric is given by the world-spa…
This paper identifies and formalizes a novel adversarial vector in large language model (LLM) safety: the use of inter-model competitive framing to accelerate and deepen safety failures across frontier AI systems. We term this the Competitive Context Exploit (…
Every classification system presupposes an observer. The Modulign Standard (DAG-OR) makes this presupposition explicit through the §OBS and §AUT segments of the dimensional address, which encode not merely who observed but at what level of certified …
The phrase "on the record" is journalism's foundational epistemic claim. It means, at minimum, that a statement or observation is attributable, verifiable, and accountable. Yet no journalism standard specifies what verifiable means formally — by what pro…
Abstract Edmund Gettier's 1963 paper in Analysis demonstrated that justified true belief is insufficient for knowledge: justification and truth can coincide accidentally. The impasse has a structural source: all parties assume justification is specifiable inde…
The dimensional address grammar itself: architecture, formal logic and certification.
The Modulign Observation Registry currently operates as a single PostgreSQL instance maintained by a sole author. This architecture is adequate for a research-stage system but is incompatible with the system's own commitments: the append-only guarantee, the Pe…
This paper presents Modulign (DAG-OR) as a unified research program comprising a formal address grammar for observable phenomena, three interoperable registries, a reproducible classification protocol, and a growing empirical corpus now exceeding 3.79 million …
The problem of reference — what makes a name, description, or term reliably track its object — has generated three dominant frameworks in the analytic tradition: Frege's sense/reference distinction, Russell's theory of definite descriptions, and Kr…
The Modulign Standard v3.0 permits automated systems (%AUT) to produce classifications, including ^EVID-grade classifications, provided domain competence requirements are met. Version 3.0 does not specify how an automated system achieves or demonstrates …
Modulign was conceived in 2026 by Vincent Gonzalez during the development of a live-stream atlas of Earth built as a single static HTML file. The problem was simple on its surface: how do you organize thousands of live video feeds from across the planet so tha…
This document does not explain Modulign. It proves it. Every claim the Standard makes about its own properties — validity, uniqueness, intersubjectivity, non-accidentality, chain-of-custody integrity, and scale-sensitivity — is here ren…
Applying the standard to admissibility, chain of custody and regulatory classification.
When an automated Modulign classification is offered as evidence in a criminal proceeding, the Confrontation Clause of the Sixth Amendment requires that the defendant be able to confront the witness against them. An algorithm cannot be cross-examined. This pap…
Courts in the United States and internationally are now regularly confronted with evidence alleged to be AI-generated, AI-enhanced, or of uncertain synthetic origin — and they lack a formal framework adequate to the problem. Existing evidentiary doctrine…
Digital chain of custody remains a frequently litigated and consequential vulnerability in forensic evidence proceedings. Existing frameworks — NIST SP 800-86, ISO/IEC 27037, the ACPO Good Practice Guide — establish procedural requirements for evid…
The evidentiary problem of AI-generated content is not a disclosure problem. It is an epistemological one. Every major governance framework — the EU AI Act's Article 50, proposed FRE Rule 707, the Take It Down Act, platform watermarking policies — …
This treatise applies the Modulign Standard v3.0 — a Dimensional Address Grammar for Observable Reality (DAG-OR) — as a formal evidentiary and legal codex framework. It establishes four foundational propositions. First, that Modulign-classified obs…
This white paper is a companion document to "Structural Dissolution of the Gettier Problem through Address-Theoretic Epistemology" (Gonzalez, under review at Analysis). That paper establishes the formal epistemological foundation. This paper …
Measuring and correcting the standard in practice.
The Modulign Observation Registry is append-only: no entry is ever modified or deleted after commit. This invariant is foundational to the system's chain-of-custody argument, its legal applications, and its epistemic integrity. But classification errors occur.…
I present the Modulign Standard v3.0, a Dimensional Address Grammar for Observable Reality (DAG-OR): a formal information architecture that assigns a canonical, permanent, cryptographically-anchored address to any observable phenomenon across any physical scal…
This paper reports the first empirical inter-rater reliability study conducted on automated classifiers implementing the Modulign Standard v3.0 — a Dimensional Address Grammar for Observable Reality (DAG-OR). Two independently designed heuristic classifi…
Pseudoisochromatic plate design, generation and recovery.
Pseudoisochromatic plates fall into design types characterised by Hardy, Rand and Rittler: demonstration, transformation, vanishing and hidden digit. The type governs what a plate measures and is ordinarily read from the test's own documentation. This note ask…
Background. Pseudoisochromatic plate tests, exemplified by the Ishihara plates, remain the most widely used screen for red-green color vision deficiency. Online reproductions are now abundant, but most reuse a small set of fixed, scanned plate images, and few …
Naming and transmission in the printed record.
This paper documents the survival of the South Slavic rolled pastry potica/povitica across more than a century in the United States, read through its printed record: community cookbooks, fraternal publications, commercial bakery archives, and mediated recipes.…
Amendments, commitments, datasets and released source. Not papers.
THE RECORD is an append-only, hash-chained ledger assigning Modulign (DAG-OR) addresses to legal documents from the Harvard Caselaw Access Project's openly published static archive. This deposit contains the complete implementation (addresser, pipelines, verif…
Three open datasets covering independent, non-conglomerate American food producers that ship direct to consumers. 1,558 records across 47 states. Every record was researched and verified individually rather than scraped from a directory. What is unusual here i…
14 tables measuring what formal mathematical libraries depend on, produced by one program (gonzalgo) reading proofs that Lean 4 and Metamath have already checked. 10,859 rows, each table as JSON and CSV. module-spend (3,261 rows) — Modules containing at least…
Exact-rational calculator for Norton's function a(j): the least k such that the product of p/(p−1) over the k smallest primes ≥ q strictly exceeds 2. This is the classical abundancy-product obstruction for odd perfect numbers (Servais 1888; Norton 1961, who pr…
In 2026, B. S. Ho published a claimed new lower bound for the kissing number in 19 dimensions: at least 11948 unit balls can simultaneously touch a central unit ball without overlapping (arXiv:2603.10425), improving the previous bound of Cohn and Li by 256. Th…
Client-side JavaScript source for the browser-based procedural pseudoisochromatic (Ishihara-style) colour-vision plate generator (PPPG). Generates plates at runtime — no server, no stored images. Companion code to the preprint of the same name.
This document specifies all amendments to the Modulign Standard that constitute version 3.1. It is a formal amendment document — not a replacement of the v3.0 specification. All v3.0 provisions not explicitly amended remain in force. The v3.1 complete sp…
Modulign is a classification standard — a grammar for assigning addresses to observable phenomena. It does not operate cameras. It does not collect surveillance footage. It does not monitor individuals. It does not build profiles of people's movements, behavio…