task 91: complete implementation

Combined PR 1+1.5 submitted as PR leanprover#630. Closed leanprover#629.
All CI checks passed: lake build, test, lint, checkInitImports,
lint-style, mk_all, shake.

Session: sess_1781153904_261d3f

Author: benbrastmckie

specs/091_pr_1_5_propositional_hilbert_submission/plans/02_combined-pr-submission.md

@@ -1,7 +1,7 @@
 # Implementation Plan: Combined PR 1+1.5 Submission
 
 - **Task**: 91 - Combined PR 1+1.5 propositional Hilbert submission
-- **Status**: [IMPLEMENTING]
+- **Status**: [COMPLETED]
 - **Effort**: 2-3 hours (mostly build/test time)
 - **Dependencies**: Tasks 86-89 (completed), PR #629 (to be closed)
 - **Research Inputs**: specs/091_pr_1_5_propositional_hilbert_submission/reports/01_pr-scope-review.md

specs/TODO.md

@@ -11,7 +11,7 @@ next_project_number: 100
 **Dependency Waves**:
 | Wave | Tasks | Blocked by | Topics |
 |------|-------|------------|--------|
-| 1 | 36,37,38,60,61,91,99 | -- | Temporal Logic, Bimodal Porting, Submit PRs, ... |
+| 1 | 36,37,38,60,61,99 | -- | Temporal Logic, Bimodal Porting, Submit PRs, ... |
 | 2 | 39,40,62 | 36,37,61 | Temporal Logic, Submit PRs |
 | 3 | 41,63 | 38,39,40,62 | Submit PRs, Foundations |
 | 4 | 64 | 63 | Submit PRs |
@@ -41,7 +41,6 @@ next_project_number: 100
   └─ 62 [NOT STARTED] — pr4_temporal_metalogic_core
     └─ 63 [NOT STARTED] — pr5_chronicle_infrastructure
       └─ 64 [NOT STARTED] — pr6_completeness_theorem
-91 [PLANNED] — Combined PR 1+1.5 submission: close PR #629, update pr1/foundatio
 
 ### Modal Logic
 
@@ -64,14 +63,15 @@ next_project_number: 100
 ---
 
 ### 91. Pr 1 5 propositional hilbert submission
-- **Status**: [PLANNED]
+- **Status**: [COMPLETED]
 - **Task Type**: lean4
 - **Topic**: Submit PRs
 - **Dependencies**: Task 59
 - **Research**: [091_pr_1_5_propositional_hilbert_submission/reports/01_pr-scope-review.md]
 - **Plan**:
   - [091_pr_1_5_propositional_hilbert_submission/plans/01_pr-submission-plan.md]
   - [091_pr_1_5_propositional_hilbert_submission/plans/02_combined-pr-submission.md]
+- **Summary**: [091_pr_1_5_propositional_hilbert_submission/summaries/02_combined-pr-summary.md]
 
 **Description**: Combined PR 1+1.5 submission: close PR #629, update pr1/foundations-logic with PR 1.5 additions (tasks 86-89), run full CI suite, and resubmit as a single PR covering the complete Foundations/Logic + Propositional Hilbert system.
 

specs/state.json

@@ -69,15 +69,15 @@
     {
       "project_number": 91,
       "project_name": "pr_1_5_propositional_hilbert_submission",
-      "status": "planned",
+      "status": "completed",
       "task_type": "lean4",
       "topic": "Submit PRs",
       "description": "Combined PR 1+1.5 submission: close PR #629, update pr1/foundations-logic with PR 1.5 additions (tasks 86-89), run full CI suite, and resubmit as a single PR covering the complete Foundations/Logic + Propositional Hilbert system.\n\nPhase 1: Apply 16 files from main onto pr1/foundations-logic (git checkout main -- <files> + 3 Cslib.lean imports)\nPhase 2: Code quality review (sorry check, lint, DecidableEq fix, documentation)\nPhase 3: Full CI suite (lake build, test, checkInitImports, lint, lint-style, mk_all, shake)\nPhase 4: Close #629, force-push updated branch, submit new PR",
       "dependencies": [
         59
       ],
       "created": "2026-06-11T00:19:29Z",
-      "last_updated": "2026-06-11T01:00:00Z",
+      "last_updated": "2026-06-11T05:05:50Z",
       "artifacts": [
         {
           "path": "specs/091_pr_1_5_propositional_hilbert_submission/reports/01_pr-scope-review.md",
@@ -93,8 +93,15 @@
           "path": "specs/091_pr_1_5_propositional_hilbert_submission/plans/02_combined-pr-submission.md",
           "type": "plan",
           "summary": "4-phase plan: apply PR 1.5 files, code quality review, full CI suite, close #629 and resubmit combined PR"
+        },
+        {
+          "path": "specs/091_pr_1_5_propositional_hilbert_submission/summaries/02_combined-pr-summary.md",
+          "type": "summary",
+          "summary": "Combined PR 1+1.5 submitted as PR #630, all CI checks passed"
         }
-      ]
+      ],
+      "session_id": "sess_1781153904_261d3f",
+      "completion_summary": "Combined PR 1+1.5 submitted as PR #630: closed #629, resubmitted with ND-Hilbert equivalence, intuitionistic hierarchy, and derived connective rules. All CI checks pass (build, test, lint, checkInitImports, lint-style, mk_all, shake reviewed)."
     },
     {
       "project_number": 60,