swaitsandClaude Opus 5.5 1291547fc4 lean: apportion's parts sum to the whole for any number of parts ...

The ranks of n parts are a permutation of 0..n-1 (being ahead is a strict
total order; pigeonhole by hand, core Lean has no subperm), so exactly
u parts get a unit and one gets the fraction. apportion_sum and
apportion_sum_of_shortfall; the audit shows only the standard axioms.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GWVo7x3UHw5kwCUaWxiejX

2026-10-14 10:17:37 -06:00

..

spec

config, mcp, gui: specs from sources, spec-blind suites, and the bugs they found

2026-10-14 10:13:05 -06:00

architecture.md

config, mcp, gui: specs from sources, spec-blind suites, and the bugs they found

2026-10-14 10:13:05 -06:00

capability-parity.md

feat: receipt unlink and attachment withdrawal

2026-10-11 18:40:51 -07:00

glossary.md

Initial commit: wanderbooks accounting semantics engine

2026-10-11 00:46:04 +00:00

mcp-interface.md

config, mcp, gui: specs from sources, spec-blind suites, and the bugs they found

2026-10-14 10:13:05 -06:00

oracle.md

test: fuzzing, Miri, benchmarks, CI, and a strategy note; the journal refuses floats

2026-10-13 15:09:22 -06:00

parallel-run.md

Next steps 5-10: resources, cash flow, QB interop, backfill, HTTP, parallel-run plan

2026-10-11 03:02:53 +00:00

parity.md

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

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

receipt-store.md

store: refusals leave the live books untouched; per-filing names; spec suite

2026-10-13 19:24:34 -06:00

requirements.md

fix(core): due-today is Current; odd cents split by largest remainder

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

testing.md

lean: apportion's parts sum to the whole for any number of parts

2026-10-14 10:17:37 -06:00

verification.md

closes: a run of members closes splits cumulatively

2026-10-13 18:58:21 -06:00