AI produces mathematical claims faster than anyone can read them. This machine does both ends of the job with the same exact arithmetic. It has settled a value conjectured open since 2019, certified what is — to our knowledge — the first hot-spots domain beyond every class analysts have reached, and refuted a published constant at its twelfth digit. Every verdict is a re-runnable certificate: proved, disproved, or honestly refused — never a probability argument.
No probability arguments and no digit-matching. A claim is admitted only by exact arithmetic on whole numbers, and an instrument that cannot decide refuses instead of guessing. When a page here says REFUTED, that is a proof, and the falsifying witness is printed beside it.
The domain is deliberately inconvenient: a convex trapezoid with side slopes 6 and 18/5, no symmetry axis, nothing any existing proof technique can grab. The machine proves its second Neumann eigenvalue is simple by certifying a spectral gap — upper bounds from an interval Galerkin method, lower bounds from exact-rational finite elements with eigenvalue counts by interval inertia. It then builds a trial function that solves the eigenvalue equation EXACTLY — a sum of Bessel fans anchored at the four corners — and certifies that its boundary defect is a hundred-thousandth, which pins the true eigenfunction within an explicit distance of the trial.
Then the geography: every interior point is assigned, in exact rational arithmetic, to a deep core, a boundary collar, or a corner sector — and each region is killed by its own argument. Core and collar cells die by comparison against certified interior witnesses; the corner sectors die by certified series expansions, where the delicate corner needs a Bessel ladder identity to tame a divergent second derivative whose singular part arrives, provably, with the helpful sign. Zero cells survive. The extremes are on the boundary, the hottest point is vertex A and nowhere else, and the whole chain — eight records, every red control firing — re-runs from one command in about two minutes. The full account:
Erdős problem #852 has a constant attached to it. In 2026 a value for that constant appeared, produced with frontier-model help and quoted to 13 decimal places. This machine enclosed the same constant in exact arithmetic. The two agree for a while and then they do not.
published 0.0752403861777
certified 0.0752403861783092455893…
↑ wrong from here
The interesting part is which wrong digits. The obvious way to compute this constant is a loop: take a few million prime numbers, turn each into a factor slightly larger than one, and multiply them together in ordinary floating point. Past a certain size those factors are so close to one that rounding makes them exactly one, and they stop contributing anything at all. The running product goes still. Going still is what convergence looks like, so the loop appears to have settled, and it prints.
The published constant is what that loop prints, digit for digit. It was not approximately right with unlucky endings. It was the bug.
That is why one wrong constant is worth a whole page. Every ordinary defence fails against this. Rerunning it reproduces the same wrong digits, because two independent floating-point implementations agree with each other rather than with the truth. Spending more compute changes nothing, because the loop is already ignoring almost every factor you would be adding. Checking the digits against a reference value fails whenever the reference came out of the same kind of pipeline — which is how a bad number gets into an answer key and stays there.
What settles it is arithmetic that never rounds. The refutation here is a strict inequality between two whole numbers, with a denominator millions of digits long and no approximation anywhere in it. The corrected value is trapped between two exact fractions that agree for 15 decimal places, so the true constant cannot be anywhere near the published one.
The correction has been public in the problem’s own thread on erdosproblems.com since 27 August 2026. The full audit → — the refutation as integers, the certified correction, and a catalogue of the other ways a mathematical answer key goes wrong without anyone noticing.
All 42 reports → — the AI-verification shelf, the Erdős problems, the applied fronts in aerospace and energy, and the classical ground the instruments were proven on first. Every number on every page is recomputed from the certificates and records at build time, and a build that drifts refuses to ship.
Everything here rests on a single rule, and most of the engineering is the cost of keeping it.
The control page carries the full drawing, live: every family, every instrument, every battery executed at its build (never remembered), the full ledger decomposition, drift status.
A real, hash-pinned day of New York helicopter traffic — 82 aircraft, 382 flights — replayed on a map. Every trail is coloured by a verdict rather than by telemetry: each flight is re-flown on paper by an electric aircraft, using that manufacturer’s own published numbers, under the FAA’s energy-reserve rule, and decided.
Beta’s ALIA can certifiably cover 100 of the 382 flights and needs exactly 10 aircraft to do it — the lower half proved by pigeonhole, the upper half by an actual schedule. Joby, Archer and Eve publish too little to certify a single fleet, and the app says NEEDS DATA rather than guessing, with the exact number that would flip it printed beside the verdict.
Open SkyAudit → — the replay, the certificate panel, the fleet frontier and the what-if sliders, live. Data © adsb.lol (ODbL). Also live: the São Paulo pack — the world’s busiest urban helicopter market, decided under Brazil’s own reserve rule.
The instrument that audits a published claim also grades a model’s output, and that is turning out to be the more useful job. A model proposes an exact object; the grader re-derives it from whole numbers and answers CERTIFIED or REFUTED. There is no judge model, no rubric, and no stored answer key — so there is nothing to leak into a training set and nothing to game. The gap between “graded correct” and “is correct” that a policy would learn to exploit does not exist, because the grade is the proof.
That is measured, not asserted. Every campaign opens with deliberate forgeries — including one wrong by a billionth, invisible to any floating-point check — and if a single forgery grades as correct the run aborts before it touches real work. Across every real-model campaign so far, 364 proposals, nothing false has ever been graded correct and no certified row has ever turned out to be wrong.
The honest limit: this works for claims that come down to finitely many exact arithmetic facts — exhibit a witness, verify an identity, bound a quantity. It does not work for mathematics at large, and nothing here pretends otherwise. Inside that boundary the same grader can sit unchanged inside a training loop, with the verifier strictly stronger than the thing it is grading.
The oracle, packaged → — one curl, no dependencies, running on your laptop in under a minute: the claim schema, the tool definition a model calls mid-generation, the paste box, the paper draft, the ledgers.
Every headline claim detaches into a certificate — a JSON file of exact numbers — plus a verifier in plain Python: standard library only, nothing to install, zero code shared with the engine. Each verifier re-derives the mathematics from the certificate alone, re-hashes the pinned sources, must refute a deliberately forged value before it will exit green, and prints the sha256 of the certificate it checked.
python3 verify/verify_erdos852.py certs/erdos852-certificate.json python3 verify/verify_keller.py certs/keller-certificate.json python3 verify/verify_strassen.py certs/strassen-certificate.json
Run from a clone of the repository (add --sources corpus/sources to re-hash the pinned source bytes too), or download the certificate and verifier right here — the proof travels without the machine.
| certificate | what it holds | re-verify |
|---|---|---|
| erdos852-certificate.json | Both Erdős #852 constants as exact data: the c0 window re-decidable at 130 digits, the C∗ refutation as strict integer inequalities with no tail bound. | verify_erdos852.py |
| erdos852-h-records.json | Every record run of pairwise-distinct consecutive prime gaps the scan has closed — index, opening prime and length. The head reproduces OEIS A078515/A079889 term for term; the tail passes them. Each record beyond the published terms is re-proved at build by an independent Miller–Rabin verifier. | battery-gated |
| ai-claims-summary.json | The six-lane AI-claim audit as the build recorded it: every lane’s verdict, scope, check count and mutation-control count, written by the report builder from a live run of all six verifiers. Not a certificate — a record of what the verifiers said, so the shelf card and the page cannot quote different numbers. | battery-gated |
| keller-certificate.json | The Jacobian/Hessian counterexample corpus — every polynomial as explicit exact rational monomials; determinants and collisions re-derivable from the file alone. | verify_keller.py |
| strassen-certificate.json | 10 fast matrix-multiplication algorithms as exact tensor identities over Q and F2 — including AlphaTensor’s rank-47, decided both ways. | verify_strassen.py |
| bilinear-certificate.json | 9 bilinear algorithms for POLYNOMIAL multiplication over F2 — full, truncated and cyclic products — each found by the generation front’s free flip-graph walk and decided by instruments/bilinear, which rebuilds the target tensor from its name rather than trusting the scheme handed to it. Every entry stores its scheme in full, so any reader can re-decide it; the published bounds each one is measured against live in corpus/bilinear-bounds.json and are not results of this repository. | battery-gated the report |
| lambda4-audit.json | The adversarial audit of the lambda(4) proof: an independent clause walk sharing no code with the engine — inner products by direct trigonometric summation, family and subfamily membership by plain integer arithmetic, thresholds read from the campaign record, finite-clause sets re-certified fresh by the calibrated instrument. Every gcd-reduced 4-set in the box must be reached by an explicit clause of the proof (generic, family dot, closure, finite, delegated, or the definitional witness); a set with no clause is a hole and aborts. Also carries the full theorem sweep of the box: zero refuters. | battery-gated |
| lambda4-campaign.json | The lambda(4) campaign record. Phase 0: Mercer's Section-5 strategy (INTEGERS 19 (2019) #A4) executed mechanically — lambda(2) and the whole lambda(3) proof re-derived with exception families discovered and thresholds derived, not transcribed; the lambda(4) generic case with its 14 exception conditions discovered and matched against the paper's hand-written list; the measured reduction: five of the fourteen carry strictly negative delta, so NINE families remain. Phase 1, in progress: each family closed so far carries its full derivation here — second-level dot theorem, subfamily cones, derived thresholds, decided finite parts. d = 2c is CLOSED. Re-derived symbolically at every build by the lambda4 battery; finite parts pinned here and sampled at every run. | battery-gated |
| sublevel-tao179.json | The Tao #179 sublevel campaign (Erdős #1038, supremum side): rational-weight discrete measures on [-1,1] are monic root-constrained polynomials via |q| < 1, and this record holds certified sublevel measures — the 2√2 witness, grid champions including the interior cubic champion near 2.7542 and the quintic transition peak near 2.8011 — plus per-degree branch-and-bound THEOREMS: odd degrees strictly below 2.82 < 2√2, even degrees localized to [2√2, 2.82845] with (x²−1)^{N/2} attaining the left end. Every measure an outward enclosure from BigInt Sturm isolation; the box bound calibrated to equal the measure on thin boxes. | battery-gated |
| mercer-mu5.json | The mu(5) ladder, mu(5) ≤ 1 + π/m rung by rung to m = 20 — every exceptional tuple closed by one exact rational evaluation. | battery-gated |
| mu-table.json | The Newman min-modulus table: every set in the named boxes exhausted, champions certified, orbits classified, conservation per row. | battery-gated |
| mu-table-40.json | The wider-box extension of the mu table — billions of sets exhausted, the narrow-box crowding artifacts corrected. | battery-gated |
| lambda-table.json | The lambda table: the source lab’s rows reproduced exactly, plus rows that lab’s record does not hold and no table this lab has read holds — a claim about the certificates, not about priority. | battery-gated |
| census-high-periods.json | The Hénon high-period census, p = 13..16: every period point of the classical map found and counted exactly, the plane exhausted box by box, each row re-checked with zero unmatched — the proving ground the interval instruments were calibrated on. | battery-gated |
| entropy-henon.json | The certified entropy lower bound for the classical Hénon map: h-sets, covering relations, and the exact spectral argument. | battery-gated |
| erdos290-tail-ext.json | The Erdős #290 sweep extension: degrees closed beyond the cited page, the constant’s enclosure tightened degree by degree. | battery-gated |
| mfg2p-regime-map.json | The TWO-population regime map: every cell of the coupling plane with its verdict and its exact witness — the symmetric cross-coupling s against the attack-defense asymmetry d, two disjoint enclosures where uniqueness provably fails, the Lasry-Lions monotone strip where it does not, and the refusal reason everywhere else. There is no single-file certifier for this map: it is decided by labs/mfg2p/box2p.js and re-gated by that lab’s battery at every build of its report. | battery-gated the report |
| mfg-regime-map.json | The mean-field-game regime map: every cell of the coupling–potential plane with its verdict and its exact witness — two disjoint enclosures where uniqueness provably fails, the monotone enclosure where it does not, and the refusal reason everywhere else. | mfg-certify.js |
| matmul-eval-ledger.jsonl | The matmul eval’s append-only ledger — every campaign row, every verdict, every tag; the leaderboard is built from this file. | battery-gated |
| chowla-records.json | Certified Chowla merits c(A) = -min_x sum cos(ax) / sqrt|A|, one row per set size n, each an exact UPPER bound proved by instruments/trigmin for the set stored beside it. THIS FILE MAKES NO CLAIM ABOUT CHOWLA’S COSINE PROBLEM. Chowla’s question is asymptotic — whether c can be driven to 0 as n grows — and a low c at one n is a fact about that n. The measured trend here RISES with n (0.6558 at n=10 to 0.8205 at n=30), which is consistent with Chowla’s conjecture that the order is sharp, i.e. evidence against the direction, not for it. Explicit sets with small c are occupied literature (Mercer, INTEGERS 2019; Bedert, arXiv:2509.05260); these rows beat only the classical families recomputed here beside them. | battery-gated |
| matmul-eval-corrections.json | Corrections to rows already written in the matmul eval ledger. The ledger is append-only and is never rewritten, so a row that turns out to be MISLABELLED is corrected here and the correction is applied when the report displays it — currently one: 90 rows tagged v4-effort-low ran at the API’s DEFAULT effort, because the harness dropped its --effort argument in campaign mode. A correction naming a tag no row carries, or claiming a row count the ledger does not hold, refuses the report build. | battery-gated |
| matmul-loop-ledger.jsonl | The verifier-in-the-loop ledger — every trajectory round with its verdict and the exact feedback sent; the loop report is built from this file. | battery-gated |
| skyaudit-forecast-ledger.jsonl | The prediction ledger — interval FORECASTS committed before their target day (sha-pinned, append-only) and scored after in exact rationals; coverage claims are conformal counting theorems, never model faith. Wrong forecasts stay forever. | battery-gated |
| forecast-gym-ledger.jsonl | The Forecast Gym’s append-only ledger — every proposer’s forecast sha-committed before its outcome exists, every score an exact Winkler rational; the gym report and its admission board are built from this file. | battery-gated |
| lambda56-campaign.json | The lambda(5)/lambda(6) campaign record (Chowla’s cosine dip, the non-monotonicity program): lambda(5) = −L(1,2,4,5,6) closed in full — the generic case certified, all eight exception families closed with derived thresholds, 1725 finite sets decided, the extremizer walled — and lambda(6) in progress with nine of its ten families closed in this record. The double-sum-core obstruction theorem (no classical weight works on b+c = a+d = e) and the Fejér–Riesz comb weight that beats it are re-proved by the battery at every run. | battery-gated |
| terra-sigmastar.json | The exact crossover of the MFG splitting program: σ* = 1/(8π²), discount-free, DECIDED IN EXACT RATIONALS — the crossover polynomial factors, the γ-coefficient is identically zero (checked k = 2..12), the band-pass identity and both harmonic windows are exact, π enters only as a Machin bracket of width 1.3e-44. | battery-gated the report |
| terra-bracket-table.json | The bracket table under the splitting theorems: seven certified rows straddling both predicted thresholds — negatives below the amplitude threshold and past the crossover, replications, and the threshold pin r_c ∈ [0.13, 0.14] with the exact-rational prediction landing inside. Honest counting lives here: two theorems plus a table, never eight. | battery-gated the report |
| mfg-cap-multiplicity.json | Certified multiplicity for the ergodic quadratic MFG past its pitchfork: at each of six couplings, at least THREE distinct exact solutions enclosed in pairwise disjoint uniqueness balls with certified positive density — exactly where Lasry–Lions monotonicity is silent. The c = −9.5 monotone-regime boundary, where the branch collapses and no claim is made, is recorded too. | battery-gated the report |
| attnflow-theorems.json | The attention-wing theorems: a rational-kernel token flow chosen so equilibrium and stability are DECIDABLE in exact ℚ — the consensus spectrum proved β- and p-free by exact dual-number expansion, the two-cluster cross-weights identically zero with the honest p = 1 boundary, the reduced flow’s double zero decided by exact division (every pitchfork claim refuted), and the phantom-bifurcation taxonomy with its live artifact. | battery-gated the report |
| facelaw-theorem.json | The face-dimension law k = |shared| − cons + z, decided against the exact ℚ null space on two seeded 4,000-network ensembles; every instance where the natural shortcut fails (precisely the z > 0 cases) is ENUMERATED here so any reader can re-run any one. | battery-gated the report |
| terra-recert-t1.json | The T1 enclosure of the congestion-MFG splitting program: a radii-polynomial certificate around the stored candidate — exact instance parameters, certified ℓ¹_ν ball radius, contraction bound Z₁, closure margin, and density floor — re-certified here against the frozen published verifier extended with the data terms; nine falsifiers fire per instance at every battery run. | battery-gated the report |
| terra-peakcount-t1.json | The certified peak count for T1: the exact number of strict maxima of EVERY density in the T1 enclosure ball, derived from CERTIFIED region signs only (instruments/critcount) — outward coefficient products, ball Lipschitz folded into the cell pad, never a float sign. | battery-gated the report |
| terra-recert-t2.json | The T2 enclosure of the congestion-MFG splitting program: a radii-polynomial certificate around the stored candidate — exact instance parameters, certified ℓ¹_ν ball radius, contraction bound Z₁, closure margin, and density floor — re-certified here against the frozen published verifier extended with the data terms; nine falsifiers fire per instance at every battery run. | battery-gated the report |
| terra-peakcount-t2.json | The certified peak count for T2: the exact number of strict maxima of EVERY density in the T2 enclosure ball, derived from CERTIFIED region signs only (instruments/critcount) — outward coefficient products, ball Lipschitz folded into the cell pad, never a float sign. | battery-gated the report |
| terra-recert-t3.json | The T3 enclosure of the congestion-MFG splitting program: a radii-polynomial certificate around the stored candidate — exact instance parameters, certified ℓ¹_ν ball radius, contraction bound Z₁, closure margin, and density floor — re-certified here against the frozen published verifier extended with the data terms; nine falsifiers fire per instance at every battery run. | battery-gated the report |
| terra-peakcount-t3.json | The certified peak count for T3: the exact number of strict maxima of EVERY density in the T3 enclosure ball, derived from CERTIFIED region signs only (instruments/critcount) — outward coefficient products, ball Lipschitz folded into the cell pad, never a float sign. | battery-gated the report |
| terra-recert-t4.json | The T4 enclosure of the congestion-MFG splitting program: a radii-polynomial certificate around the stored candidate — exact instance parameters, certified ℓ¹_ν ball radius, contraction bound Z₁, closure margin, and density floor — re-certified here against the frozen published verifier extended with the data terms; nine falsifiers fire per instance at every battery run. | battery-gated the report |
| terra-peakcount-t4.json | The certified peak count for T4: the exact number of strict maxima of EVERY density in the T4 enclosure ball, derived from CERTIFIED region signs only (instruments/critcount) — outward coefficient products, ball Lipschitz folded into the cell pad, never a float sign. | battery-gated the report |
| terra-recert-t5.json | The T5 enclosure of the congestion-MFG splitting program: a radii-polynomial certificate around the stored candidate — exact instance parameters, certified ℓ¹_ν ball radius, contraction bound Z₁, closure margin, and density floor — re-certified here against the frozen published verifier extended with the data terms; nine falsifiers fire per instance at every battery run. | battery-gated the report |
| terra-peakcount-t5.json | The certified peak count for T5: the exact number of strict maxima of EVERY density in the T5 enclosure ball, derived from CERTIFIED region signs only (instruments/critcount) — outward coefficient products, ball Lipschitz folded into the cell pad, never a float sign. | battery-gated the report |
| terra-recert-t6.json | The T6 enclosure of the congestion-MFG splitting program: a radii-polynomial certificate around the stored candidate — exact instance parameters, certified ℓ¹_ν ball radius, contraction bound Z₁, closure margin, and density floor — re-certified here against the frozen published verifier extended with the data terms; nine falsifiers fire per instance at every battery run. | battery-gated the report |
| terra-peakcount-t6.json | The certified peak count for T6: the exact number of strict maxima of EVERY density in the T6 enclosure ball, derived from CERTIFIED region signs only (instruments/critcount) — outward coefficient products, ball Lipschitz folded into the cell pad, never a float sign. | battery-gated the report |
| terra-recert-t7.json | The T7 enclosure of the congestion-MFG splitting program: a radii-polynomial certificate around the stored candidate — exact instance parameters, certified ℓ¹_ν ball radius, contraction bound Z₁, closure margin, and density floor — re-certified here against the frozen published verifier extended with the data terms; nine falsifiers fire per instance at every battery run. | battery-gated the report |
| terra-peakcount-t7.json | The certified peak count for T7: the exact number of strict maxima of EVERY density in the T7 enclosure ball, derived from CERTIFIED region signs only (instruments/critcount) — outward coefficient products, ball Lipschitz folded into the cell pad, never a float sign. | battery-gated the report |
| terra-recert-t8.json | The T8 enclosure of the congestion-MFG splitting program: a radii-polynomial certificate around the stored candidate — exact instance parameters, certified ℓ¹_ν ball radius, contraction bound Z₁, closure margin, and density floor — re-certified here against the frozen published verifier extended with the data terms; nine falsifiers fire per instance at every battery run. | battery-gated the report |
| terra-peakcount-t8.json | The certified peak count for T8: the exact number of strict maxima of EVERY density in the T8 enclosure ball, derived from CERTIFIED region signs only (instruments/critcount) — outward coefficient products, ball Lipschitz folded into the cell pad, never a float sign. | battery-gated the report |
| mfg-cap-census-N2-c-12.json | The Krawczyk exhaustion census at Galerkin level N = 2: every subbox of the printed box eliminated by interval residual or Krawczyk exclusion, each survivor isolated by K(X) ⊂ int(X) — EXACTLY three solutions of the truncated even system at c = −12, matched one-to-one to the candidates. Box-bounded, truncation-level; the PDE-level count is the stated open problem. | battery-gated the report |
| mfg-cap-census-N3-c-12.json | The Krawczyk exhaustion census at Galerkin level N = 3: every subbox of the printed box eliminated by interval residual or Krawczyk exclusion, each survivor isolated by K(X) ⊂ int(X) — EXACTLY three solutions of the truncated even system at c = −12, matched one-to-one to the candidates. Box-bounded, truncation-level; the PDE-level count is the stated open problem. | battery-gated the report |
| mfg-cap-census-N4-c-12.json | The Krawczyk exhaustion census at Galerkin level N = 4: every subbox of the printed box eliminated by interval residual or Krawczyk exclusion, each survivor isolated by K(X) ⊂ int(X) — EXACTLY three solutions of the truncated even system at c = −12, matched one-to-one to the candidates. Box-bounded, truncation-level; the PDE-level count is the stated open problem. | battery-gated the report |
| mfg-cap-census-N5-c-12.json | The Krawczyk exhaustion census at Galerkin level N = 5: every subbox of the printed box eliminated by interval residual or Krawczyk exclusion, each survivor isolated by K(X) ⊂ int(X) — EXACTLY three solutions of the truncated even system at c = −12, matched one-to-one to the candidates. Box-bounded, truncation-level; the PDE-level count is the stated open problem. | battery-gated the report |
| ember-spectrum.json | Stage 1 of the hot-spots chain: two-sided spectrum localization for the trapezoid — interval Galerkin Rayleigh–Ritz uppers (floats only pick the subspace), exact-rational Crouzeix–Raviart assembly with interval LDLᵀ inertia counts and Liu’s framework for the lowers; the certified gap makes μ₁ SIMPLE. The rectangle regression encloses π² at every run. | battery-gated the report |
| ember-defect.json | Stage 2: the frozen Helmholtz trial’s boundary defect — order-2 interval Taylor jets along every edge with Bessel-ODE closure, a certified midpoint-Taylor cell rule, value AND derivative bridges against an independent float evaluation, and the exact trial coefficients frozen for every downstream stage. | battery-gated the report |
| ember-eigenpair.json | Stage 3: the eigenpair certificate — the boundary-residual identity with the rational star-shaped trace constant and the CR localization tightens μ₁ by a factor of ~105 and encloses the eigenfunction in L²; also the H¹ error and the δλ bound the pointwise machinery consumes. | battery-gated the report |
| ember-pointwise.json | Stage 4: the solid-mean pointwise machinery — kernel norm I₀ = 5/48 DERIVED in exact rationals, witness balls decided inside Ω in exact rationals, and every CORE cell of the 1/100 grid (corner-min depth ≥ 3/40, exact by concavity) killed on both sides with zero survivors. | battery-gated the report |
| ember-collar.json | Stage 5: the collar sweep — every sub-core cell killed by the value argument with REFLECTED pointwise bounds across its nearest open edge (the single layer bounded by the certified per-edge flux sups), kill-or-refine to 1/800, ZERO residual cells. | battery-gated the report |
| ember-corner.json | Stage 6: the four corner-tip certificates — Bessel–Fourier coefficients certified by annulus L² extraction AND re-extracted at a second annulus (the enclosures must intersect — a condition of entry), value kills at B/C/D, radial monotonicity at A, and the ladder-identity wedge bound at C where the boundary minimum lives. | battery-gated the report |
| ember-cross.json | The independent cross-derivations: I₀ = 5/48 in exact rationals, the trace constant re-derived on directed dyadic big-floats from the exact-rational star geometry, μ₁ bounded above on an independent conforming P1 basis, and the two-annulus corner condition re-asserted. | battery-gated the report |
| ember-theorem.json | The assembled hot-spots theorem: cross-record chain consistency (every stage’s inputs equal the upstream outputs), the interior partition RE-DECIDED IN EXACT RATIONALS, every sweep and tip verdict re-checked, the honest framing with its fence list, and the sha256 of every input record. | battery-gated the report |
Code, corpus, and full provenance: github.com/carlostoledo1891/cert-machine — MIT, no dependencies. Instruments lifted from a private source lab are hash-pinned in PROVENANCE.json; patches are declared so they can never be mistaken for drift.
This is one machine and one operator. The trust base is stated rather than hidden: V8’s big-integer arithmetic and IEEE-754 correct rounding are assumed correct, and a handful of named external theorems are consumed and cross-checked rather than machine-proved. Nothing here is a formal proof in the sense of Lean or Coq, and no page claims to be.
What it does meet is the working standard of the computer-assisted-proof tradition — Tucker on the Lorenz attractor, Galias on the Hénon censuses, whose published counts this machine reproduces independently. That is one rung below a formal proof and several rungs above a decimal that looked convincing.