Relationship to the research program

Theorem Library is one layer in a larger evidence architecture.

research question / observation
          |
          v
mathematical subclaim worth settling
          |
          v
Theorem Library (Lean proof)
          |
          v
stable theorem identifier
          |
          v
Research Notes explanation + claim boundary

Research Notes

Research Notes tells the public research story. It explains why a theorem was needed, how it changed the experiment plan, and what empirical conclusion does not follow automatically.

Private research layer

Active theorem-ledger state, unpublished mathematical branches, correspondence to private runs, and promotion decisions can remain private until ready.

Why separate repositories

The separation lets a reader inspect the mathematics without needing training code or private infrastructure, while also preventing a formal result from inheriting empirical status merely by living next to an experiment.

The public formal checkpoint index connects theorem identifiers back to the notebooks that use them.