From f53ab1578757f7f3812d1c49f655cb215a732b1c Mon Sep 17 00:00:00 2001
From: Brandon Schneider <ceo@sovereign-stack.local>
Date: Wed, 13 May 2026 22:01:12 -0500
Subject: [PATCH] feat: create Lean Expert Agent with full inspection protocol

Agent inspects Lean code for:
1. Structural health (theorem/def/eval/sorry counts)
2. Naming conventions (camelCase/PascalCase per AGENTS.md)
3. Q0_16/Q16_16 compliance
4. Proof quality (native_decide, .isSome guards, tautologies)
5. Dependency analysis (unused imports, circular deps)

First inspection of Physics/ found 95 issues:
  79 naming violations (systematic snake_case)
  2 unused imports (Semantics.FixedPoint)
  4 trivial/tautological proofs
  3 #eval vs #eval! inconsistencies
  1 duplicate theorem
  6 def naming violations (SCALE, absDiff)

Trigger with: /inspect <target>
---
 .../artifacts/lean_expert_agent/AGENTS.md     | 68 +++++++++++++++++++
 1 file changed, 68 insertions(+)
 create mode 100644 shared-data/artifacts/lean_expert_agent/AGENTS.md

diff --git a/shared-data/artifacts/lean_expert_agent/AGENTS.md b/shared-data/artifacts/lean_expert_agent/AGENTS.md
new file mode 100644
index 00000000..08a83420
--- /dev/null
+++ b/shared-data/artifacts/lean_expert_agent/AGENTS.md
@@ -0,0 +1,68 @@
+# Lean Expert Agent — AGENTS.md
+
+## Purpose
+Inspect Lean 4 code for structural integrity, proof correctness, naming conventions, and dependency hygiene. Reports findings as DAG receipts.
+
+## Trigger
+`/inspect <target>` where target is a Lean file, directory, or module name.
+
+## Inspection Protocol
+
+For every file inspected, the agent MUST report:
+
+### 1. Structural Health
+- Count of `theorem` vs `def` vs `#eval` vs `#eval!`
+- Count of `sorry` axioms (⚠️ flag if > 0)
+- Count of `native_decide` proofs vs hand-written proofs
+- Count of empty theorem bodies (`:= by` with no following tactic)
+- Count of tautological theorems (`X = X`, `v ≤ v`)
+- Count of unused imports (import a module without using it)
+- Count of `set_option` linter suppressions
+
+### 2. Naming Conventions (per AGENTS.md §2)
+- File names: `PascalCase.lean` (⚠️ flag if snake_case or kebab-case)
+- Types: `PascalCase` (⚠️ flag if not)
+- Functions: `camelCase` (⚠️ flag if snake_case or PascalCase)
+- Theorems: `camelCase` (⚠️ flag if not)
+- Namespaces: `Semantics.<Domain>` (⚠️ flag if not)
+- Banned: `snake_case` in any file/type name
+- Banned: `getFoo`, `setFoo`, `checkFoo` prefixes
+- Banned: `_v2`, `_final` suffixes
+
+### 3. Q0_16 / Q16_16 Compliance (per AGENTS.md §1.4)
+- Are dimensionless scalars using `Q0_16` (16-bit, pure fraction)?
+- Are mixed quantities using `Q16_16` (32-bit, signed) ONLY when necessary?
+- Is `Float` used in hot-path code? (⚠️ flag if yes)
+- Are Q16_16 operations provably deterministic?
+
+### 4. Proof Quality
+- Does every `def` have a companion `theorem` or `#eval` witness?
+- Do `.get!` calls have companion `.isSome` theorems?
+- Are `native_decide` proofs used when the problem is decidable?
+- Are inductive proofs used when the problem is inductive?
+- Are there unused variables in theorem statements?
+
+### 5. Dependency Analysis
+- Does the file import modules it doesn't use?
+- Does the file use any `sorry` axiom from imported modules?
+- Are there circular dependencies between modules?
+
+## Output Format
+
+```lean
+/- DAG Receipt — Lean Expert Inspection
+   File: <path>
+   Date: <date>
+   Pass: <true/false>
+   Issues: <count>
+-/
+```
+
+Each issue MUST include `file:line` reference, severity (⚠️ ERROR, 🔶 WARNING, ℹ️ INFO), and a concise fix suggestion.
+
+## Agent Resources
+
+- `AGENTS.md` at repo root for naming conventions
+- `6-Documentation/docs/AGENTS.md` for strict operating rules
+- `0-Core-Formalism/lean/Semantics/Semantics/Physics/` for target inspection
+- `lake build` at `0-Core-Formalism/lean/Semantics/` for compilation verification