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.
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
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.