Preliminary overview of papers, preprints, and working drafts in (constructive) logic.
Listed from most recent arXiv revision.
2026
arXiv:2605.18924 [math.LO] arXiv
Proves and mechanizes in Rocq an obstruction theorem for primitive closure predicates over the implication-falsity fragment. The paper separates generative evaluation completeness from decisional excluded-middle completeness and shows that their conjunction forces a reflective fixed point whose classification collapses to inconsistency under modus ponens.
2025–2026
arXiv:2509.10382 [math.LO, cs.LO] arXiv
Introduces a way to encode two natural numbers into one natural number using Fibonacci-based representations. The method avoids multiplication, factorization, or interleaving digits, and it is designed so encoding and decoding stay simple and predictable. It proves that the encoding is one-to-one, that valid encoded numbers can be recognized, and that the main results were formally checked in Rocq.
2025–2026
arXiv:2510.00759 [math.LO] arXiv
Proves a bounded compilation result: for each fixed resource limit, checking a syntactic proof can be represented by a finite system of cubic Diophantine equations over a bounded domain. It also corrects earlier versions by withdrawing the stronger claim that this gave a reduction from unbounded theoremhood to one fixed bounded-domain cubic instance.
2025–2026
arXiv:2511.07774 [math.LO, cs.LO] arXiv
Gives a proof-theoretic account of the constructive classification of positive integers as 1, prime, or composite. It develops bounded decision procedures, a recursive sieve for the primes, modular cancellation, and finite arithmetic certificates, while separating what Heyting Arithmetic proves internally from what depends on the standard interpretation of the natural numbers.
2025–2026
arXiv:2512.08149 [math.LO] arXiv
The paper identifies a structural obstruction to uniformly separating two classes inside constructive arithmetic. The obstruction is not tied to what the classes mean; it appears whenever two evaluator predicates are maintained in parallel and inference is uniformly representable.
2025–2026
arXiv:2511.21296 [math.LO] arXiv
Small philosophical argument that physically meaningful propositions are constrained by what admissible measurement can actually extract: finite observational sequences, terminating procedures, or stable uniform conditions.
2025–2026
arXiv:2511.14665 [cs.CC] arXiv
Structural analysis of global decision problems over arithmetically represented domains. The paper studies how class-quantification transports impredicativity into formal problem spaces, relating diagonalization, reflection, and uniform complexity statements.
2025–2026
arXiv:2510.08934 [math.LO, cs.LO] arXiv
This paper studies a boundary between local self-application and global self-certification. Irrational quantities are treated operationally, as procedures whose approximations are refined by effective update rules. The golden ratio Φ is used as a model of stable local recurrence: the reciprocal update R(x)=1+1/x has a unique positive fixed point and admits finite witnessed approximations.
2026
Selfhosted .pdf
Presents a logical pipeline for EMNIST-style classification where preprocessing, prediction rules, training traces, and evaluator behavior are made replayable and checkable. Instead of treating training as an opaque optimization run, it uses integer-valued repair steps that expose decidable invariants and concrete counterexamples when something fails.