How this site is put together, and why.
Every claim on kodamaseclabs.com is meant to be checkable, and this page is where we say plainly what's verified, what isn't yet, what we deliberately don't publish, and why. No quantum hype, no algorithm hype, no math hype — if something here turns out wrong, the fix is to correct it and say so, not to reword it into something unfalsifiable.
Pre-alpha software, and it is the instrument, not the work
What this site publishes is the output of a piece of software, not the software. The tooling itself is not published and we say below why not — but refusing to name it, which this page did until 7 August 2026, was a step too far: it left the results looking as if they came from nowhere, and "an internal tool" is not something a reader can weigh. So, plainly. TRINITY is not one model. It is a family of them, and the one behind everything published on this site is the generic test model, build test_min_max_0 — the general-purpose one, the one used to find out what the approach can and cannot do. Other lines exist and are in development; they are not named here, because none of them has produced anything published yet and naming a model before it has output is exactly the kind of claim this site is built to avoid. When one does, it will appear here with its results, not before.
As for the stage that generic model is at: this page called it alpha until 7 August 2026. It is not alpha. Alpha implies the parts light up, and ours do not all light up: one of the engines the system loads fails on every single run (a library it needs is not available in the measurement environment), and one module — the Tian–Yuan–Zhang corollary — contradicts OEIS on n = 210 and carries “DO NOT USE YET” in its own docstring, written by us, on purpose. The right word for a build that runs, produces results, and has engines that never ignited is pre-alpha, and that is what this is. It is nowhere near a general-purpose computer algebra system — nothing here approaches the breadth of an established CAS like Maple or Mathematica, thousands of built-in functions refined across essentially every branch of mathematics over decades. What we have is narrower and rougher: closer to a single, carefully-ground lens than a full optical bench. A lens like that isn't something you hand to just anyone and expect a clear image from — getting it in focus takes a deliberate process, and it's easy to knock it far enough out of alignment that it stops being useful at all. That's the state of what's behind this site: real, but still being calibrated, not a finished instrument.
Most of the actual day-to-day work isn't clean derivation. It's collecting a large volume of attempts that turn out to be conceptually wrong, and then finding that some of them are still related to each other — by an actual axiom sometimes, by a person just noticing a pattern a mechanical check wouldn't catch other times. Each of those gets classified, but classified as unvalidated: zero weight in our own internal accounting until something stronger says otherwise. Doing that for long enough produces a large, structured body of raw material that reads a lot like an ARC-AGI-style puzzle — individually senseless-looking pieces that a person can still put in order and give a category to, the same way people (not yet machines, reliably) are good at finding structure in problems that don't come with rules attached. What actually promotes a piece of that out of "zero weight" hasn't changed from the rest of this page: Lean 4 checking it, or an equivalent proof-assistant / independent-method check — not how interesting it looked the moment someone first noticed it.
Not everything real is verified the same way — we don't blur that
Lean-checked
Compiled and checked by the Lean 4 theorem prover (v4.32.0) against a pinned Mathlib revision, no sorry. A machine verified every logical step. This is the strongest claim we make, and we only use the badge where it's literally true — see the The Notebook's log for the specific results that qualify today.
Tested against independent reference
The three free tools aren't formally proven, but every one of them is cross-checked against an independently written reference calculation before shipping — not just "it looked right once." The exact counts (2998 integers, 41/41 Collatz steps, etc.) are shown right there, not just claimed here.
Measured on real hardware
The quantum results (GHZ, cluster states) are experimental measurements on a real IBM Quantum backend, not simulations. The Notebook shows the literal job IDs, not a description of what supposedly happened.
Not yet peer-reviewed
This is our own in-progress research, presented as-is. It may contain errors and is subject to revision. We say this explicitly rather than let a confident tone imply a certification that doesn't exist yet.
A mismatch is data, not a failure
The cross-checking above isn't "run it twice and hope." When two independent methods disagree, that disagreement is the most useful signal either one produces — it's the point where an actual person looks, and where an actual bug gets found. Below is that loop, plainly: not implying a system that corrects itself, because there isn't one — a person reads the discrepancy every time. The same three letters run through everything here: V for a claim that held on what was tried, X for one refuted by a counterexample, P for one proved, which only Lean’s kernel awards. The findings registry on /challenges uses them, and so does the mascot’s notebook, which can hand out the first two and never the third.
The loop above, with numbers in it. Method A: the determinant of the n×n Redheffer matrix (entry 1 when j = 1 or i divides j), computed exactly in BigInt by Bareiss elimination. Method B: the Mertens function M(n) = Σμ(k) from a linear sieve. They share no code; Redheffer (1977) proved they are equal, so every dot must land on the staircase. The button rewrites the sieve with the mistake a first sieve usually has — μ of a number with a squared prime factor taken as ±1 instead of 0 — and the comparison reports the first n where the two disagree. That number is the whole value of the loop: not "it disagreed" but where, which is where a person looks. (The identity itself is the one we formalised in Lean 4 and submitted to Mathlib.)
Why we'd rather find the error than avoid finding it
A disagreement between two independent methods is the highest-value moment in this whole process — the one point where being wrong is cheap to catch and expensive to miss. Treating it that way means slower short-term progress (a clean run that turns out to hide a bug isn't actually progress) in exchange for results that hold up when someone else checks them. That's the trade this lab makes on purpose: study the discrepancy, find the actual cause, fix it, re-run, and only then move on — not paper over it and keep going. The willingness to be shown wrong, repeatedly, and to treat each instance as useful rather than embarrassing, is most of what "methodology" means on this page.
What we actually do, and what we don't claim
Nothing runs from a CDN
Every script and stylesheet this site loads — including KaTeX and Paper.js — is vendored and served from our own origin. The Content-Security-Policy is script-src 'self' with a per-request nonce and no 'unsafe-inline' or 'unsafe-eval': no third party is in a position to inject or swap code at runtime, even if one of those upstream projects were compromised. style-src does allow 'unsafe-inline', needed for KaTeX's own generated positioning — a materially lower-severity exception, since it permits styling, not code execution.
Real HTTP hardening, not a checklist
HSTS with preload, a nonce-based CSP (no unsafe-inline), COOP/CORP isolation, a locked-down Permissions-Policy, and cache-busted assets keyed to file modification times so a deploy can't leave a stale script cached in a visitor's browser. All of it lives in one security.php, included at the top of every page — not scattered, not skippable.
Exact arithmetic, not floating-point cryptography
The RSA walkthrough and Miller–Rabin tool use JavaScript BigInt throughout — no float ever touches a modular-exponentiation or primality step, the same "never floats, only exact integers" discipline the internal research tooling runs on. That's a correctness property, not a secrecy one: these are educational demos with no secret key to protect, by design.
If a CVE lands in something we ship or depend on
Because every third-party file here is vendored, not fetched live, a disclosed vulnerability in KaTeX, Paper.js, or anything else we use doesn't auto-propagate to visitors the moment it's published — but it also doesn't auto-patch itself. We watch upstream advisories for what we vendor, and when one applies here we re-vendor the fixed version and redeploy, the same way we'd fix a bug in our own code. We don't claim immunity to vulnerabilities in code we didn't write; we claim control over exactly when and how it changes on this site.
For context: how a real encrypted messenger is built
This site is a research and tools showcase, not a messaging app — so this isn't a like-for-like comparison, and we don't claim to match or exceed a product like Threema. Worth understanding anyway, as a well-documented example of the field: Threema's end-to-end encryption runs on NaCl/libsodium — Curve25519 for key exchange, XSalsa20 for symmetric encryption, Poly1305 for message authentication, SHA-256 for key fingerprints, a second transport-layer encryption hop to hide header metadata, and per-session forward secrecy (their Ibex protocol) so a compromised key can't retroactively expose past messages. Those are audited, widely deployed primitives, maintained by cryptography specialists over many years — which is exactly why, on a site with no secret message content to protect, the right move is to learn from that bar rather than hand-roll our own primitives just to have something to point at.
This site's own cryptographic bill of materials (CBOM)
The first thing a real PQC-migration audit asks for — every cryptographic primitive in use, where, and whether it's quantum-vulnerable — applied here to ourselves rather than described in the abstract. Short list, because this is a static/edge-rendered site with no user accounts and nothing to keep secret past its own uptime, not because the inventory was trimmed to look better.
| Component | Algorithm | Quantum-vulnerable? | Where |
|---|---|---|---|
| RSA key-generation walkthrough | Textbook RSA, exact BigInt | Yes (Shor) — by design, it's the demo of exactly that | The Notebook |
| Subresource Integrity | SHA-384 | No (hash, not key exchange) | every CSS/JS asset tag |
| Deploy integrity manifest | SHA-256 | No | the deploy script |
| Transport encryption | TLS 1.3, edge-terminated | Depends on Cloudflare's negotiated key exchange, outside this repo's control | every request to this domain |
| Post-quantum (ML-KEM/ML-DSA/SLH-DSA) | Not deployed | N/A | nowhere — there is nothing here that needs it yet |
Combinatorial optimization — not yet a published result
We're exploring NP-hard combinatorial optimization (vehicle routing, TSP-class problems) with the same exact-arithmetic tooling behind everything else on this site. There is no benchmark, no working solver, and no product to point to yet, so we're not going to describe one here as if there were. When we do validate against standard reference instances, the results will go on this page held to the same standard as everything else — the actual instance IDs, the actual numbers, checked against a known-good reference, not a description of what it's expected to do.
The standard benchmark sets we'd validate against, for anyone who wants to follow along or hold us to it: VRPLIB (Solomon, Homberger and Uchoa instances with best-known solutions) and TSPLIB for routing and the travelling-salesperson problem; the UCI Machine Learning Repository for broader structured-data work, an academic archive with provenance on every dataset rather than a mixed public upload site; and NIST's random number generation project for randomness and cryptographic robustness testing.
This site itself is part of that same habit of learning in the open: the math visualizations you see across it are built by evaluating real, self-hosted open-source libraries (KaTeX for typesetting, Paper.js for vector art, with more under evaluation) rather than reinventing them badly.
Results are public. The pipeline that produces them isn't, yet
Every calculation on this site — The Notebook, the free tools, the RSA demo — runs on tooling we built in-house for this work, not a third-party library doing the mathematics for us. We don't name that internal tooling or publish its source here: the underlying research programme is still active and some of it is genuinely unfinished. What we do publish is the results themselves, in a form anyone can check independently — formulas, job IDs, step-by-step traces — without needing access to anything confidential. If a result can't be shown this way without exposing the pipeline, we leave it out rather than publish a claim nobody can verify.
Real hardware, real numbers — not a claim to take on faith
We know how this reads from the outside: an independent lab, no big-name backing, publishing results that sound significant. So here's what's actually behind it, in plain computer-science terms rather than a spec sheet — ordinary hardware, used carefully, not a data centre.
Compute
Ordinary consumer-grade hardware run continuously, plus free-tier cloud notebooks for the heavier jobs — no research cluster. Cloudflare's edge network handles request-level security and caching (the Worker and CDN behind this site), and IBM Quantum provides access to real superconducting hardware for the quantum results elsewhere on this site — not a simulator standing in for one.
Microcontrollers, as a matter of curiosity
Away from the software, a genuine hobby: microcontroller boards (Arduino, ESP32) and off-the-shelf modules sold openly by any electronics supplier, wired up and programmed to see how everyday hardware actually works. Same rule as the rest of this page — real, owned hardware, named plainly, not implied capability. It is curiosity, nothing more, and all of it is our own equipment on our own bench, kept entirely within the law.
How a result gets validated
The same discipline everywhere: exact arithmetic only (BigInt / Python Fraction, never floating point for a result that has to be exactly right), and wherever two independent methods can reach the same answer, both get computed and compared before anything is called correct — the Redheffer chart on The Notebook is a live example: a matrix determinant and an independent Möbius sieve, checked against each other, not assumed to agree.
What's actually been checked, in numbers
132 individual research findings tracked in the internal record, 26 of them compiled and checked by the Lean 4 theorem prover against Mathlib — a machine proof, not a manual claim — across 15 separate Lean source files. The site-wide automated test suite: 26 findings closed by Lean 4’s kernel, with the axioms named wherever a compiler stands in for it (see the verification seal in the footer).
Why publish this at all
Because the alternative — "trust us" — isn't worth much from an independent lab nobody's heard of. Every number on this page is something you could ask us to reproduce, and several results elsewhere on this site (the Redheffer chart, the RSA walkthrough, the Miller–Rabin visualizer) run the actual computation live in your browser as you read them, not a screenshot of one that ran somewhere else once.
Try it on this exact sentence
⊢ marks below are live, not screenshots — click one and it re-runs that exact computation in your own browser, right now, and shows you what came back.
97 is prime — Miller–Rabin, deterministic witness set for this range.
What you've verified this visit
Starts empty on purpose — nothing is pre-filled. Click the ⊢ mark above (and the others on the homepage and in The Notebook's Redheffer entry — each keeps its own page's ledger) and it lands here, newest first.
Headroom, if a problem needs it
The everyday hardware above is what runs the site and most of the research; it isn't a hard ceiling. Cloudflare's own paid Workers tiers and IBM Cloud's on-demand compute instances scale well past it when a specific problem calls for more, and IBM Quantum's pay-as-you-go plans provide additional QPU time beyond what's freely available, on the same real superconducting hardware — not a different, lesser system. We size compute to the problem rather than running everything at maximum by default, and say so here instead of implying a permanent supercomputer that isn't actually there.
What's actually on each page
403.