feat(rsr+proofs): tropical RSR Bronze (42%→77%) + Lean verified 20/20 + PROOF-STATUS

[hyperpolymath]

Summary

tropical-resource-typing end-to-end — RSR 41.67% → 76.81% (🥉 Bronze) plus a genuinely reproduced Lean proof verification.

Proof verification (the headline)

• Lean 4 — VERIFIED. Installed Lean v4.13.0 (GitHub-direct toolchain; pure core Lean, no Mathlib) and ran lake build after rm -rf .lake/build (clean rebuild). Result: 20/20 targets type-check. No proof changes were needed — the Lean development was already correct.
• Isabelle/HOL — honestly flagged, NOT re-verified here. The 9 *.thy theories (Tropical_Semirings session) are CI-gated via just isabelle-build; Isabelle is a multi-GB toolchain not installed in this environment, so I state that plainly rather than assert it.

PROOF-STATUS.adoc records exactly what was reproduced vs CI-gated.

RSR additions (additive)

• .well-known/{security,ai,humans}.txt
• MAINTAINERS.adoc; CODE_OF_CONDUCT.md (Contributor Covenant + enforcement)
• CONTRIBUTING: Tri-Perimeter Contribution Framework (TPCF)
• flake.nix (elan + just devShell); .gitattributes
• Justfile lean-build + validate recipes

Residual (honest)

flake.lock (needs nix); SECURITY "24 hours" literal (brittle check — tropical has its own SECURITY policy); a "mentions testing" doc nit. Bronze (≥75%) achieved.

Reproduce (Lean)

lake build   # Lean 4 v4.13.0

🤖 Generated with Claude Code

https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 42 issues detected

Severity	Count
🔴 Critical	1
🟠 High	28
🟡 Medium	13

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_workflow",
    "file": "codeql.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "missing_workflow",
    "file": "scorecard.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "missing_workflow",
    "file": "mirror.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/checkout@v4 needs attention",
    "type": "unpinned_action",
    "file": "lean.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in lean.yml",
    "type": "missing_timeout_minutes",
    "file": "lean.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Required file missing (condition: has_dependencies)",
    "type": "missing_requirement",
    "file": ".github/dependabot.yml",
    "action": "create",
    "rule_module": "cicd_rules",
    "severity": "high"
  },
  {
    "reason": "Required file missing (condition: public_repo)",
    "type": "missing_requirement",
    "file": ".github/workflows/scorecard.yml",
    "action": "create",
    "rule_module": "cicd_rules",
    "severity": "high"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/tropical-resource-typing/tropical-resource-typing/tests/validate.test.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "Isabelle oops -- intentionally incomplete proof (1 occurrences, CWE-704)",
    "type": "isabelle_oops",
    "file": "/home/runner/work/tropical-resource-typing/tropical-resource-typing/Tropical_Ordinal.thy",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

[github-actions]

🔍 Hypatia Security Scan

Findings: 42 issues detected

Severity	Count
🔴 Critical	1
🟠 High	28
🟡 Medium	13

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_workflow",
    "file": "codeql.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "missing_workflow",
    "file": "scorecard.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "missing_workflow",
    "file": "mirror.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/checkout@v4 needs attention",
    "type": "unpinned_action",
    "file": "lean.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in lean.yml",
    "type": "missing_timeout_minutes",
    "file": "lean.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Required file missing (condition: has_dependencies)",
    "type": "missing_requirement",
    "file": ".github/dependabot.yml",
    "action": "create",
    "rule_module": "cicd_rules",
    "severity": "high"
  },
  {
    "reason": "Required file missing (condition: public_repo)",
    "type": "missing_requirement",
    "file": ".github/workflows/scorecard.yml",
    "action": "create",
    "rule_module": "cicd_rules",
    "severity": "high"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/tropical-resource-typing/tropical-resource-typing/tests/validate.test.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "Isabelle oops -- intentionally incomplete proof (1 occurrences, CWE-704)",
    "type": "isabelle_oops",
    "file": "/home/runner/work/tropical-resource-typing/tropical-resource-typing/Tropical_Ordinal.thy",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence