Metadata-Version: 2.5
Name: loadbearing
Version: 0.1.1
Summary: Separate what a claim asserts from what its derivation consumed.
Project-URL: Homepage, https://github.com/vince-gonzalez/loadbearing
Project-URL: Source, https://github.com/vince-gonzalez/loadbearing
Project-URL: Issues, https://github.com/vince-gonzalez/loadbearing/issues
Author-email: Vincent Gonzalez <vincegonzalez@me.com>
License-Expression: Apache-2.0
License-File: LICENSE
Keywords: axioms,epistemology,lean,metamath,provenance,reproducibility
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: Apache Software License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Scientific/Engineering :: Mathematics
Requires-Python: >=3.10
Provides-Extra: formal
Requires-Dist: gonzalgo>=0.5.3; extra == 'formal'
Requires-Dist: mmforge>=0.1.1; extra == 'formal'
Description-Content-Type: text/markdown

```
╔════════════════════════════════════════════════════════════════════════════════════════════╗
║                                                                                            ║
║  ██╗      ██████╗  █████╗ ██████╗ ██████╗ ███████╗ █████╗ ██████╗ ██╗███╗   ██╗ ██████╗    ║
║  ██║     ██╔═══██╗██╔══██╗██╔══██╗██╔══██╗██╔════╝██╔══██╗██╔══██╗██║████╗  ██║██╔════╝    ║
║  ██║     ██║   ██║███████║██║  ██║██████╔╝█████╗  ███████║██████╔╝██║██╔██╗ ██║██║  ███╗   ║
║  ██║     ██║   ██║██╔══██║██║  ██║██╔══██╗██╔══╝  ██╔══██║██╔══██╗██║██║╚██╗██║██║   ██║   ║
║  ███████╗╚██████╔╝██║  ██║██████╔╝██████╔╝███████╗██║  ██║██║  ██║██║██║ ╚████║╚██████╔╝   ║
║  ╚══════╝ ╚═════╝ ╚═╝  ╚═╝╚═════╝ ╚═════╝ ╚══════╝╚═╝  ╚═╝╚═╝  ╚═╝╚═╝╚═╝  ╚═══╝ ╚═════╝    ║
║                                                                                            ║
║                                   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

```bash
pip install loadbearing
```

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

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

```bash
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

```python
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:

```bash
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`](https://pypi.org/project/mmforge/),
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 `Node`s and `Edge`s. 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

| substrate | via | asserted | consumed |
|---|---|---|---|
| Metamath | `mmforge` | — | proof citations |
| Lean 4 | `gonzalgo` | statement dependencies | proof dependencies |

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

## Checking this yourself

```bash
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](https://orcid.org/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](https://f-keys.com) — independent hardware, software
and internet products. See the [working log](https://f-keys.com/log/)
and [live status](https://f-keys.com/status/).
