Project Navi
Research software for measurement, security, and formal verification. Zero-dependency libraries with audit-grade quality gates.
Research software for measurement, security, and formal verification. Zero-dependency libraries with audit-grade quality gates.
A field theory of coherence: autopoietic closure as a nonlinear elliptic boundary value problem on a compact Riemannian manifold, with existence conditions, spectral viability thresholds and explicit falsifiability criteria.
Deterministic sanitization of untrusted text: invisible characters, homoglyphs and encoding tricks handled before your code sees them, with legitimate Unicode preserved. Zero dependencies, no ML.
Lean 4 + Mathlib existence theory for the Creative Determinant boundary value problem. Positive solutions fully proved on finite weighted graphs; continuum results conditional on explicit, documented elliptic hypotheses.
Lean 4 + Mathlib proof that the (u,v)-flowers have dimension log(u+v)/log u: as a recurrence limit, as a log-ratio of the explicit graphs, and as a box-counting dimension at every resolving scale. No sorry.
Lean 4 + Mathlib proof of Takens' theorem for generic pairs: C² delay embeddings with 2d+1 coordinates are open and dense in Diff²(M) × C²(M, ℝ). Also finite-regularity Sard and exact finite-state horizons. No sorry.