swaitsandClaude Fable 5.1 fb83af5948 verify(lean): one docstring on Books after the S5 and S7 merges ...

The S7 merge kept both branches' doc comments for the Books structure,
S5's (which names the sends) stranded above an unrelated theorem and
S7's on the structure; Lean refused the stray one. S5's text stays, on
the structure it describes. Kani's 52 harnesses verified in the same
run; only Lean's build stopped.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HS8WZziDnyxunC23MUxrLp

2026-10-29 05:02:12 -06:00

..

Apportion.lean

P3: odd cents split the same running way everywhere (defect 17, D-38)

2026-10-20 21:35:00 -06:00

Basic.lean

feat(core): prove the accounting laws (Kani + Lean); fix three engine gaps

2026-10-13 11:12:13 -06:00

Closing.lean

P3: odd cents split the same running way everywhere (defect 17, D-38)

2026-10-20 21:35:00 -06:00

Documents.lean

verify(lean): one docstring on Books after the S5 and S7 merges

2026-10-29 05:02:12 -06:00

Entry.lean

feat(core): prove the accounting laws (Kani + Lean); fix three engine gaps

2026-10-13 11:12:13 -06:00

Ledger.lean

P3: dated 1099 decisions, payment methods and the card exception (defects 23, 12, 18, D-40)

2026-10-21 12:12:26 -06:00

Parties.lean

P3: party totals by what moved the money, once (defects 14, 11, 24)

2026-10-21 12:12:26 -06:00

Prorate.lean

P3: depreciation straight-line by days through the final month, schedules by day (defects 22, 9, D-37)

2026-10-21 14:04:11 -06:00

Statements.lean

P3: the cash flow statement by ASC 230 (defect 1, D-35, D-42)

2026-10-21 09:35:32 -06:00