loadbearing 0.1.0

╔════════════════════════════════════════════════════════════════════════════════════════════╗
║                                                                                            ║
║  ██╗      ██████╗  █████╗ ██████╗ ██████╗ ███████╗ █████╗ ██████╗ ██╗███╗   ██╗ ██████╗    ║
║  ██║     ██╔═══██╗██╔══██╗██╔══██╗██╔══██╗██╔════╝██╔══██╗██╔══██╗██║████╗  ██║██╔════╝    ║
║  ██║     ██║   ██║███████║██║  ██║██████╔╝█████╗  ███████║██████╔╝██║██╔██╗ ██║██║  ███╗   ║
║  ██║     ██║   ██║██╔══██║██║  ██║██╔══██╗██╔══╝  ██╔══██║██╔══██╗██║██║╚██╗██║██║   ██║   ║
║  ███████╗╚██████╔╝██║  ██║██████╔╝██████╔╝███████╗██║  ██║██║  ██║██║██║ ╚████║╚██████╔╝   ║
║  ╚══════╝ ╚═════╝ ╚═╝  ╚═╝╚═════╝ ╚═════╝ ╚══════╝╚═╝  ╚═╝╚═╝  ╚═╝╚═╝╚═╝  ╚═══╝ ╚═════╝    ║
║                                                                                            ║
║                                   what a claim rests on                                    ║
║                                                                                            ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝

loadbearing separates two things that look alike. What a claim says it rests on is one set. What its derivation actually used is another. In a formal library both are machine-readable, so the distance between them can be measured instead of argued about.

Install

pip install loadbearing

The core has no dependencies. Reading a library needs one more:

pip install "loadbearing[formal]"

That pulls mmforge for Metamath databases and gonzalgo for Lean 4 environment dumps.

633 of the 1,016 hold up nothing

1,016 theorems in set.mm have a route to the axiom of countable choice. Remove any one of 633 of them and every other theorem still gets there, because those 633 hold up nothing except themselves.

seam           reaches  carries  carries nothing  idle share  heaviest  holds up
-------------  -------  -------  ---------------  ----------  --------  --------
ax-cc             1016      383              633  62.3%       axcc2lem       937
ax-ac, ax-ac2      524      247              277  52.9%       axac3          514
ax-13              494      188              306  61.9%       ax13v          493

reaches counts every theorem with a route to the seam. carries counts the ones holding up at least one other theorem. The remainder are leaves of the cone: real users of the axiom that no other proof passes through.

The load is concentrated. One statement, axcc2lem, holds up 937 of the 1,016.

python scripts/severing.py path/to/set.mm

Measured on set.mm at ledger digest ee3fc0f7, with syntax excluded: 49,237 nodes and 904,702 consumed edges, in about forty seconds.

Every answer carries the command that re-derives it

from loadbearing.sever import capture

w = capture("set.mm", ["ax-ac", "ax-ac2"])
w.write_script("reproduce.py")

The script that comes out digests the database, the version of mmforge that read it, and the answer itself. Run it on another machine and point it at your own copy:

python reproduce.py --source database=/your/set.mm

It exits non-zero if the database moved, if mmforge is a different build under the same version number, or if the recomputed answer disagrees with the recorded one. Standard output only ever carries an answer that matched.

The model

A Ledger holds Nodes and Edges. Every edge is ASSERTED or CONSUMED: what the author declared, against what the derivation pulled in. A Node carries a sort — SYNTAX, AXIOM, DEFINITION, DERIVED, UNKNOWN — which is a property of the target and is orthogonal to the edge kind.

Sort matters before any count is taken. In set.mm 40.0% of all consumed edges point at notation, and ten of the twelve most-cited labels are syntax constructors. A centrality figure over the raw edge set measures the grammar of the language. SupportGraph therefore excludes syntax by default and reports the exclusion in every summary, so a number cannot be read without the population it came from.

Split gives the surplus and the deficit for one claim: cited and unused against used and uncited. In Lean, Classical.propDecidable arrives through instance resolution and appears in a proof's dependencies with nothing matching on the statement side, which is what a pure deficit looks like.

What it reads

A Metamath proof records what it used and says nothing about intent, so that adapter produces consumed edges alone.

Checking this yourself

git clone https://github.com/vince-gonzalez/loadbearing
cd loadbearing
python -m unittest discover -s tests

188 tests, no test dependency. The severing measurement is checked twice by different means: a dominator tree over the reversed graph, and a plain closure recomputed with the candidate removed. Every run certifies a sample of the first against the second and raises on a disagreement.

Determinism is checked by running the same measurement in two subprocesses at different PYTHONHASHSEED values and comparing the bytes.

Author

Vincent Gonzalez — 0009-0005-3640-014X · vincegonzalez@me.com

Apache-2.0.

╔════════════════════════════════════════════════════════════╗
║                                                            ║
║      ███████╗      ██╗  ██╗███████╗██╗   ██╗███████╗       ║
║      ██╔════╝      ██║ ██╔╝██╔════╝╚██╗ ██╔╝██╔════╝       ║
║      █████╗  █████╗█████╔╝ █████╗   ╚████╔╝ ███████╗       ║
║      ██╔══╝  ╚════╝██╔═██╗ ██╔══╝    ╚██╔╝  ╚════██║       ║
║      ██║           ██║  ██╗███████╗   ██║   ███████║       ║
║      ╚═╝           ╚═╝  ╚═╝╚══════╝   ╚═╝   ╚══════╝       ║
║                                                            ║
║               ·   C  R  E  A  T  I  V  E   ·               ║
║                                                            ║
║          ────────────────────────────────────────          ║
║                                                            ║
║                      Vincent Gonzalez                      ║
║                         f-keys.com                         ║
║                 ORCID 0009-0005-3640-014X                  ║
║                                                            ║
╚════════════════════════════════════════════════════════════╝

Part of F-Keys — independent hardware, software and internet products. See the working log and live status.