loadbearing 0.1.1

╔════════════════════════════════════════════════════════════════════════════════════════════╗
║                                                                                            ║
║  ██╗      ██████╗  █████╗ ██████╗ ██████╗ ███████╗ █████╗ ██████╗ ██╗███╗   ██╗ ██████╗    ║
║  ██║     ██╔═══██╗██╔══██╗██╔══██╗██╔══██╗██╔════╝██╔══██╗██╔══██╗██║████╗  ██║██╔════╝    ║
║  ██║     ██║   ██║███████║██║  ██║██████╔╝█████╗  ███████║██████╔╝██║██╔██╗ ██║██║  ███╗   ║
║  ██║     ██║   ██║██╔══██║██║  ██║██╔══██╗██╔══╝  ██╔══██║██╔══██╗██║██║╚██╗██║██║   ██║   ║
║  ███████╗╚██████╔╝██║  ██║██████╔╝██████╔╝███████╗██║  ██║██║  ██║██║██║ ╚████║╚██████╔╝   ║
║  ╚══════╝ ╚═════╝ ╚═╝  ╚═╝╚═════╝ ╚═════╝ ╚══════╝╚═╝  ╚═╝╚═╝  ╚═╝╚═╝╚═╝  ╚═══╝ ╚═════╝    ║
║                                                                                            ║
║                                   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      525      247              278  53.0%       axac3          515
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 sha256 6a3a8589, 51,185,034 bytes, with syntax excluded: 49,261 nodes and 905,274 consumed edges, in about forty seconds. The counts move with the database, so the digest is part of the figure. An earlier release quoted this table against a revision that no longer exists anywhere, which is the failure the digest is here to prevent.

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.

Where the measurement comes from

Severing is introduced by mmforge.impact, by the same author, which states it and computes it the same way: the theorems whose every route to the axiom passes through T are its dominator subtree on the reversed proof DAG. This package makes that measurement portable. It runs over any ledger rather than a Metamath database, takes a target set rather than one axiom, and attaches a witness to every answer.

Dominators are Lowry and Medlock, 1969; the iterative form is Cooper, Harvey and Kennedy, 2001.

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
pip install -e ".[formal]"
python -m unittest discover -s tests

210 tests, and no test framework to install. 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.