docs(proof): KRL-specific proof narrative + assumption registry; drop template content

[hyperpolymath]

Summary

Replace template-content "proofs" with a coherent KRL-specific proof narrative and an explicit assumption registry.

What's added

• PROOF-NARRATIVE.md — single coherent story of what KRL proves, what it assumes, and what it owes. Covers obligations KR-1..KR-8 with statement, why valuable, status, explicit assumptions, and how to discharge per obligation.
• ASSUMPTIONS.md — registry of every load-bearing unproven assumption (12 entries, classified MATH / DESIGN / EMPIRICAL / CRYPTO).

What's rewritten

• PROOF-NEEDS.md — 8-row per-obligation checklist (KR-1..KR-8) with category, prover, priority, effort. Previously was a template scaffold with the "Project-Specific Proofs" section empty (just | | | | | | |).
• TEST-NEEDS.md — KRL-specific (CRG D, real test inventory). Previously referred to "rsr-template-repo" throughout and claimed CRG Grade: C — ACHIEVED 2026-04-04 which referred to the template, not KRL.
• PROOF-STATUS.md — now reflects actual KR-1..KR-8 obligations (0 proven / 2 partial / 6 not started) instead of 7 mythical template obligations.

What's deleted (recoverable from rsr-template-repo upstream)

File	Was	Why deleted
verification/proofs/coq/TypeSafety.v	generic Inductive ty := TyNat | TyBool typed arithmetic	Nothing KRL-specific. Header says "Coq Proof Template".
verification/proofs/lean4/ApiTypes.lean	generic ApiResult α Functor laws + BoundedNat	Nothing KRL-specific. Header says "Template — replace with your project's API types."
verification/proofs/idris2/Types.idr	generic Bounded record + NonEmpty list	Nothing KRL-specific. Header says "Template — replace with your project's core types."
verification/proofs/idris2/ABI/Pointers.idr	generic SafePtr + Handle	Nothing KRL-specific. Header says "Template proof — customise for your project's pointer types."
.../Foreign.idr .../Layout.idr .../Platform.idr .../Compliance.idr	generic ABI scaffolds	All "Template proof".

The 2026-06-01 audit found these were creating a false impression of formal verification: PROOF-STATUS.md claimed "7 proofs remaining, 0 proven" without acknowledging that the 7 listed were templates.

README correction

README.adoc claimed the KRL parser/lowering lives in this repo ("TanglePL compiler module (this repo)"). It does not — it lives in KRLAdapter.jl (canonical) and quandledb/server/krl/ (server-side query parser). The architecture diagram is corrected to attribute implementations to their actual repos.

What KRL's soundness actually rests on now

The actual semantic-core proofs live in hyperpolymath/tangle/proofs/Tangle.lean (16 results including Progress, Preservation, Determinism, Type Safety + 12 lemmas). KRL's job is the lowering — PROOF-NARRATIVE.md makes that obligation explicit (KR-1, KR-2, KR-3) instead of papering over it.

Test plan

• No tests broken (this PR is docs-only + scaffold-deletion).
• panic-attack assail --proofs-only no longer reports template-content false-positives.
• GPG-signed commit.
• All edited files pass the global pre-commit Owner check.
• Auto-merge with squash + branch delete.

Part of the focused krl + quandledb + tangle audit/elevation pass. Not estate-wide. Companion PRs in tangle and quandledb adding their own PROOF-NARRATIVE + ASSUMPTIONS follow.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 71 issues detected

Severity	Count
🔴 Critical	4
🟠 High	7
🟡 Medium	60

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dependabot-automerge.yml",
    "type": "missing_timeout_minutes",
    "file": "dependabot-automerge.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "missing_timeout_minutes",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence