2 Commits

Include renames

Author	SHA1	Message	Date
swaitsandClaude Opus 5.5	a7f3cc09a9	P3: odd cents split the same running way everywhere (defect 17, D-38) ... Members' shares of earnings are split cumulatively by largest remainder in the closes, the members' equity statement, the K-1 worksheet and the viewer, so a member's capital on a given day never moves by a cent when its month is later closed. Old closes replay as they were; the first P3 close carries any true-up. Feature members_cumulative. Kani and Lean proofs of the bounded drift; bookspec examples. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01T3gXMVt7XJPi6ens1or9Dj	2026-10-20 21:35:00 -06:00
swaitsandClaude Opus 5.5	714caf9be9	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