P-0.3: proof credit from evidence only: l3_kani_proved/l4_lean_proved integers ignored; Kani credit = resolving #[kani::proof] (47), Lean credit = sorry-free resolving theorem (8); declar #2911

DAG row P-0.3 — docs/specifications/pp-066-dag.yaml (epic #2873; spec: #2870 phase 0/1 text (improve-provable-contracts.md not in tree); PP-066 §5 Track P).

Track: P · lane: 0.66 · host: intel (CI runner) for P-0.6, else any · owner: spec-owner · expiry: 2026-09-19 · quorum: review-only

Blockers (rows): DEC-D-11
Linked issues: #2732

A — acceptance (exit 0 = done):

• . scripts/pv_bin.sh && "$PV" proof-status contracts/ --binding contracts/aprender/binding.yaml prints discharged Lean 8 / Kani 47 beside declared 181 / 1,257
• cargo test -p aprender-contracts --lib proof_credit (a contract with hand-typed l4_lean_proved: 7 and no resolving theorem scores 0)

Contract: contracts/pv-p-0-3-v1.yaml
Mutation → RED: re-trust the verification_summary integer in gates_extended.rs:401 / explain_render.rs:133 -> fixture RED

Filed by the PP-066 driver STEP 5; status tracked in the DAG (status: complete after the receipt docs/audits/impl-<ticket>-receipt.md).