Metadata-Version: 2.5
Name: loadbearing
Version: 0.1.0
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      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.

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

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

## 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
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](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/).
