0%

Lean calculus pristine

The proof corpus builds clean apart from one warning, and its conformance verdict is a tracked target-state gap owned by another plan. Pristine means both facts are PROVEN, not assumed.

Measured at authoring: lake build exit 0 with exactly ONE warning — AimsProof/Partition.lean:682:5: unused variable 'hdraw' in theorem scc_external_source_determines. Zero sorry / admit / axiom / native_decide. 18 modules, 15,259 lines, 734 theorem-or-lemma declarations. check-proofs.sh: 182 checked, 1 definition-only skipped, 0 regressions, and locality conformance verdict: divergent_pending (non-fatal). dual-discharge.sh: 130 theorems agree.

Section SIZE is not a completion criterion. Depth comes from proof/statement coverage, theorem-to-rule parity, placeholder lint, dual discharge, and falsifier evidence — NOT from inflating this section into implementing locality.

Deliverables

  • Clear the hdraw warning at its source; lake build emits zero warnings.
  • Placeholder lint proving zero sorry / admit / axiom / native_decide remain, run as a gate rather than a one-time read.
  • Prove every non-passing conformance row is manifest-backed and correctly owned. flip-divergent-pending.sh --as-flip-trigger exits 2 naming seven entries blocked by unified-locality-dimension, and aims-rules.md:49-63 classifies RL-14..21 / RL-22..26 and the fifth Locality value as target-only. Record the evidence; do NOT weaken the flip trigger.
  • Theorem-to-rule parity check: every governing rule the calculus claims has a discharged theorem, and every theorem maps to a rule.
  • Dual-discharge gate green, with the agreeing-theorem count recorded from the script’s own output.