Navigation:
Preliminary overview of papers, preprints, and working drafts in constructive logic, computability, and formal problem spaces.
Listed from most recent arXiv revision.
2026
arXiv:2605.18924 [math.LO] arXiv
Stands out as the most substantial contribution. 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
Stands out as the second most substantial contribution. 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] arXiv
Argues that, in constructive arithmetic, there is no single total procedure that can uniformly turn proofs of primality-style statements into explicit witness-producing proofs. It approaches this from three angles: a geometric picture of prime versus composite configurations, a proof-theoretic obstruction to uniform witness extraction, and a recursion-theoretic link to the absence of total Skolem functions. The final section interprets the result as an informational boundary around what constructive proofs of primality can uniformly reveal.
Remark. Under a substantial revision process.
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. The result is framed as stricter than classical barriers such as relativization, natural proofs, or algebrization, because it blocks the logical form of uniform separation itself rather than a specific proof method.
2025–2026
arXiv:2511.21296 [math.LO] arXiv
Philosophical. Small argument that physically meaningful propositions are constrained by what admissible measurement can actually extract: finite observational sequences, terminating procedures, or stable uniform conditions. It identifies the resulting constructive fragment with simple existential claims and stable universal-existential claims, then proves an operational incompleteness result: some true claims about admissible extraction cannot be decided by any sound recursively axiomatized spacetime theory.
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] arXiv
Philosophical. Proposes a geometric interpretation of constructive proof steps using Fibonacci-style additive recurrence. Its main claim is that modus ponens can be represented as a bounded constraint-satisfaction process: each inference step becomes a checkable geometric condition under golden-ratio scaling. It frames this as a bridge between additive combinatorics, proof theory, and symbolic computation.
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. The project’s main point is not that the classifier is more powerful than a perceptron-style model, but that learned evaluators can be accepted only through an explicit certification gate comparing the specialized evaluator against the reference one under fixed conditions.