actions

Author: denisecase

.github/lychee.toml

@@ -1,6 +1,7 @@
 # ============================================================
-# lychee.toml (Lychee link checker configuration)
+# .github/lychee.toml (Lychee link checker configuration)
 # ============================================================
+# Updated: 2026-04-13
 
 # REQ.PROJECT: Automatic link checking using GitHub Actions and Lychee.
 # WHY-FILE: Shared Lychee configuration (lychee.toml) for documentation-heavy repositories.
@@ -32,11 +33,14 @@ accept = [
   308, # Permanent redirect
   403, # Forbidden (often false positive)
   429, # Too many requests (rate limiting)
-  503, # Service unavailable (temporary)
 ]
 
 # WHY: Exclude patterns that shouldn't be checked
 exclude = [
+  "^https://shields\\.io", # WHY: Shields.io badges often have anti-bot measures that cause false positives
+  "^https://img\\.shields\\.io", # WHY: Shields.io image badges often have anti-bot measures that cause false positives
+  "^https://badges\\.github\\.com", # WHY: GitHub badges often have anti-bot measures that cause false positives
+  "^https://www\\.linkedin\\.com", # WHY: LinkedIn often blocks automated requests, causing false positives
   "example\\.com",   # WHY: Exclude example domains in documentation
   "localhost",       # WHY: Exclude local development URLs
   "127\\.0\\.0\\.1", # WHY: Exclude local loopback

.pre-commit-config.yaml

@@ -111,7 +111,7 @@ repos:
       - id: se-validate-manifest
         name: E2) Validate SE manifest against schema
         language: system
-        entry: uvx --from se-manifest-schema se-manifest validate-manifest --strict
+        entry: uvx --python 3.14 --from se-manifest-schema se-manifest validate-manifest --strict
         pass_filenames: false
         always_run: true
 

README.md

@@ -48,12 +48,6 @@ lake build
 lake exe verify
 ```
 
-## Optional Markdown Lint
-
-```shell
-npx markdownlint-cli2 --fix
-```
-
 ## Documentation
 
 - [Paper to Lean Mapping](./docs/MAPPING.md)

docs/LEAN.md

@@ -83,12 +83,12 @@ Tactics are commands used inside `by` blocks to construct proofs.
 
 ## Latin/Logic Terms
 
-| Term      | Origin                      | Meaning                                            |
-| --------- | --------------------------- | -------------------------------------------------- |
-| `exfalso` | Latin: "ex falso quodlibet" | From falsehood, anything follows.                  |
-| `rfl`     | "reflexivity"               | Something equals itself.                           |
-| `mp`      | "modus ponens"              | Forward direction of iff (`P ↔ Q` gives `P → Q`).  |
-| `mpr`     | "modus ponens reverse"      | Backward direction of iff (`P ↔ Q` gives `Q → P`). |
+| Term      | Origin                 | Meaning                                            |
+| --------- | ---------------------- | -------------------------------------------------- |
+| `exfalso` | Latin: "ex quodlibet"  | From falsehood, anything follows.                  |
+| `rfl`     | "reflexivity"          | Something equals itself.                           |
+| `mp`      | "modus ponens"         | Forward direction of iff (`P ↔ Q` gives `P → Q`).  |
+| `mpr`     | "modus ponens reverse" | Backward direction of iff (`P ↔ Q` gives `Q → P`). |
 
 ---