Skip to content
View Fieldnote-Echo's full-sized avatar

Sponsors

@dleighsystem

Organizations

@Project-Navi

Block or report Fieldnote-Echo

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Content in all repositories owned by your account will be closed.
Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. Markdown is supported. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
Fieldnote-Echo/README.md

Hey, I'm Nelson.

OpenHands - Contributor Software Agent SDK - Contributor Mathlib - Contributor

I map failure patterns across complex systems and build the security boundaries required to stabilize them.

I'm the founder of Project Navi - an open-source AI security company focused on zero trust architecture and mathematical governance. Before that, I spent seven years in behavioral health research, coordinating peer-support programs across 500+ organizations and publishing on workforce collapse in the APA Psychiatric Rehabilitation Journal.

The same structural breakdowns I studied in human systems - drift under pressure, coherence loss at scale, collapse when governance is bolted on instead of built in - show up in AI deployments. So I started building infrastructure to prevent them.


What I'm Building

Takens' theorem for generic pairs, machine-checked. On a compact smooth d-manifold, the pairs (T, h) of a C² diffeomorphism and a C² observation whose delay map with 2d+1 coordinates is a C² embedding are open and dense in Diff²(M) × C²(M, ℝ). Also finite-regularity Sard (via a port of Moreira's theorem), exact finite-state horizons and ordinal codes. Lean 4 + Mathlib v4.34.1; no sorry, standard axioms only.

Box-counting dimension of the (u,v)-flowers, machine-checked. For 1 < u ≤ v, the Rozenfeld–Havlin–ben-Avraham flowers have dimension log(u+v)/log u: as the limit of their recurrences, as a log-ratio of the explicit graphs, and as a box-counting dimension over minimum box covers at every resolving scale. Lean 4 + Mathlib v4.34.1; no sorry, standard axioms only.

Existence theory for the Creative Determinant boundary value problem −ΔΦ = a|∇Φ| + bΦ − c(Φ₊)ᵖ. On finite weighted graphs, a positive solution is fully proved; the continuum results are conditional on explicit, documented elliptic hypotheses. Lean 4 + Mathlib v4.34.1; standard axioms only. Theory in the paper.

Deterministic input sanitization for untrusted text in LLM pipelines. Strips homoglyphs, invisible Unicode, null bytes, template injection, and path traversal vectors. Zero dependencies. Python 3.12+. Live on PyPI.

Agent Skills for coding agents: start and release Python packages, add or repair CI, harden the supply chain, keep docs accurate, review changes and verify findings, and calibrate measurements or refuse bad fits. Each skill is a standalone folder of instructions with checked examples, exercised by agents on throwaway projects.


Open Source Contributions

  • OpenHands: Disclosed a CVSS 9.1 security vulnerability; wrote and merged the fix into main. Contributed defense-in-depth SecurityAnalyzer ensemble.
  • Mathlib: Contributed SimpleGraph.ball (open metric ball).
  • NIST and NCCoE: Submitted responses on AI agent identity, authorization, and adversarial prompt detection (Zenodo).

Get In Touch


Machine cognition, human values.

The knowledge is free, the community is open. If you wish to support our mission, buy a t-shirt. 🐘

Pinned Loading

  1. Project-Navi/fd-formalization Project-Navi/fd-formalization Public

    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. …

    Lean 3

  2. Project-Navi/navi-sanitize Project-Navi/navi-sanitize Public

    Deterministic input sanitization for untrusted text — invisible characters, homoglyphs, and encoding tricks, handled before your code sees them. Zero dependencies, no ML. Python 3.12+.

    Python 3

  3. Project-Navi/takens-formalization Project-Navi/takens-formalization Public

    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. No sorry.

    Lean 3

  4. Project-Navi/cd-formalization Project-Navi/cd-formalization Public

    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, document…

    Lean 2

  5. Project-Navi/skills Project-Navi/skills Public

    Agent Skills for coding agents: start and release Python packages, add or repair CI, harden the supply chain, keep docs accurate, review changes and verify findings, and calibrate measurements or r…

    Python