Formal statements

The mathematical statements behind the lab’s results, set as formulas, for a technical reader. Each is labelled by the tool that checked it, or as measured; results not listed here say on their own pages how they were checked. The plain account of each result is on its own page, and the lab’s exact wording is one link further.

The lab’s exact wording, result by result

One statement that is not presented as a result

The high-k dielectric screen, the row below headed “An optical-only screen for high-k dielectrics, against a bar the lab chose”, is a finding about two public computed materials databases, not laboratory measurements.

The lab’s record of current claims does not list this result, and its run record notes uncommitted changes in the working copy it ran from. It is shown with the formal statements, not as one of the lab’s results.
As the formula reads, the bar is a total dielectric constant of at least 20 together with a band gap of at least 1 eV, and the optical-only screen keeps materials whose optical dielectric constant is at least 10.
The lab says it wrote the bar down before the run; this site holds no date or commit for it.

Theorems & Bounds

Checked by the Lean 4 kernel; standard axioms only, per its receipt
$no-leakage \land full-reuse ⟹ ∣ S ∣ \geq 2^{T \cdot n} ⟹ lo g_{2} ∣ S ∣ \geq T \cdot n$
$no-leakage \land full-reuse$ $⟹ ∣ S ∣ \geq 2^{T \cdot n}$ $⟹ lo g_{2} ∣ S ∣ \geq T \cdot n$
A cache-bookkeeping bound (dense-rights model only)
A pooled cache policy that shares cached prompts across T tenants and n blocks with zero leakage and full reuse needs at least T·n bits of isolation state, in the dense rights model: T*n is the DENSE rights model -- every (tenant, block) right independent. It binds when a block may be authorized to an arbitrary SUBSET of tenants (group / shared-read ACLs). If each block belongs to a single tenant, the floor (not part of the Lean statement) is T^n states = n*log2(T) bits, exponentially smaller.
What was shown
A machine-checked proof that a shared AI cache which never leaks between customers and always reuses what it may must remember at least one bit for every pairing of a customer with a cached item, where any item can be shared with any group of customers (the lab’s “dense rights model”).
Why it matters
A provider that serves many customers from one shared model cache must never hand one customer’s cached work to another, yet wants to reuse it whenever that is allowed. The question is how much permission bookkeeping that takes.
AxiomLimit · The full result · Certificate
Checked by the Lean 4 kernel; standard axioms only, per its receipt
$\forall σ \in Ev^{*} : mem_{AP} (run_{G, c} (σ)) \leq G = 64 KiB (c = 16 KiB);$ $\forall B \exists σ : mem_{AP} (run_{c}^{no quota} (σ)) > B$
$\forall σ \in Ev^{*} : mem_{AP} (run_{G, c} (σ)) \leq G = 64 KiB$ $(c = 16 KiB);$ $\forall B \exists σ : mem_{AP} (run_{c}^{no quota} (σ)) > B$
A hard memory ceiling for post-quantum Wi-Fi
With the lab's admission quota, no attacker schedule, however many sessions, pushes it past 64 KiB; without it, every memory budget can be broken. Proved for a hand-written Lean model of the lab's admission-control module, not its code, and not over a radio. In the lab’s model the access point reserves four 16 KiB slots and refuses a fifth; the lab’s account is that four unfinished sign-ins therefore block other devices. Whether slots expire is not stated in the files we serve.
What was shown
In the lab’s model of its admission-control module (the code that decides which sign-ins an access point accepts), a machine-checked proof that an access point’s memory for half-received quantum-resistant sign-ins stays capped, however many devices an attacker connects.
Why it matters
In the lab’s model, an access point keeps half-received quantum-resistant sign-ins in memory until the devices sending them are verified. In that model, capping the memory per connection alone does not stop an attacker who opens many connections at once from exhausting the access point’s memory.
OrbitalProof · The full result · Certificate
Certified by interval arithmetic
$\forall θ \in Θ_{pair} : k (θ) = \frac{C _{true} ( θ )}{C _{pairwise} ( θ )} \leq 0.90524537 ⟹ \frac{C _{pairwise}}{C _{true}} \geq 1.10467$
$\forall θ \in Θ_{pair} :$ $k (θ) = \frac{C _{true} ( θ )}{C _{pairwise} ( θ )} \leq 0.90524537$ $⟹ \frac{C _{pairwise}}{C _{true}} \geq 1.10467$
Pair-by-pair coupling overstates tight via pairs
Inside the lab's frozen simplified model, for every layout in this design family, adding up coupling one pair of vias at a time over-predicts the worst case by at least the floor in the formula beside this text: certified, not sampled. Against the lab's more exact solver the gap is measured on examples only.
What was shown
A proof, over every layout in one narrow family in a simplified model, that adding up coupling one pair at a time always overstates the worst case by at least a stated minimum.
Why it matters
The lab’s starting point is that fast chip-package tools estimate the coupling within a group of vertical wires by adding it up one pair at a time; its record gives no source for which commercial tools do. In the sources the lab searched (listed below), how wrong that pair-by-pair sum can be appears only as sampled examples, not as a guaranteed minimum over a whole family of layouts.
ChipletOS · The full result · Certificate
Measured bound
$1347 \leq ∣ π_{reticle} ∣ \leq 1379 bytes for 64 \leq N_{tiles} \leq 1048576 (measured)$
$1347 \leq ∣ π_{reticle} ∣ \leq 1379 bytes for 64 \leq N_{tiles} \leq 1048576 (measured)$
A whole-reticle certificate whose size stayed nearly flat across the tile counts measured
Fold-annotated certificates compose tile to reticle and stay 1,347-1,379 bytes across 64 to 1,048,576 tiles, checkable by a verifier importing only hashlib, hmac, json and math. Its size was measured only across those tile counts, not proved constant beyond them, and its assurance does not stay constant: the number of tiles that must be opened grows with how small a chance of missing a corrupted tile is wanted. An unchallenged tile is not proven correct.
What was shown
A sign-off record for a whole photomask that stayed a little over a kilobyte in size across every mask size the lab tried; its size does not buy assurance.
Why it matters
Handing someone a sign-off record for a whole photomask built from per-piece records means handing over something that grows with the number of pieces. Constant-size summaries of many records are standard since hash trees, so the lab’s claim is narrower: how four pass/fail checks combine into one record.
ChipletOS · The full result · Certificate
Measured bound
$# {compound attacks} = 8 generations \times 1400 evaluations = 11200, # {escapes} = 0$
$# {compound attacks} = 8 generations \times 1400 evaluations = 11200,$ $# {escapes} = 0$
11,200 budgeted attempts against the lab’s models, none got through
A search given no starting attack sequence, combining moves from the lab’s own list of known attacks up to ten steps deep, searched ten post-quantum Wi-Fi handshake designs, and none got past the protected configuration. How deep it went, in the lab's words: it tried about 1,120 per design, roughly 1% of just the two-step combinations, while combinations of up to ten steps were allowed. A second run the lab calls exhaustive (up to three attack families) found none. As a control, with the known attack KRACK re-opened in the lab’s models, the same search finds an escape. A budgeted search against the lab's own software models, not a proof that no attack exists.
What was shown
An automated search, given no starting attack sequence and no hint of which combination might work, tried combinations of moves from the lab’s own list of known attacks against the lab’s hardened models of quantum-resistant Wi-Fi sign-in designs, and, within a small fixed budget, found no combined attack that got through.
Why it matters
A designer’s own list of attacks tests only what the designer thought of, so the lab’s claim that its repairs close combined attacks rests only on the attacks the lab thought to write down. The search is “unseeded” in one sense only: it was given no starting attack sequence and no hint of which combination works. It still builds its attempts from the lab’s own list of known attack moves, so it can find only combinations of those moves.
OrbitalProof · The full result · Certificate
Measured bound
$P (E_{g} < 1 eV ∣ ε_{el} \geq 10) = 0.883,$ $P (ε_{el} < 10 ∣ ε_{tot} \geq 20 \land E_{g} \geq 1 eV) = 0.913$
$P (E_{g} < 1 eV ∣ ε_{el} \geq 10) = 0.883,$ $P (ε_{el} < 10 ∣ ε_{tot} \geq 20 \land E_{g} \geq 1 eV) = 0.913$
An optical-only screen for high-k dielectrics, against a bar the lab chose
Against a bar the lab says it wrote down before the run (this site holds no date or commit for it), an optical-only screen for high-k gate dielectrics misses 42 of the 46 materials that meet the bar in the Materials Project's dielectric data. There, 136 of the 154 materials it picks have a band gap under 1 eV, so fail the bar. In the Joint Automated Repository for Various Integrated Simulations (JARVIS) it misses 606 of 709, and 1186 of its 1435 picks have a band gap under 1 eV.
Lattice Graph · Certificate

How we show numbers

Every number on this site links to the file it comes from. How each result is checked

We never show a number before its file has loaded.
A question we have not checked yet is marked as unchecked.
A check that found nothing says so.
A file with no value for a question says so.
A number whose file is missing or has changed is not shown.
Two files that disagree about what a number describes are both flagged.
A number from too few samples shows its sample size.
Two files that give different values are both shown.
A file we cannot publish is listed by its fingerprint only.
A measurement more than a week old shows its age.
A question that does not apply to a page is left off it.
A measurement whose program failed is shown as failed.

Formal statements

The lab’s exact wording, result by result

One statement that is not presented as a result

Theorems & Bounds

A cache-bookkeeping bound (dense-rights model only)

A hard memory ceiling for post-quantum Wi-Fi

Pair-by-pair coupling overstates tight via pairs

A whole-reticle certificate whose size stayed nearly flat across the tile counts measured

11,200 budgeted attempts against the lab’s models, none got through

An optical-only screen for high-k dielectrics, against a bar the lab chose