feat(lean): migrate + repair tropical proofs; unify the min-max ⇄ max-plus duality

[hyperpolymath]

What

Brings the min-max transport semiring (TropicalAdapterPath.lean) in beside its
max-plus twin (TropicalSessionTypes.lean), repairs both to compile clean under a
pinned Lean 4.13.0 toolchain via Lake, and proves the order-reversing duality that
connects them. Source of the min-max file is the frozen provenance archive in
protocol-squisher — that copy is left untouched.

Why it mattered

Both files, as inherited, did not compile on any installed toolchain (the headers'
Verified: Lean 4.13.0 / 4.29.0 claims were never true — corroborating
protocol-squisher's PROVENANCE.adoc). Only pathCost_mono + hub_ceiling had ever
been machine-checked, in isolation.

Repairs

TropicalSessionTypes.lean (max-plus): import ordering; max-distributivity helpers
(Nat.max_def + split + omega); local One class + OfNat shim (4.13.0 core has Zero
but not One); spec_par QTT case; header version corrected.

TropicalAdapterPath.lean (min-max): import ordering; dangling doc-comment;
push_neg (Mathlib-only) → core tactics; AdapterPath def→abbrev; pathCost_append

• pathCost_le_sequential reproved.

Corrected a false theorem: dual_tcMul_bounded claimed
dual(max m n) = dual m + dual n − maxGrade, false at m=1, n=2 (1 vs 0). Replaced with
the true De Morgan dual dual_tcMul_is_min: dual(max m n) = min(dual m, dual n),
completing the duality pair with dual_tcAdd_is_max.

Verification

• lake build is green.
• Axiom audit: every headline theorem depends only on propext (+ Quot.sound) — no
  sorry, no Classical.choice. CI (.github/workflows/lean.yml) re-runs this and
  fails on any sorry/Classical.choice.

Also

• lean-toolchain (pinned 4.13.0), lakefile.lean, lake-manifest.json, .gitignore.
• docs/LEAN-FORMALIZATION.adoc (authoritative reference), README section, CHANGELOG,
  machine-readable ECOSYSTEM.a2ml, and a drift note on docs/FORMAL-PROOFS.adoc
  (its Lean listings predate the v6.0 source).

Commits GPG-signed (1835A14A).

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 40 issues detected

Severity	Count
🔴 Critical	1
🟠 High	26
🟡 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 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": "Action tions/checkout@v4\n\n needs attention",
    "type": "unpinned_action",
    "file": "lean.yml",
    "action": "pin_sha",
    "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"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "missing_timeout_minutes",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "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"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence