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 reads from a single
SQLite file mounted at data/registry.db. There's no separate database
server. A background verification worker thread drains the
verification_queue table forever, upgrading fact confidence asynchronously.
Why SQLite? The registry is read-heavy and writes are bounded by
verification throughput (≪1 write/second). One file, no separate DB process.
Backups are cp registry.db registry.db.bak.<date>.
The worker thread starts on Flask boot (start_background_worker()
in verification_worker.py). It polls verification_queue every
2 s, claims the highest-priority pending row with BEGIN IMMEDIATE, runs
the tier, and writes back.
Fly auto-stop means the machine sleeps when idle and wakes on incoming
request (cold start ~1 s). Background worker resumes on wake; jobs that were
running at sleep get re-claimed.
2. The verification engine, inside out
The boundary-circle verifier certifies whether
Re(z·f'(z)/f(z)) > 0 on the disk
|z| ≤ r. It's sound in both directions: a proven verdict really proves
the property; a disproven verdict comes with a certified 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 - only when interval arithmetic certifies
lo(Re g) > 0 on every arc. Sample-based 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. Tiered async pipeline
When you submit a function via the admin form, three verifier tiers run - Tier 1
synchronously so you get an immediate verdict, Tiers 2 and 3 in the background.
A fact's confidence is monotonically upgraded as higher tiers complete:
numerical_strong → rigorous_verified → proven.
A higher-tier disprove is terminal - a sound counterexample always
supersedes a numerical pass.
Tier 1 / screen
Sampled grid on 80×40 points. Float arithmetic. Returns numerical_strong
or numerical_weak. Fast (<20 ms) but never authoritative - clearly
labeled as screening, not proof.
Tier 2 / rigorous polynomial
Centered-form interval arithmetic on the 20-term Taylor truncation, with
argument-principle zero check. Returns rigorous_verified on the truncation
object, NOT necessarily the original f.
Tier 3 / rigorous exact
Same engine, but on the symbolically-derived g(z) = z·f'/f from the closed form.
Returns proven - the strongest level, because it operates on the actual
function rather than a truncation.
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, monotonic facts
Verification runs are appended, never deleted. A fact's confidence increases
monotonically (numerical → rigorous → proven) as higher tiers complete.
A higher-tier disprove is terminal, overriding any prior proven status.
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.