This page lists arXiv submissions and working drafts on constructive logic and the theory of computation.
The list follows the date of the most recent arXiv revision.
May–July 2026
arXiv:2605.18924 [math.LO] arXiv
This paper proves an obstruction theorem for primitive closure predicates in the implication-falsity fragment. A Rocq development checks the proof. The theorem distinguishes generative evaluation completeness from decisional excluded-middle completeness. Together, these properties force a reflective fixed point whose classification yields inconsistency under modus ponens.
November 2025–July 2026
arXiv:2511.07774 [math.LO, cs.LO] arXiv
This paper gives a proof-theoretic account of the constructive classification of positive integers as 1, prime, or composite. It develops bounded decision procedures, a recursive prime sieve, modular cancellation, and finite arithmetic certificates. It distinguishes the internal results of Heyting Arithmetic from results that depend on the standard interpretation of natural numbers.
Note: This research project is complete.
October 2025–June 2026
arXiv:2510.08934 [math.LO, cs.LO] arXiv
This paper studies the boundary between local self-application and global self-certification. It treats irrational quantities as procedures with effective rules that refine their approximations. The golden ratio Φ provides a model of stable local recurrence. The reciprocal update R(x)=1+1/x has a unique positive fixed point and allows finite, witnessed approximations.
September 2025–May 2026
arXiv:2509.10382 [math.LO, cs.LO] arXiv
This paper encodes two natural numbers as one through Fibonacci-based representations. The method does not use multiplication, factorization, or digit interleaving. Its encoding and decoding procedures remain simple and predictable. The paper proves that the encoding is injective and that a procedure can recognize valid encoded numbers. A Rocq development checks the main results.
October 2025–April 2026
arXiv:2510.00759 [math.LO] arXiv
For each fixed resource limit, this paper represents syntactic proof checking as a finite system of cubic Diophantine equations. The variables range over a bounded domain. The current version withdraws an earlier, stronger claim. That claim described a reduction from unbounded theoremhood to one fixed, bounded-domain cubic instance.
Note: This research project is complete.
December 2025
arXiv:2512.08149 [math.LO] arXiv
This paper identifies a structural obstruction to the uniform separation of two classes in constructive arithmetic. The obstruction does not depend on the meaning of the classes. It occurs when a system maintains two evaluator predicates in parallel and represents inference uniformly.
November 2025
arXiv:2511.21296 [math.LO] arXiv
This short philosophical paper argues that admissible measurement limits physically meaningful propositions. Admissible measurements can extract finite observation sequences, terminating procedures, or stable uniform conditions.
November 2025
arXiv:2511.14665 [cs.CC] arXiv
This paper analyzes global decision problems over arithmetically represented domains. It studies how class quantification introduces impredicativity into formal problem spaces. The analysis connects diagonalization, reflection, and uniform complexity statements.
January 2026
Read the self-hosted PDF.
This draft presents a logical pipeline for EMNIST classification. It makes preprocessing, prediction rules, training traces, and evaluator behavior replayable and checkable. The pipeline uses integer-valued repair steps instead of an opaque optimization run. These steps expose decidable invariants and specific counterexamples when a step fails.