mirror of
https://github.com/luxfi/magnetar.git
synced 2026-07-27 02:53:47 +00:00
19 lines
991 B
Plaintext
19 lines
991 B
Plaintext
# Unproven-assertion budget (max counts). Enforced by
|
|
# ~/work/lux/luxfi/security/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.
|
|
#
|
|
# HONEST ACCOUNTING: the proof tree contains NO live `sorry`/`admit` tactic and
|
|
# NO theorem/lemma/axiom — the remaining .ec/.lean files are 0-content scaffolds.
|
|
# axiom-budget.sh is now COMMENT-AWARE (it strips (* *) / -- / /- -/ before
|
|
# counting), so the word "admit"/"sorry" inside the scaffold BANNERS that
|
|
# *describe the deleted cheats* ("whose proof body was `sorry`", "by `admit`")
|
|
# no longer counts. The real machine count is SORRY=0 ADMIT=0 AXIOM=0; the
|
|
# 8 banner mentions surface as a prose [warn] only. The budget is the truth (0),
|
|
# so any genuinely NEW live sorry/admit/axiom trips the gate immediately.
|
|
# The headline threshold claim is honestly "research-only", not "proven".
|
|
SORRY=0
|
|
ADMIT=0
|
|
AXIOM=0
|
|
VACUOUS=0
|