initial

Author: denisecase

.editorconfig

@@ -0,0 +1,125 @@
+# ============================================================
+# .editorconfig (Keep files consistent across editors and IDEs)
+# ============================================================
+
+# REQ.UNIVERSAL: All professional GitHub project repositories MUST include .editorconfig.
+# WHY: Establish a cross-editor baseline so diffs stay clean and formatting is consistent.
+# ALT: Repository may omit .editorconfig ONLY if formatting is enforced equivalently by CI and formatter tooling.
+# CUSTOM: Adjust indent_size defaults only if organizational standards change; keep stable across projects.
+# NOTE: Sections are ordered by editorial importance, not strict alphabetical order.
+# EditorConfig is documented at https://editorconfig.org
+
+root = true
+
+# === Global defaults (always apply) ===
+
+[*]
+# 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 markup; language-specific overrides follow.
+indent_style = space
+indent_size = 2
+
+
+# === Build systems (special rules) ===
+
+[Makefile]
+# WHY: Makefiles require tabs.
+indent_style = tab
+
+[*.mk]
+# WHY: Makefile includes require tabs.
+indent_style = tab
+
+
+# === Citation and metadata ===
+
+[CITATION.cff]
+# WHY: Citation tooling expects stable YAML formatting.
+indent_size = 2
+indent_style = space
+
+
+# === Markup and documentation ===
+
+[*.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 configuration ===
+
+[*.{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
+
+
+# === Programming languages ===
+
+[*.{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.
+indent_size = 4
+indent_style = space
+
+[*.{sh,bash}]
+# WHY: Shell script convention is 2 spaces.
+indent_size = 2
+indent_style = space
+
+
+# === Proof assistants and formal languages ===
+
+[*.lean]
+# WHY: Lean 4 convention is 2 spaces; matches Mathlib and stdlib style.
+indent_size = 2
+indent_style = space
+
+[*.{v,vo}]
+# WHY: Coq convention is 2 spaces.
+indent_size = 2
+indent_style = space

.gitattributes

@@ -0,0 +1,130 @@
+# ============================================================
+# .gitattributes (Keep files consistent across operating systems)
+# ============================================================
+
+# REQ.UNIVERSAL: All professional GitHub project repositories MUST include .gitattributes.
+# WHY: Ensure consistent line endings, diff behavior, and file classification
+# across Windows, macOS, and Linux environments.
+# ALT: Repository may omit .gitattributes ONLY if equivalent normalization is
+# enforced reliably by tooling and CI (rare and fragile).
+# CUSTOM: Update file-type rules only when introducing new languages,
+# binary artifacts, or documentation formats.
+# NOTE: Rules are ordered by impact and generality, not alphabetically.
+# Git attributes are documented at https://git-scm.com/docs/gitattributes
+
+# === Core defaults (always apply) ===
+
+# WHY: Auto-detect text files and normalize line endings to avoid cross-platform drift.
+* text=auto
+
+
+# === Programming languages and scripts ===
+
+# 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.
+*.md    text eol=lf
+*.tex   text eol=lf
+*.sty   text eol=lf
+*.cls   text eol=lf
+*.bib   text eol=lf
+
+
+# === Configuration and structured 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
+
+
+# === Proof assistants and formal languages ===
+
+# WHY: Lean source 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
+
+# WHY: Lake build directory should be excluded, but if tracked, treat as binary.
+.lake/**  binary
+
+
+# === 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 and 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
+
+
+# === GitHub metadata and UI ===
+
+# WHY: Exclude documentation and tests from GitHub language statistics.
+docs/**    linguist-documentation
+tests/**   linguist-documentation
+
+# === LOG FILES ===
+# WHY: Log files are typically large and binary in nature; prevent text normalization.
+*.log binary
+project.log binary

.github/.yamllint.yml

@@ -0,0 +1,16 @@
+# ============================================================
+# .github/.yamllint.yml (Keep YAML files clean and consistent)
+# ============================================================
+# Updated: 2026-04-13
+
+# WHY: Enforce YAML correctness (.github/.yamllint.yml) without arbitrary style constraints.
+# OBS: Default yamllint rules conflict with GitHub Actions YAML.
+#      Line length, document start, truthy, and comment spacing are intentionally disabled.
+
+extends: default
+
+rules:
+  line-length: disable
+  document-start: disable
+  truthy: disable
+  comments: disable

.github/dependabot.yml

@@ -0,0 +1,24 @@
+# ============================================================
+# .github/dependabot.yml (Check for GitHub Actions updates)
+# ============================================================
+# REQ.PROJECT: This repository SHOULD track GitHub Actions updates automatically.
+# WHY-FILE: GitHub Actions are executable dependencies and may receive security or behavior updates.
+# OBS: Language-level dependencies (e.g., Python packages) are upgraded manually.
+# OBS: GitHub Actions are the only dependency class automated here.
+# ALT: Dependabot could be omitted if workflows are pinned and reviewed manually.
+# CUSTOM: Update interval if CI cadence or security posture changes.
+
+# NOTE: This file automatically updates the versions used in Actions workflows.
+# You don't need to modify this file.
+# To disable: Delete this file or set enabled: false below.
+# enabled: false # Uncomment to disable Dependabot
+
+version: 2 # Dependabot configuration version
+
+updates:
+  - package-ecosystem: "github-actions" # Dependency type
+    directory: "/" # Location of GitHub Actions workflows
+    schedule:
+      interval: "monthly" # ALT: Use "weekly" for higher security when needed
+    commit-message:
+      prefix: "(deps)"  # WHY: enable filtering by commit type

.github/lychee.toml

@@ -0,0 +1,48 @@
+# ============================================================
+# .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.
+# REQ: Link checking MUST be reliable and CI-safe.
+# WHY: Configures Lychee link checker behavior for CI/CD.
+# OBS: Flat structure required by lychee v0.22+; no nested sections.
+# OBS: No path exclusions; all documentation files are expected to be link-clean.
+# OBS: Link integrity preserves stable, reconstructible references over time.
+# OBS: Link integrity maintains connections to external resources.
+
+# WHY: Control verbosity and CI-friendly output
+verbose = "info"   # WHY: Balance between detail and noise
+no_progress = true # WHY: Progress bars don't work well in CI logs
+
+# WHY: Performance tuning for link checking
+max_concurrency = 6 # WHY: Parallel requests without overwhelming servers
+max_retries = 3     # WHY: Retry flaky connections before failing
+retry_wait_time = 8 # WHY: Wait 8 seconds between retries
+timeout = 30        # WHY: 30 seconds per request before timeout
+
+# WHY: Accept common status codes that don't indicate broken links
+# OBS: 403 and 429 reduce false positives
+accept = [
+  200, # OK
+  206, # Partial content
+  301, # Moved permanently
+  302, # Found (temporary redirect)
+  307, # Temporary redirect
+  308, # Permanent redirect
+  403, # Forbidden (often false positive)
+  429, # Too many requests (rate limiting)
+]
+
+# 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
+  "\\.local",        # WHY: Exclude local network domains
+]

.github/workflows/ci-lean.yml

@@ -0,0 +1,42 @@
+# ============================================================
+# .github/workflows/ci-lean.yml (Continuous Integration)
+# ============================================================
+# Updated: 2026-04-28 THEORY VARIANT, ONLY BUILD
+
+name: CI Lean
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  lean:
+    name: Build Lean and export contract
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+
+    steps:
+      # ============================================================
+      # A) ASSEMBLE: Get code and set up Lean
+      # ============================================================
+
+      - name: A1) Checkout repository code
+        uses: actions/checkout@v6
+
+      - name: A2) Set up Lean toolchain
+        uses: leanprover/lean-action@v1
+
+      # ============================================================
+      # B) BUILD: Compile Lean project
+      # ============================================================
+
+      - name: B1) Build Lean project
+        run: lake build
+        # WHY: Compiles the Lean formal contract surface.
+        # OBS: Uses the Lean version declared in lean-toolchain.