initial

Author: denisecase

.editorconfig

@@ -0,0 +1,104 @@
+# REQ.UNIVERSAL: All professional GitHub project repositories MUST include .editorconfig.
+# WHY: Establish a cross-editor baseline (VS Code, PyCharm, Vim, etc.) so diffs stay clean and formatting is consistent.
+# ALT: Repository may omit .editorconfig ONLY if formatting is enforced equivalently by CI + formatter tooling for all contributors or solo projects.
+# CUSTOM: Adjust indent_size defaults only if organizational standards change; keep stable across projects.
+
+root = true
+
+[*]
+# WHY: Normalize line endings and encoding across Windows, macOS, and Linux.
+end_of_line = lf
+charset = utf-8
+
+# WHY: Newline at EOF avoids noisy diffs and tool warnings.
+insert_final_newline = true
+
+# WHY: Remove accidental whitespace noise in diffs.
+trim_trailing_whitespace = true
+
+# WHY: Default to 2 spaces for configs and many markup files; language-specific overrides follow.
+indent_style = space
+indent_size = 2
+
+# === Markup ===
+
+[*.md]
+# WHY: Keep Markdown clean; use explicit <br> for hard line breaks.
+indent_size = 2
+trim_trailing_whitespace = true
+
+[*.{tex,cls,sty}]
+# WHY: LaTeX convention is 2 spaces.
+indent_size = 2
+indent_style = space
+
+[*.xml]
+# WHY: XML convention is 2 spaces.
+indent_size = 2
+indent_style = space
+
+[*.{yml,yaml}]
+# WHY: YAML convention is 2 spaces.
+indent_size = 2
+indent_style = space
+
+# === Data and config ===
+
+[*.{json,jsonc,jsonl,ndjson}]
+# WHY: JSON tooling typically expects 2 spaces.
+indent_size = 2
+indent_style = space
+
+[*.toml]
+# WHY: TOML often follows 4-space indentation in many projects.
+indent_size = 4
+indent_style = space
+
+# === Code ===
+
+[*.{js,ts}]
+# WHY: JS/TS ecosystem commonly uses 2 spaces.
+indent_size = 2
+indent_style = space
+
+[*.{py,pyi}]
+# WHY: Python convention is 4 spaces.
+indent_size = 4
+indent_style = space
+
+[*.ps1]
+# WHY: PowerShell convention is 4 spaces.
+indent_size = 4
+indent_style = space
+
+[*.{c,cpp,h,java,cs,go,rs}]
+# WHY: Many C-family and systems languages commonly use 4 spaces (project-dependent).
+indent_size = 4
+indent_style = space
+
+[*.{sh,bash}]
+# WHY: Shell script convention is 2 spaces.
+indent_size = 2
+indent_style = space
+
+# === Proof Assistants ===
+
+[*.lean]
+# WHY: Lean 4 convention is 2 spaces; matches Mathlib and standard library style.
+indent_size = 2
+indent_style = space
+
+[*.{v,vo}]
+# WHY: Coq convention is 2 spaces.
+indent_size = 2
+indent_style = space
+
+# === Build System ===
+
+[Makefile]
+# WHY: Makefiles require tabs.
+indent_style = tab
+
+[*.mk]
+# WHY: Makefile includes require tabs.
+indent_style = tab

.gitattributes

@@ -0,0 +1,117 @@
+# REQ.UNIVERSAL: All professional GitHub project repositories MUST include .gitattributes.
+# WHY: Ensure consistent line endings, diff behavior, and repository metadata
+#      across Windows, macOS, and Linux.
+# ALT: Repository may omit .gitattributes ONLY if equivalent normalization is
+#      enforced by tooling and CI (rare and fragile).
+# CUSTOM: Update file-type rules only when introducing new languages or artifact types.
+
+# WHY: Auto-detect text files and normalize line endings to avoid cross-platform drift.
+* text=auto
+
+
+# === Source Code ===
+
+# WHY: Python and shell scripts must use LF for CI/CD, Linux environments, and containers.
+*.py    text eol=lf
+*.sh    text eol=lf
+
+# WHY: PowerShell convention on Windows uses CRLF.
+*.ps1   text eol=crlf
+
+
+# === Markup and Documentation ===
+
+# WHY: Documentation and markup files use LF; standard for cross-platform tooling.
+*.bib   text eol=lf
+*.cls   text eol=lf
+*.md    text eol=lf
+*.sty   text eol=lf
+*.tex   text eol=lf
+
+
+# === Configuration and Data (Text) ===
+
+# WHY: Configuration and structured text formats use LF for stable diffs.
+*.json     text eol=lf
+*.jsonc   text eol=lf
+*.jsonl   text eol=lf
+*.ndjson  text eol=lf
+*.toml    text eol=lf
+*.yaml    text eol=lf
+*.yml     text eol=lf
+
+
+# === GitHub Metadata ===
+
+# WHY: Exclude documentation and tests from GitHub language statistics.
+docs/**   linguist-documentation
+tests/**  linguist-documentation
+
+
+# === Notebooks ===
+
+# WHY: Jupyter notebooks require specialized diff and merge handling.
+*.ipynb   diff=jupyternotebook
+*.ipynb   merge=jupyternotebook
+
+
+# === Databases (Binary) ===
+
+# WHY: Database files are binary; prevent text normalization and meaningless diffs.
+*.db       binary
+*.duckdb   binary
+*.sqlite   binary
+*.sqlite3  binary
+
+# === Columnar / Analytical Data (Binary) ===
+
+# WHY: Columnar and analytical data formats are binary; diffs are not meaningful.
+*.arrow    binary
+*.avro     binary
+*.feather  binary
+*.orc      binary
+*.parquet  binary
+
+
+# === Office, BI, PDFs, and Compressed Artifacts (Binary) ===
+
+# WHY: Office documents, BI files, PDFs, and compressed artifacts are binary.
+*.7z     binary
+*.bz2    binary
+*.docx   binary
+*.gz     binary
+*.pbix   binary
+*.pbit   binary
+*.pdf    binary
+*.pptx   binary
+*.rar    binary
+*.tar    binary
+*.tgz    binary
+*.xls    binary
+*.xlsm   binary
+*.xlsx   binary
+*.xz     binary
+*.zip    binary
+
+
+# === Proof Assistants ===
+
+# WHY: Lean files must use LF for cross-platform consistency and CI.
+*.lean   text eol=lf
+
+# WHY: Lean build artifacts are binary; prevent normalization and meaningless diffs.
+*.olean  binary
+*.ilean  binary
+*.trace  binary
+
+# WHY: Coq source uses LF; compiled objects are binary.
+*.v      text eol=lf
+*.vo     binary
+*.vok    binary
+*.vos    binary
+*.glob   binary
+
+# === Lean Build System ===
+
+# WHY: Lake build directory should be excluded but if tracked, treat as binary.
+.lake/**  binary

.github/dependabot.yml

@@ -0,0 +1,13 @@
+# WHY: Automatically updates GitHub Actions to latest versions
+# OBS: Runs monthly to keep actions secure and up-to-date
+# REQ: Keep this file to maintain security patches in workflows
+
+version: 2
+
+updates:
+  - package-ecosystem: "github-actions" # WHY: Updates action versions in workflows
+    directory: "/" # WHY: Scan all .github/workflows/*.yml files
+    schedule:
+      interval: "monthly" # WHY: Monthly updates balance freshness vs notification noise
+    commit-message:
+      prefix: "ci(deps)" # WHY: Conventional commit format for changelog tools

.github/workflows/ci.yml

@@ -0,0 +1,16 @@
+# REQ: Verify Lean proofs compile on every push and PR.
+# WHY: Proofs are the deliverable; broken proofs must not merge.
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v6 # OBS: v6 current as of Dec 2025
+      - uses: leanprover/lean-action@v1

.github/workflows/lean_action_ci.yml

@@ -0,0 +1,98 @@
+# WHY: Automated link checking - behavior controlled by repo variable
+# OBS: Set IS_ACTIVE_REPO=true in GitHub Repository Settings > Secrets and variables > Actions > Variables
+# ALT: Default (no variable set) runs manual only - perfect for student repos
+
+name: Check Links
+
+on:
+  workflow_dispatch: # WHY: Manual trigger - always available
+
+  schedule:
+    - cron: "0 6 1 * *" # WHY: Runs monthly (1st of month) if IS_ACTIVE_REPO=true
+
+  pull_request: # WHY: Validates PR links if IS_ACTIVE_REPO=true
+
+# WHY: Prevent multiple simultaneous link checks on same ref
+concurrency:
+  group: link-check-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  lychee:
+    # WHY: Skip scheduled/PR runs unless IS_ACTIVE_REPO=true or manual trigger
+    # OBS: vars.IS_ACTIVE_REPO linted as error in VS Code but works on GitHub
+    if: github.event_name == 'workflow_dispatch' || vars.IS_ACTIVE_REPO == 'true'
+
+    runs-on: ubuntu-latest
+
+    # WHY: Permissions needed for PR comments and issue creation
+    permissions:
+      contents: read
+      issues: write
+      pull-requests: write
+
+    steps:
+      - uses: actions/checkout@v6 # OBS: v6 current as of Dec 2025
+
+      # WHY: Check all documentation and config files for broken links
+      - name: Check links with Lychee
+        uses: lycheeverse/lychee-action@v2 # OBS: v2 current as of Dec 2025
+        with:
+          args: >
+            --verbose
+            --no-progress
+            --user-agent "${{ github.repository }}/lychee"
+            './**/*.bib'
+            './**/*.md'
+            './**/*.html'
+            './**/*.tex'
+            './**/*.yml'
+            './**/*.yaml'
+          lycheeVersion: latest # OBS: Always use latest lychee release
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      # WHY: Provide helpful feedback on PRs with broken links
+      - name: Comment on PR if links broken
+        if: failure() && github.event_name == 'pull_request'
+        uses: actions/github-script@v8 # OBS: v8 current as of Dec 2025
+        with:
+          script: |
+            const comment = `## Link Check Results
+
+            Some links appear broken. Check the [workflow logs](${context.payload.repository.html_url}/actions/runs/${context.runId}) for details.`;
+
+            github.rest.issues.createComment({
+              issue_number: context.issue.number,
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              body: comment
+            });
+
+      # WHY: Track broken links found during scheduled checks
+      # OBS: Only creates issue if none already open with 'broken-links' label
+      - name: Create issue for scheduled failures
+        if: failure() && github.event_name == 'schedule'
+        uses: actions/github-script@v8 # OBS: v8 current as of Dec 2025
+        with:
+          script: |
+            const title = `Link Check Failed - ${new Date().toISOString().split('T')[0]}`;
+            const body = `Weekly link check found broken links. [Check logs](${context.payload.repository.html_url}/actions/runs/${context.runId})`;
+
+            // WHY: Avoid duplicate issues
+            const existing = await github.rest.issues.listForRepo({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              labels: 'broken-links',
+              state: 'open'
+            });
+
+            if (existing.data.length === 0) {
+              await github.rest.issues.create({
+                owner: context.repo.owner,
+                repo: context.repo.repo,
+                title: title,
+                body: body,
+                labels: ['maintenance', 'broken-links']
+              });
+            }

.github/workflows/links.yml

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2025 Denise M. Case
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.