No-Go-as-a-Service
Book 6's job, per its own charter, is finding uses and turning ideas into products. The Cosmic No-Go chapter (Ch DE-1) proves something with a genuinely portable shape: given a system's transverse stability rate, a locked identity (c = H′) forces a hard exclusion on what the system's expansion behavior can do. That shape — feed in a measured rate, get back a hard yes/no on what's excluded — is exactly the shape of a useful API call. This working paper is both the product spec and a working prototype of it.
What actually ships
Four endpoints, each a thin numeric wrapper around a specific theorem in
HelixToyModel.lean, not a black box:
| Route | Backing theorem | Returns |
|---|---|---|
/trichotomy?z= | neutral_line_trichotomy — fully proved, no sorry | repelling / neutral / attracting classification |
/epsilon?eps0=&z0=&t= | epsSol — closed form (issue #H1) | the transverse deviation ε(t) |
/lyapunov?eps0=&z0=&t= | lyapunov_exponent_eq — issue #H2 | numerical Lyapunov rate, converging to −2 |
/nogo?limit= | nogo_attractor_not_deSitter + attractor_excludes_deSitter — issue #H3/#H3b | whether a claimed transverse-rate limit excludes any positive finite (de Sitter) expansion rate |
One real bug was caught and fixed in building this: the naive
implementation of /lyapunov computed ε(t) directly and then
took its log, which underflows to exactly 0.0 in floating
point once t is more than a few hundred, throwing a
math domain error on log(0). The fix computes
log|ε(t)/ε0| directly from the closed-form exponent
(−2t + 2e−z0(1−e−t))
instead of exponentiating and then re-taking the log — the kind of
numerical-stability bug that only shows up when a proof gets turned into
running code, not when it stays a theorem statement.
The product angle
Fit with existing distribution: the membership tiers already on Gumroad ($25–$250/year, per-repo access) are built for humans reading chapters. An API is a different buyer — a script, not a person — and the natural model is metered or flat-fee API-key access layered on top of the existing tiers, not a replacement for them. No pricing number is committed here; that is a decision for after the prototype has real callers, not before.
What this chapter does not claim
The underlying Lean file still carries three tracked sorries (#H1, #H2,
#H3/#H3b) — the closed-form ODE check, the Lyapunov limit, and the
no-go integral are stated precisely but not machine-verified in Lean
yet, only numerically verified in Python above and derived on paper in
helix_toy_model.tex. The API is honest about this: every
response names the theorem it implements, sorry-status included, so a
caller can tell the difference between "kernel-checked" and "numerically
checked, paper-derived" without reading the Lean source. Selling access
to a numerically-verified-but-not-yet-kernel-checked result is fine as
long as it is labeled as such, which is why every JSON response carries
its own theorem citation rather than a bare number.
| Component | Status | Notes |
|---|---|---|
| 4 endpoints, running prototype | built + tested | Flask, tested via test client; see AXLE/nogo-api/ |
| Numerical stability (large-t underflow) | fixed | Caught this session; see bug note above |
| Underlying Lean proofs | partial | Trichotomy proved; #H1/#H2/#H3/#H3b remain sorry |
| Auth, rate limiting, deployment | not started | Prototype 0.1 is local-only, no production hardening |
| Pricing model | deliberately undecided | Metered API-key layer proposed; no number committed |