v0.6.0

Stärkere Evidenz — zweiter maschineller Beweis, konsistente Zahlen.

Neu

• Zweiter Lean-Invariant: Nichtnegativität. proofs/Werterhaltung.lean beweist jetzt sorry-frei sowohl Werterhaltung als auch Nichtnegativität (kein Konto wird je negativ, über jede Buchungsfolge). #print axioms für beide: nur propext, Quot.sound. Auf Lean 4.31.0 (CI-Toolchain) verifiziert. Die Drei-Schichten-Kette Typen→Property→Beweis ist damit für zwei Invarianten geschlossen, nicht mehr nur einen.
• ledger 6/6 (vorher 5/5): In-Suite-Diskriminierungstest (der naive Gebühren-Entwurf verliert beweisbar Wert, der korrekte erhält ihn) + geweitete Generatoren, die den Ablehnungs-/Nichtnegativitätspfad real auslösen.

Korrektheit

• derive-tests-Bug: veraltete Test-Namen bei umsortierten Kriterien werden jetzt korrigiert statt blind übersprungen (+ Regressionstest). CDD 37/37.
• Zahlen über Paper (neu kompiliert, 19 S.), Whitepaper, Talk, Onboarding, Blog, Landing konsistent; ledger-Verweise auf den belegenden Commit re-ankert.

docker run -d -p 8080:8080 -v /srv/cdd/data:/data ghcr.io/koschnag/cdd:v0.6.0