32 deposited works · 28 full texts here
Everything below has a DOI and is open access. 28 of the 32 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
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…
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…
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 (…
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 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 …
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 …
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…
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.…
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…
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…
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…
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…
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…
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 — …
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 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…
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 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 …
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…
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 …
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.…
The Kernel Index — what 14 formal libraries across six foundations rest on, measured by one program.
What machine-generated proofs rest on — 9,169 AI-written Lean 4 proofs audited.