fix: make the positive implication target auditable

.github/workflows/lean_action_ci.yml

@@ -5,19 +5,45 @@ on:
   pull_request:
   workflow_dispatch:
 
-# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
 permissions:
-  contents: read # Read access to repository contents
-  pages: write # Write access to GitHub Pages
-  id-token: write # Write access to ID tokens
+  contents: read
 
 jobs:
   build:
     runs-on: ubuntu-latest
 
     steps:
       - uses: actions/checkout@v5
+        with:
+          # Dashboard provenance checks need the canonical branch/PR refs.
+          fetch-depth: 0
+      - name: Bind pull-request revision to the canonical remote
+        if: github.event_name == 'pull_request'
+        env:
+          PR_NUMBER: ${{ github.event.pull_request.number }}
+          EVENT_SHA: ${{ github.sha }}
+        run: |
+          test "$(git rev-parse HEAD)" = "$EVENT_SHA"
+          git update-ref "refs/remotes/origin/pull/${PR_NUMBER}/merge" "$EVENT_SHA"
       - uses: leanprover/lean-action@v1
         with:
           build-args: --wfail
-      - uses: leanprover-community/docgen-action@v1
+      - uses: actions/setup-python@v6
+        with:
+          python-version: "3.12"
+      - uses: actions/setup-node@v5
+        with:
+          node-version: "24"
+          cache: npm
+      - name: Install dashboard dependencies
+        run: npm ci
+      - name: Test classification audit contract
+        run: npm run test:python
+      - name: Check dashboard types
+        run: npm run dashboard:check
+      - name: Build dashboard from this revision
+        if: github.event_name == 'pull_request' || github.repository == 'felixpernegger/pibase-lean'
+        run: npm run dashboard:build
+      - name: Verify dashboard artifacts
+        if: github.event_name == 'pull_request' || github.repository == 'felixpernegger/pibase-lean'
+        run: npm run dashboard:verify

.github/workflows/pages.yml

@@ -7,35 +7,47 @@ on:
 
 permissions:
   contents: read
-  pages: write
-  id-token: write
+
+env:
+  PIBASE_DATA_COMMIT: 5c343408ea723e78e31523f9899bfb22580235bd
 
 concurrency:
   group: pages
   cancel-in-progress: true
 
 jobs:
-  build-deploy:
+  build:
     runs-on: ubuntu-latest
-    environment:
-      name: github-pages
-      url: ${{ steps.deployment.outputs.page_url }}
     steps:
       - uses: actions/checkout@v5
-      - name: Check out Felix's Lean source
-        # Full history is used for per-file authorship in the review audit.
-        run: git clone --filter=blob:none --no-tags --branch master https://github.com/felixpernegger/pibase-lean.git "$RUNNER_TEMP/felix-pibase-lean"
-      - name: Check out Felix's pi-base data
-        run: git clone --depth 1 --branch main https://github.com/felixpernegger/pibase-data.git "$RUNNER_TEMP/felix-pibase-data"
-      - uses: actions/setup-python@v5
+        with:
+          # Full history is used for provenance and per-file authorship.
+          fetch-depth: 0
+      - name: Check out pinned pi-base data
+        run: |
+          git init "$RUNNER_TEMP/felix-pibase-data"
+          git -C "$RUNNER_TEMP/felix-pibase-data" remote add origin https://github.com/felixpernegger/pibase-data.git
+          git -C "$RUNNER_TEMP/felix-pibase-data" fetch --depth 1 origin "$PIBASE_DATA_COMMIT"
+          git -C "$RUNNER_TEMP/felix-pibase-data" checkout --detach FETCH_HEAD
+          test "$(git -C "$RUNNER_TEMP/felix-pibase-data" rev-parse HEAD)" = "$PIBASE_DATA_COMMIT"
+      - name: Set up Lean and build the classification audit
+        uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          build: true
+          build-args: --wfail classificationAudit
+          test: false
+          lint: false
+          use-mathlib-cache: true
+      - uses: actions/setup-python@v6
         with:
           python-version: "3.12"
       - name: Refresh the implications payload
         # Felix's deduction engine (build_site.py) produces the payload replayed
         # by the Implications page, so assertions accepted upstream are current
         # at every deploy.
         run: |
-          pip install pyyaml
+          pip install PyYAML==6.0.3
           PYTHONDONTWRITEBYTECODE=1 python3 scripts/fetch_implications.py "$RUNNER_TEMP/felix-pibase-data"
       - uses: actions/setup-node@v5
         with:
@@ -47,15 +59,53 @@ jobs:
         run: npm run dashboard:check
       - name: Build the project dashboard
         run: npm run dashboard:build
-        env:
-          PIBASE_LEAN_SOURCE: ${{ runner.temp }}/felix-pibase-lean
       - name: Verify dashboard artifacts
         run: npm run dashboard:verify
-      - uses: actions/configure-pages@v5
-        with:
-          enablement: true
+      - name: Build API documentation into the project site
+        # docgen-action also deploys Pages on every push. Build its doc-gen4
+        # target here instead so the dashboard and API docs have one publisher.
+        run: |
+          DOC_BUILD_DIR="$RUNNER_TEMP/pibase-docbuild"
+          mkdir -p "$DOC_BUILD_DIR"
+          cat > "$DOC_BUILD_DIR/lakefile.toml" <<EOF
+          name = "docbuild"
+          reservoir = false
+          version = "0.1.0"
+          packagesDir = "$GITHUB_WORKSPACE/.lake/packages"
+
+          [[require]]
+          name = "pibase-lean"
+          path = "$GITHUB_WORKSPACE"
+
+          [[require]]
+          scope = "leanprover"
+          name = "doc-gen4"
+          rev = "$(cut -d: -f2 lean-toolchain)"
+          EOF
+          (
+            cd "$DOC_BUILD_DIR"
+            MATHLIB_NO_CACHE_ON_UPDATE=1 lake update pibase-lean
+            lake build PiBaseLean:docs
+          )
+          test ! -e site/docs
+          cp -R "$DOC_BUILD_DIR/.lake/build/doc" site/docs
+          test -f site/docs/index.html
       - uses: actions/upload-pages-artifact@v3
         with:
           path: site
+
+  deploy:
+    needs: build
+    runs-on: ubuntu-latest
+    permissions:
+      pages: write
+      id-token: write
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    steps:
+      - uses: actions/configure-pages@v5
+        with:
+          enablement: true
       - id: deployment
         uses: actions/deploy-pages@v4

PiBaseLean.lean

@@ -6,7 +6,10 @@ import PiBaseLean.AdditionalDefs.Games
 import PiBaseLean.AdditionalDefs.Meta
 import PiBaseLean.AdditionalDefs.SetTheoryAxioms
 import PiBaseLean.Bundled.Basic
+import PiBaseLean.Bundled.Classification
 import PiBaseLean.Bundled.Defs
+import PiBaseLean.Bundled.SetTheoryVariation
+import PiBaseLean.Goal
 import PiBaseLean.Properties.P1.Bundled
 import PiBaseLean.Properties.P1.Defs
 import PiBaseLean.Properties.P1.Lemmas

PiBaseLean/Bundled/Basic.lean

@@ -99,21 +99,21 @@ instance : CompleteAtomicBooleanAlgebra Property :=
 @[simp]
 theorem compl_toPred (p : Property.{u}) : pᶜ.toPred = p.toPredᶜ := rfl
 
-end PiBase.Formal.Property
-namespace PiBase.Formal
-
-protected theorem Property.le_iff (p q : Property.{u}) :
+/-- Bundled-property order is implication on every topological space. -/
+theorem le_iff (p q : Property.{u}) :
     p ≤ q ↔ (∀ (X : Type u) (_ : TopologicalSpace X), p.toPred X → q.toPred X) := by
   rfl
 
-protected theorem Property.ne_le_iff (p q : Property.{u}) :
+/-- Refuting an implication amounts to exhibiting a topological counterexample. -/
+theorem not_le_iff (p q : Property.{u}) :
     ¬ p ≤ q ↔ (∃ (X : Type u) (_ : TopologicalSpace X), p.toPred X ∧ ¬ q.toPred X) := by
-  simp [Property.le_iff]
+  simp [le_iff]
 
+/-- Two bundled properties are equal when they agree on every topological space. -/
 @[ext]
-protected theorem Property.ext
+theorem ext
     {p q : Property.{u}} (h : ∀ (X : Type u) (_ : TopologicalSpace X), p X ↔ q X) : p = q :=
   le_antisymm
-    ((Property.le_iff p q).mp fun X _ ↦ (h X _).mp) ((Property.le_iff q p).mp fun X _ ↦ (h X _).mpr)
+    ((le_iff p q).mp fun X _ ↦ (h X _).mp) ((le_iff q p).mp fun X _ ↦ (h X _).mpr)
 
-end PiBase.Formal
+end PiBase.Formal.Property

PiBaseLean/Bundled/Classification.lean

@@ -0,0 +1,128 @@
+module
+
+public import PiBaseLean.Bundled.SetTheoryVariation
+
+/-!
+# Auditable implication classifications
+
+This file describes the evidence required to classify a fixed, finite catalogue of bundled
+properties. Property identities are list indices rather than values of `Property`: two catalogue
+entries must remain distinct even when their predicates are extensionally equal.
+
+The status of every pair is an explicit parameter of `ClassificationFor`. In particular, the
+contexts of a conditionally varying implication cannot be selected existentially inside a
+classification proof.
+-/
+
+@[expose] public section
+
+universe u
+
+namespace PiBase.Formal
+
+/-- An ordered pair of distinct entries in a property catalogue. -/
+structure ImplicationPair (properties : List Property.{u}) where
+  source : Fin properties.length
+  target : Fin properties.length
+  distinct : source ≠ target
+  deriving DecidableEq, Fintype
+
+namespace ImplicationPair
+
+/-- The antecedent represented by an indexed implication pair. -/
+def antecedent {properties : List Property.{u}}
+    (pair : ImplicationPair properties) : Property.{u} :=
+  properties[pair.source]
+
+/-- The consequent represented by an indexed implication pair. -/
+def consequent {properties : List Property.{u}}
+    (pair : ImplicationPair properties) : Property.{u} :=
+  properties[pair.target]
+
+/-- The proposition represented by an indexed implication pair. -/
+abbrev statement {properties : List Property.{u}} (pair : ImplicationPair properties) : Prop :=
+  pair.antecedent ≤ pair.consequent
+
+/-- Indexed implication pairs are equivalent to unequal pairs of catalogue positions. -/
+def equivSubtype {properties : List Property.{u}} :
+    ImplicationPair properties ≃
+      {pair : Fin properties.length × Fin properties.length // pair.1 ≠ pair.2} where
+  toFun pair := ⟨(pair.source, pair.target), pair.distinct⟩
+  invFun pair := ⟨pair.1.1, pair.1.2, pair.2⟩
+  left_inv pair := by cases pair; rfl
+  right_inv pair := by cases pair; rfl
+
+/-- The number of ordered pairs of distinct entries in a finite property catalogue. -/
+theorem card (properties : List Property.{u}) :
+    Fintype.card (ImplicationPair properties) =
+      properties.length * properties.length - properties.length := by
+  classical
+  rw [Fintype.card_congr equivSubtype]
+  rw [Fintype.card_subtype]
+  change (Finset.univ.filter fun pair : Fin properties.length × Fin properties.length ↦
+    pair.1 ≠ pair.2).card = _
+  rw [show (Finset.univ.filter fun pair : Fin properties.length × Fin properties.length ↦
+      pair.1 ≠ pair.2) = (Finset.univ : Finset (Fin properties.length)).offDiag by
+    ext pair
+    simp [Finset.mem_offDiag]]
+  rw [Finset.offDiag_card]
+  simp
+
+end ImplicationPair
+
+/-- The existence of a topological space satisfying `p` and refuting `q`. -/
+def HasCounterexample (p q : Property.{u}) : Prop :=
+  ∃ (X : Type u) (topology : TopologicalSpace X),
+    @p.toPred X topology ∧ ¬ @q.toPred X topology
+
+/-- Having a counterexample is equivalent to refuting the universal implication. -/
+theorem hasCounterexample_iff_not_implication (p q : Property.{u}) :
+    HasCounterexample p q ↔ ¬ p ≤ q :=
+  (Property.not_le_iff p q).symm
+
+/-- The three evidence-bearing statuses admitted by the project classification target. -/
+inductive ImplicationStatus
+  /-- The implication has an unconditional Lean proof. -/
+  | proved
+  /-- An existential topological counterexample refutes the implication. -/
+  | refuted
+  /-- The implication and its negation follow under two fixed, named contexts. -/
+  | variesUnder (positiveContext negativeContext : SetTheoryContext)
+  deriving DecidableEq
+
+/-- Evidence required by a status for an implication `p ≤ q`. -/
+def ImplicationStatus.Evidence (status : ImplicationStatus) (p q : Property.{u}) : Prop :=
+  match status with
+  | .proved => p ≤ q
+  | .refuted => HasCounterexample p q
+  | .variesUnder positiveContext negativeContext =>
+      ImplicationVariesUnder p q positiveContext negativeContext
+
+/-- A partial, explicit assignment of statuses to implication pairs. -/
+abbrev ClassificationPlan (properties : List Property.{u}) :=
+  ImplicationPair properties → Option ImplicationStatus
+
+/-- Every status recorded by a plan has the evidence required by that status. -/
+def ClassificationPlan.Sound {properties : List Property.{u}}
+    (plan : ClassificationPlan properties) : Prop :=
+  ∀ pair status, plan pair = some status →
+    status.Evidence pair.antecedent pair.consequent
+
+/-- A plan assigns a status to every implication pair in its catalogue. -/
+def ClassificationPlan.Complete {properties : List Property.{u}}
+    (plan : ClassificationPlan properties) : Prop :=
+  ∀ pair, (plan pair).isSome
+
+/--
+Soundness and completeness of an explicit status plan for a property catalogue.
+
+The `plan` function is deliberately visible in the type. A project-wide certificate should use a
+concrete, reviewable plan; existentially hiding it would permit the same vacuous context selection
+rejected by `SetTheoryVariation`.
+-/
+structure ClassificationFor (properties : List Property.{u})
+    (plan : ClassificationPlan properties) : Prop where
+  sound : plan.Sound
+  complete : plan.Complete
+
+end PiBase.Formal