Nova-Violet Role is a non-profit organisation working at the intersection of cognitive science, law, and software — building frameworks that let people approach complex problems from more than one angle at a time.

🎯 Mission — Develop and share convergent cognitive frameworks that help individuals and organisations think in more dimensions than a single discipline allows.

🌟 Vision — A world where complex problems are met with holistic, multi-faceted thinking rather than one lens applied harder.

⚖️ Method — Reality is the judge. Every number in these repositories is meant to be re-run by you. If one of them is wrong, telling us is the most welcome contribution we accept, and there is an issue form for exactly that.

Nine ways of seeing the same problem, reasoning at once. Each is incomplete alone; the system is the overlap. They do not take turns, and they are not permitted to average themselves into consensus — where they disagree is the output, not a failure.

"Each one is a different way of seeing the same problem. Together, they see everything — and where they disagree is where the real answer lives."

The roster is not prose. It is declared once in a machine-readable contract and an executable checker holds every charter to it in both directions, so no lens can quietly acquire an extra facet in a document nobody re-reads.

What is pinned is never cut.

For any conversation, any policy — hence any summarizer, any keep ratio, any trigger — and any number of compression rounds, the pinned messages that come out are exactly the pinned messages that went in.

theorem pinned_never_cut (p : Policy) (c : Conv) :
    ((run p c).filter effectivePinned).map pinExtract
      = (c.filter effectivePinned).map pinExtract

Retention is not a request made of a model. Pinned messages are carried across the summary boundary structurally — the same way the system prefix is — and are never inside the replaced span. No threshold, no summarizer prompt, and no number of rounds can erode them.

It rests on two companions, and together the three are why context can be treated as effectively unbounded:

theorem run_shrinks   (p : Policy) (c : Conv) : countChars (run p c) ≤ countChars c
theorem run_fixpoint  (p : Policy) (c : Conv) : ∃ r, stepE p (run p c) = .error r

Shrinks — the result is never larger than the input. Converges — iteration strictly decreases and halts. Preserves — what you pinned is still there, unchanged. Compression that shrinks but loses what matters is worthless; compression that preserves but never converges is a hang. The theorem is the conjunction.

Proved in Lean 4, machine-checked, zero sorry — and mutation-tested, so we know which theorems constrain behaviour rather than merely being true.

A nine-lens cognitive Mixture-of-Experts router for Claude Code: ten routing lanes and a measured R/s+ divergence gauge, specified in Lean 4 and bound to the shipped hooks by an executable checker — so the specification cannot silently drift from the code it describes.

➜ RoT-MoE

A /goal engine where completion is earned, not announced. Acceptance criteria are real shell commands, the Stop hook re-runs every one of them, and only exit 0 ends the session. A model cannot talk its way to done.

➜ RoT-DTD-GOAL

Context compression as a transparent proxy: old messages compress while recent context stays verbatim, so a conversation never hits the wall. Ships with the Lean 4 formalisation above — proving the compression policy rather than asserting it — plus a port to the Mistral Vibe CLI with an eight-agent routed crew.

➜ claude-rolling-context-Lean-4-

DNSCrypt, DoH and ODoH client for Android — no-root ad blocking, encrypted DNS with a local CDN, a Rust engine, and Lean 4 proofs over the resolver invariants. Alpha pre-release.

➜ Yeah-Torta

Start here: Contributing · Code of Conduct · Security · Support · Governance

• Discussions — Q&A, Ideas and Show-and-tell on the active repositories
• Ko-fi — ko-fi.com/saimonokuma — buys time, never priority
• GitHub — our repositories are open and public

As a non-profit, Nova-Violet Role is committed to open knowledge and collaborative development — and to making that commitment binding rather than promised.

Our work is licensed AGPL-3.0-or-later OR EUPL-1.2. These are copyleft licences, chosen deliberately over permissive ones: what is shared here cannot be enclosed later, by anyone, including us. If this organisation ever goes quiet, the code, the proofs and the history remain yours to carry forward.