fix: make the positive implication target auditable

[Deicyde]

Important

This companion fix is stacked directly on #1316 and targets implicationset, not master. Because #1316 still contains the old #1315 API, the first two commits carry the #1321 replacement and its distinct-context hardening.

Caution

Maintainer scope decision required before merge. Felix's original implicationSet is not a complete signed classification: for each unordered pair {A, B} it includes only A → B and A → ¬B, omitting the inequivalent B → A and ¬A → B classes. A faithful distinct-property signed target modulo contraposition would therefore have 120,540 obligations, not 60,270. This PR deliberately offers the existing dashboard's coherent 60,270 directed-positive fragment instead and names it PiBasePositiveImplicationGoal; it does not claim to settle the eventual signed project goal.

Why this redesign is needed

The original completion predicate can be inhabited for every property set by classically splitting each implication into true or false. Its independence predicate is separately vacuous because it existentially chooses assumptions after seeing the proposition. The original implicationSet also uses extensional Property values as IDs, so distinct π-Base catalogue entries can collapse.

This PR makes one finite scope explicit: every ordered implication between distinct positive catalogue properties. Negated literals and multi-premise queries remain a separate workflow pending a deliberate signed-target design.

Lean changes

• Replace the old independence claim with conditional VariesUnder evidence whose two named contexts remain visible and must be distinct. The API deliberately makes no consistency or ZFC-independence claim.
• Key pairs by catalogue positions, so extensionally equal properties do not collapse distinct π-Base IDs.
• Bind stable IDs 1 through 246 directly to P1 through P246, with checked ID order, catalogue length, and 60,270-pair cardinality.
• Replace the existential partition with an explicit partial ClassificationPlan; every assigned status must have proof, existential counterexample evidence, or VariesUnder evidence.
• Add one transparent executable canonical plan, a maintained partial-soundness theorem, and the closed PiBasePositiveImplicationGoal. The initial plan is intentionally all-open, and Lean proves both an open pair and the negation of the completion target today.
• Make classificationAudit typecheck the goal/completeness equivalence, require the plan soundness theorem, and fail compilation if either audit theorem gains an axiom beyond propext, Classical.choice, or Quot.sound.
• Import the goal and classification API from the project root.

A generic classically selected plan can still satisfy the generic checker; it does not satisfy the maintained project workflow. The named executable plan and CI audit are the enforcement boundary.

Website integration

• Run the Lean audit during dashboard generation and fail closed on malformed output, wrong declarations, unsound status, wrong counts, catalogue-order mismatch, dirty Lean source, or a revision not exactly named by a canonical upstream remote-tracking ref.
• Publish the exact audit in schema v5 and show its real status: 0 proved, 0 refuted, 0 context-dependent, and 60,270 open.
• State explicitly that the existing π-Base/regex-derived explorer matrix is a separate view and does not count as ClassificationFor progress.
• Relabel hand-maintained independence data as external axiom-dependency metadata. T67 is linked only as the π-Base source note for its converse, not presented as a theorem proving P58 → P57.
• Describe the signed-literal checker as separate and incomparable; unlike the positive target, its canonical census excludes P164.
• Build and verify this integration in PR CI and build Pages from the exact checked-out Lean revision. The external pi-base-data input is pinned.
• Preserve Lean API documentation under /docs, while making the dedicated Pages workflow the sole publisher and limiting Pages/OIDC credentials to its deploy-only job.

Current status

This PR states and audits the positive completion target; it does not claim the explorer matrix or the wider signed problem is complete. The canonical plan is executable and sound under the allowlisted standard Lean axioms, but all 60,270 pairs are currently open.

Verification

• lake build --wfail — 3,101 jobs
• lake build --wfail classificationAudit — 5,590 jobs/facets
• lake exe classificationAudit — 246 properties, 60,270 pairs, sound: true, complete: false
• compile-time audit theorem axiom allowlist — only propext, Classical.choice, and Quot.sound
• npm run test:python — 18 tests
• npm run dashboard:check
• npm run dashboard:build && npm run dashboard:verify from the exact upstream PR ref — 1,598 modules and a commit-bound schema-v5 artifact
• workflow YAML and embedded shell syntax parse; git diff --check