Appending adds sizes.
Not proved yet, so it sits in the Open group.
Guarantees
Open
Tally.Laws
Falsified
Tally.Laws
The claim that all totals match is false.
The name's _falsified suffix files this disproof in the Falsified group.
Checks
Tally.Laws
Generated tallies sum correctly.
✓ No axioms@checked with one thousand generated tallies, which files it in the Checks group.
Guarantees
Tally.Laws
Appending adds totals.
✓ No axiomsThe total of two tallies appended equals the sum of their totals.
The empty tally changes nothing.
✓ No axiomsAppending empty leaves the total as it was.
Size is stable.
Rests on Laws.counts_are_smallRests on the assumption above, so its badge reads as axiom-dependent.
Tally.Prose
A first line wholly in bold titles a theorem.
✓ No axiomsA Theorem or Corollary with this form appears on the Guarantees page under that title. A Lemma
never does.