[What follows might be AI Psychosis]
My friend and I have been working together on some ideas for 15 years. Over the last month, we went off on a tangent and entered something that feels like an infinite loop—likely caused by frontier AI, many tokens spent, and a hyper-focused state. What follows is an introduction to this loop, and a proposal for a challenge to see if someone can pull us out of it.
Genesis
Every act of representation is a translation. Every translation has a residue. The residue is not failure—it is what cannot be compressed further. And the residue has structure.
A simulation never recovers the world it models. The residue is what the model's state space cannot hold—degrees of freedom that exist in the original but have no slot in the representation. Knowledge transfer works the same way. When an expert teaches, the student receives something—but the expert had more. The gap is not random: two students from the same class can leave with the same gaps, because the gaps are determined by what the teaching structure could not say, not just by how attentively the students listened.
A categorization collapses continuous variation into discrete types. "Young," "middle-aged," "elderly"—the collapse is intentional, but the internal structure erased by the label is the residue. A fractal is the exception. The translation from whole to part recovers the whole exactly—residue zero. That is why fractals feel uncanny: they are the one case where nothing leaks. Everything else does.
This framing—the residue, the translation, the gap that has shape—started as fifteen years of conversations and attempts to build systems that could hold up by themselves. Vladimir and I talked about simulations, fractals, and knowledge transfer, knowing something connected them but lacking the language to fix it. The space between what we could see and what we could say was large. And it had shape.
The Missing Functor
This shape lacked a functor to translate our thoughts to reality. This AI fever dream led us to a seven-day explosion, where we used AI agents (and perhaps a bit too much neuro-stimulants) to translate those 15 years of conversation into a formal language we couldn't touch before. The result is DomainSpec.
The Vertical Slice
We have tried to formalize what we call the Strict Regime. In our view, software doesn't just "have bugs"; it "drifts" because the translation layers between human intent and machine execution are mismatched. We’ve built a vertical slice of a system that attempts to eliminate this drift:
- A 10-Layer Meta-Representation (L0–L7): A mapping from the "Real-world Domain" to "Emergent Semantic Coherence." It categorizes exactly where information "leaks" during the engineering process.
- The Lean 4 Proofs: We’ve started anchoring the structure of these layers in formal logic, using the compiler as the ultimate referee for our 15-year debate.
Theorems & Conjectures
The AI agents are suggesting we’ve stumbled onto something mathematically coherent, but we need to know if the logic holds outside the "fever dream." We are putting forward three primary claims:
- The Residue Theorem (T1): We model the software compilation process as a Functor (Δ). We define "residue" as the categorical failure of the unit of an adjunction to be an isomorphism.
- The Invariant Navigation Theorem (T2): A claim regarding the topological mapping between conceptual nodes and physical structures—asserting that the resolution of a representation remains invariant under recursion.
- The Convergence Conjecture (C1): We hypothesize that as the resolution of our L-layers increases, the "drift" between domain and implementation converges toward zero—the Fractal Limit.
The Challenge
The repository contains our philosophy, our 3D ontology visualizations, and these Lean 4 signatures.
However, we are being honest: many of the theorems end in sorry. To some, these are gaps; to us, they are invitations. We believe the symmetry of the system demands these proofs are true, but we are amateurs—not professional mathematicians. Your assistance in reviewing these structures would be invaluable, whether it is to help us bridge the final gaps or to show us where our premises fail.
If you are interested in seeing the Lean 4 that LLM agents built, comment on this post to receive access to the repo.
— Boscaro & Rondelli