What it shows
The lab’s own entry states the result this way:
The published record says, word for word (an excerpt)
For every (diameter, pitch, guard height) in the declared N=3 symmetric family, the many-body screening factor is certified k ∈ [0.370, 0.944] by interval branch-and-bound (25,469 boxes, 0 failure regions)
In plain words: the screening factor is the share of the pair’s isolated coupling that remains with the guard in place. The lab’s entry also records a direction, that moving the guard closer increases screening; this page does not say over what range of guard positions that is proved, so we do not rely on it here. The proof processed 25469 boxes of the family’s parameters and found 0 regions where it could not certify the bounds.
Why it matters
Guard vias are a standard way to reduce coupling, and designers size them by rule of thumb or by sampling. A bound proved over the whole family says how much one guard can and cannot do, without sampling.
What is ours, and what is not
Interval branch-and-bound is a known method (see the prior art below), and guard vias are standard practice. What is ours is this family and the certificate.
Who should care
- Package designers sizing guard vias between tight signal pairs.
- Reviewers. The bound holds in a simplified model, and the page says so.
The limits, in the record’s words
The published record says, word for word (an excerpt)
A symbolic Lean lift of this floor was attempted and honestly closed as needing a log-aware proof
In plain words: the bounds hold in a simplified model of the vias, one simulation compared with another, and the gap to our full solver adds on top and is stated, not proved. The general line-up of three vias is not certified, and an attempt to move this floor into a machine-checked proof did not close. The proof’s soundness also assumes the interval core rounds outward correctly, which is tested, not formally proved.
Open source for this step
Tools and datasets we publish for the package step of building a multi-chip package. They are the checkers around this work, not a copy of the result itself.
- physics-lint: One command that checks a folder of physics models against a fixed set of named physical rules, with findings straight into CI.
- maxwell-lint: Flags a coupling extractor whose answers no passive set of conductors could produce.
- sparam-lint: Is your signal-response model physically possible? Five physical laws checked from the command line.
- interval-core: The interval arithmetic core behind our proofs over whole families of layouts.
- touchstone-tools: Read, write and convert Touchstone files, the standard text files that record how signals pass through a package's connections, and refuse to write one that cannot be read back.
- physics-lint-mcp: The physics checks, callable by an AI agent.
- physics-lint-action: A GitHub Action that fails the build when a model breaks one of a fixed set of named physical rules.
- Signal-response validity corpus: A labelled corpus of physically invalid signal-response networks, and a scorer that grades any checker against it.
- screening-ceiling: The screening-ceiling family as an open dataset.