How the registry works underneath - request paths, the verification engine internals,
the tiered async pipeline, and the data model. Each diagram below is hand-drawn SVG;
click any box to jump to the file or endpoint that implements it.
1. Request flow
A user request lands on Fly.io's edge proxy, then on a single Flask process running in a
shared-cpu-1x 256 MB Docker container. The Flask app opens the
certified data/registry.db snapshot read-only and immutable. Page-view
statistics and feedback are the only mutable website state, kept separately on
the Fly volume at /persist/site.db.
Why SQLite? The certified corpus is read-heavy, compact, and
distributed as one validated file. The deployed app opens it with
mode=ro&immutable=1 and query_only=ON.
Offline release pipeline. Candidate data and verification runs
are generated outside the public web process, reviewed, and admitted only by
the correctness release gate.
Fly auto-stop lets the machine sleep when idle. The separate
/persist/site.db volume retains view totals and feedback; it never
changes the certified registry snapshot.
2. The verification engine, inside out
The boundary-circle verifier certifies whether
Re(z·f'(z)/f(z)) > 0 on the disk
|z| ≤ r. A positive scan is a finite-disk bound only after
zero-freeness and object identity are certified; it is not a whole-unit-disk
proof. A disproof requires a certified interior counterexample point.
Below is what happens when you call POST /api/v2/verify_sandbox with a
closed form.
Soundness contract
The verifier never says "proven" by sampling. Interval arithmetic can certify
a finite-disk bound only when the same object is checked and zero-freeness is
established on that disk. Negativity (hi<0) is sound
only because interval arithmetic guarantees the bound holds across the whole arc,
not just at a point.
Centered form vs naive
Naive Horner evaluates the polynomial with z as a single interval - each occurrence of
z gets enlarged independently, producing exponentially wide bounds on slowly-decaying
truncations. The centered form anchors at the arc midpoint (a thin interval) and bounds
only the variation across the arc by the derivative, scaling with arc width rather than
polynomial degree.
Why exact-form-first matters
A 20-term truncation of z/(1-z) = z+z²+z³+… has zeros near |z|=1 and
genuinely isn't starlike there - the polynomial is a different function than f.
When a SymPy closed form is available we verify the true f, not its truncation.
3. Offline release pipeline
Screening, interval verification, literature ingestion, and family additions
happen outside the public web process. Candidate records retain their evidence
scope: numerical screens, finite-disk bounds, whole-domain proofs, and certified
disproofs are not collapsed into one label.
1. Generate candidates. Researchers run the same verifier
components locally and preserve assumptions, parameters, witnesses, and
object identity with each result.
2. Review and validate. Evidence-policy checks reject unsupported
upgrades and conflicting certified conclusions. Database and artifact tests
run against the exact proposed snapshot.
3. Publish atomically. A successful correctness release binds the
database digest and code commit. Fly serves that snapshot read-only; runtime
requests cannot alter its mathematical contents.
4. Data model
The encyclopedia centers on function_families - the canonical mathematical
entities. Concrete points in parameter space become function_instances.
Statements about them become facts. Every verifier run leaves a record in
verification_runs. Papers cited in support attach via evidence.
No NULL-link tombstones: every paper claim's provenance is preserved.
immutable runs, fail-closed facts
Verification runs are appended, never deleted. Facts are recomputed from
registered routes, explicit scope, applicability, and object identity.
Conflicting certified conclusions clear the public result and enter review.
Fingerprint deduplication
Every instance has a SHA-256 fingerprint based on its rotation-normalized
coefficient sequence. Before inserting a new family, add_family
checks for fingerprint collisions and surfaces merge candidates.
Paper → evidence → fact
A paper claim (extracted by text mining) becomes a piece of evidence when
a human curator or an automated matcher links it to an existing fact.
This creates the cross-tab between literature and the encyclopedia.
We use first-party site metrics to improve navigation: page visits, internal clicks, search result counts (not search terms), and approximate active time. A random tab ID groups events for seven days; GPC/DNT turns this off. The separate visitor count uses a self-hosted pseudonymous fingerprint and also respects GPC/DNT.