loadbearing
Separates two things every axiom census runs together: what a statement asserts, and what the derivation behind it consumed. They are different questions with different answers.
0.2.0 · pip install loadbearing · Lean 4 and Metamath · MCP server included
What it does
Separates two things every axiom census runs together: what a statement
asserts, and what the derivation behind it consumed. They are
different questions and they have different answers.
pip install "loadbearing[formal]"
Why the distinction pays
Measured across four libraries and two foundations: more than half of
every axiom cone holds up nothing at all. Reach — the count of what
sits downstream of an assumption — overstates responsibility by up to
58× against the severing counterfactual, which asks the harder
question of what actually breaks if you take the assumption away.
It reports what it did not check
A graph carries the population it excluded, and a ledger that excluded
nothing says so explicitly. The digest is taken over installed file contents,
so a measurement can be quoted with the version of the thing that produced it
— a reach without a digest is not a citation, it is a memory.
How it works
- Install it with the extras you need
pip install "loadbearing[formal]" for the Lean and Metamath adapters, [mcp] for the server. - Point it at a libraryIt reads Lean 4 or Metamath and separates asserted dependencies from consumed ones.
- Sever, and see what breaksThe counterfactual is the measurement: not what sits downstream of an assumption, but what actually fails without it.
What it measures
Half of every cone holds up nothingMeasured across four libraries and two foundations.
Reach overstates by up to 58×Counting what is downstream of an assumption is not the same as counting what depends on it, and the gap is enormous.
It carries what it excludedA graph reports the population it left out; a ledger that excluded nothing says so explicitly.
A digest with every measurementTaken over installed file contents, so a number can be quoted with the version that produced it. A reach without a digest is a memory, not a citation.
Lean 4 and MetamathTwo foundations, one measurement.
An MCP serverSo the measurement is available to a tool, not just a shell.
Specifications
| Install | pip install loadbearing |
|---|
| Version | 0.2.0 |
|---|
| Extras | [formal] for Lean and Metamath, [mcp] for the server |
|---|
| Reads | Lean 4, Metamath |
|---|
| Source | vince-gonzalez/loadbearing |
|---|
Questions
- What is the difference from gonzalgo?
- gonzalgo reports which axioms a proof step introduced. loadbearing asks the harder question of what the claim would lose if the assumption were removed.
- Why does the digest matter?
- Because a measurement quoted without the version that produced it cannot be checked by anybody, including you.