luxfi/magnetar
1
0
Fork 0
mirror of https://github.com/luxfi/magnetar.git synced 2026-07-27 02:53:47 +00:00
Code Issues Packages Projects Releases Wiki Activity

high-assurance: declare unproven-assertion budget

Browse Source 
Enforced by ~/work/lux/proofs/framework/check.sh. Caps the current trust
surface so it cannot silently grow; the goal is to drive it down.
This commit is contained in:
Antje Worring
2026-06-21 13:37:32 -07:00
parent df4c537c16
commit 31227a435a
1 changed files with 10 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
.assurance/budget.txt
+10
View File
@@ -0,0 +1,10 @@
# Unproven-assertion budget (max counts). Enforced by
# ~/work/lux/proofs/framework/checks/axiom-budget.sh. FAILS on any drift above.
# Goal: decrease, never raise. Current surface (2026-06), after deleting the
# circular/vacuous strict-atom proofs. The remaining 4 sorry + 4 admit are in
# SUPPORTING (non-load-bearing) lemmas, disclosed in PROOF-CLAIMS; the headline
# threshold claim is now honestly "research-only", not "proven".
SORRY=4
ADMIT=4
AXIOM=0
VACUOUS=0