Definition: Ledger entry and status

Each ledger entry records:

1. its mathematical statement and domain of quantification;

2. the operational data or extracted object on which it depends;

3. whether it is a declaration, an additional assumption, a derived property, an open obligation, or a documentary comparison;

4. its proof or source, where a derivation is claimed;

5. the exact conclusion for which it is used.

The status labels are

Only $\mathsf{ASSUMED}$ entries belong to the additional hypothesis list as assumptions. A $\mathsf{DERIVED}$ entry must name its actual premises and proof. An $\mathsf{OPEN}$ entry cannot be used as a proved premise.