Research-Stack/.devin/skills/lean-proof/SKILL.md

name	description
lean-proof	Writing, reviewing, and completing Lean 4 proofs and modules in the Research Stack. Use this skill whenever creating or editing .lean files, adding theorems, filling sorries, or auditing a Lean module for quality. Enforces the project's proof quality contract: no tautologies, no unexplained sorries, no floating TODOs without notes.

Lean Proof Skill

This skill governs all Lean 4 authoring and review work in the Research Stack.

Core Rules

1. Double-check every output

After writing or editing any Lean content, re-read the produced definitions and proofs before considering the task done. Verify:

• Types match the stated intent.
• No accidental namespace clash or shadowing.
• #eval witnesses print the expected values (check them against hand-computed expected values in comments).

Run lake build <Module.Name> after every edit. Review the output for errors and for unexpected info: / #eval values that contradict expectations. If the first build pass reveals surprises, fix and rebuild before committing.

2. Sorries must be explained or eliminated

Preferred: complete the proof.

If a sorry cannot be closed immediately:

• Add a structured comment immediately above it explaining why it is deferred:

  -- TODO(lean-port): blocked on missing Mathlib lemma X. Tracked in TODO_MAP.md §A7.
  -- Proof sketch: show Y by induction on Z; use Finset.sum_congr.
  sorry
  

• The comment must state: what is needed, a proof sketch if possible, and where it is tracked.
• A bare sorry with no explanation is not acceptable.

sorry-free is the goal. Every new module should aim for 0 sorries. Use #check, exact?, apply?, omega, simp, decide, norm_num, and Finset / List lemmas from Mathlib before reaching for sorry.

3. TODOs follow the same contract as sorries

A -- TODO(lean-port): ... comment is acceptable only when:

• It names the specific thing that needs to be done.
• It gives a proof sketch or a pointer to where the logic lives in Python/Rust.
• It is tracked in TODO_MAP.md if it affects a blessed Compiler surface module.

Bare -- TODO with no explanation is not acceptable in Lean files.

4. No tautological theorems

Every theorem and lemma must prove something non-trivial. Forbidden patterns:

-- Forbidden: trivially true by rfl
theorem foo : 1 = 1 := by rfl

-- Forbidden: restating a definition with no additional content
theorem bar (x : Nat) : x + 0 = x := Nat.add_zero x   -- only if this adds nothing new

-- Forbidden: wrapper with no proof obligation
theorem baz : True := trivial

A theorem is acceptable only if it:

• Establishes a property of a domain type defined in this project (e.g., alignment scores, density bounds, receipt validity, Q16_16 arithmetic invariants).
• Is used by another definition, downstream theorem, or #eval witness.
• Would not be provable by rfl / trivial alone without domain-specific reasoning.

Acceptable examples:

• Bounds on alignmentScore: ∀ s, alignmentScore s ≤ 100
• Monotonicity: density increases as more axes are hit
• Receipt validity gate: compileRow r |>.receipt.valid ↔ r.alignmentStatus ≠ .missingPrediction

5. Proof must have a purpose

Before writing a theorem, answer:

"What does this proof guarantee about the system's behavior?"

If the answer is "nothing specific beyond what the definition already states by construction," the theorem should not be written. Convert it to a #eval witness or a comment instead.

Proofs that are justified:

• Invariant proofs: the scoring sum stays in [0, 1].
• Gate proofs: a gate only passes when preconditions are met.
• Monotonicity / ordering proofs: more evidence → higher score.
• Receipt proofs: receipt is valid iff alignment passed.

Workflow

1. Read the nearest AGENTS.md before editing any subtree.
2. For new modules in the Compiler surface, check lakefile.toml to see if the module needs to be added to [[lean_lib]] roots.
3. Write the module, including #eval witnesses with expected values in comments.
4. Run lake build <Module>. Fix all errors.
5. Re-read the produced code. Check:
   • Every sorry has an explanation comment.
   • Every theorem has a clear domain purpose.
   • #eval outputs match the expected values stated in comments.
6. If the Compiler surface was touched, run lake build Compiler and confirm the job count matches the baseline in 0-Core-Formalism/lean/Semantics/AGENTS.md.
7. Run python3 -m py_compile on any Python shims updated to add BOUNDARY comments.

Q16_16 Fixed-Point Contract

• No Float in compute paths. ofFloat is only permitted at the external boundary (parsing JSON, reading sensor data) and must be immediately bracketed. In particular: Compiler-surface modules (Semantics.RRC.*, Semantics.AVMIsa.*, Semantics.ReceiptCore) must contain zero ofFloat calls in any definition that feeds into a receipt, score, or gate decision.
• Use Q16_16.ofRatio num den for rational constants.
• Use Q16_16.ofRawInt only when the raw integer is documented with its float equivalent in a comment on the same line: Q16_16.ofRawInt 53739 -- 0.82 * 65536 An undocumented magic integer is a bug.
• Arithmetic inside def bodies: accumulate in raw Int, then call Q16_16.ofRawInt once at the end. Never use native + / * on two Q16_16 values without going through Q16_16.mul / Q16_16.add.

#eval Witness Contract

Every #eval in a Compiler-surface module must carry a -- expect: comment on the same or preceding line stating the expected output:

#eval determineAlignment fixtureClf   -- expect: alignedExact
#eval (emitFixture.totalRows, emitFixture.candidateRows)  -- expect: (6, 3)

• The expected value must be hand-computed or derived from first principles, not copy-pasted from a previous build output.
• After each build, manually confirm the info: lines from lake build match the -- expect: comments. If they diverge, treat it as a failing test.
• #eval blocks without -- expect: comments are not acceptable in new code. Existing ones without comments should be annotated when the file is next touched.

Namespace and Closing Discipline

• Every module must open with namespace Semantics.X.Y and close with end Semantics.X.Y (exact match, including case).
• The closing end must be the last non-blank line of the file.
• open statements are scoped to the namespace block only; do not open at file level outside a namespace (causes leakage into downstream imports).
• To use RRCShape constructors with dot notation, add inside the namespace: open Semantics.RRCLogogramProjection
• DecidableEq RRCShape is derived but BEq RRCShape is not automatically synthesized. Use exhaustive match for shape comparisons, not ==.

Lakefile / Compiler Surface Discipline

• The blessed Compiler target roots are fixed: Semantics.RRC.Emit, Semantics.AVMIsa.Emit, Semantics.RRC.Corpus250
• Do not add new roots to [[lean_lib]] name = "Compiler" without explicit user approval. New modules under Semantics/RRC/ are imported by existing roots, not added as independent Compiler roots.
• After any change to lakefile.toml, run lake build Compiler and verify the job count matches the baseline in 0-Core-Formalism/lean/Semantics/AGENTS.md. A job-count decrease means a module was silently dropped — investigate before committing.

Schema and Claim Boundary Strings

Receipt JSON schemas are versioned strings. Existing values must not be renamed:

Module	Schema string
Semantics.RRC.Emit	"rrc_emit_fixture_v1"
Semantics.AVMIsa.Emit	"avm_canary_emit_v1" / "avm_rrc_corpus250_v1"
Semantics.RRC.ReceiptDensity	"receipt-density-scoring-only; not-a-proof; promotion=not_promoted"

• To add a new schema, use the next version suffix (e.g. _v2) and document the change in ARCHITECTURE.md §7.1.
• claim_boundary strings must end with "admissibility-and-routing-pass-only" or an equivalent explicit limitation. Never use vague strings like "ok" or "verified".

Promotion Gate Invariant

promotion = not_promoted is a hard invariant at this stage of the pipeline. No Lean definition, theorem, or #eval block may set Promotion.candidate on any row without explicit user approval and a corresponding update to TODO_MAP.md.

Violation pattern to reject:

-- Forbidden: silently promoting a row
promotion := .candidate

Axiom / Unsafe / native_decide Prohibition

The following are forbidden in all Compiler-surface modules without explicit sign-off:

• axiom (introducing an unproven assumption)
• unsafe (bypassing the type system)
• native_decide (compiles to native code, bypasses kernel — allowed in test harnesses only, never in blessed Compiler modules)

If you believe one of these is necessary, stop, document the reason in a comment, and flag it to the user before proceeding.

Python Shim BOUNDARY Comment Format

When a Python shim's logic has been ported to Lean, the shim file must be updated with a BOUNDARY block in this exact format, immediately after the docstring:

# BOUNDARY: Python thin IO shim; logic in <Lean.Module.Name>.
#   - python_function_name  → Lean.Module.Name.leanDefinitionName
#   - ...

• One entry per ported function.
• Lean module name must be fully qualified.
• The comment must appear before any import statements that are not part of the original shim header.
• If a file still contains un-ported logic, the BOUNDARY comment must say # PARTIAL BOUNDARY and list both what is ported and what remains.

Reference Files

• Build baseline and Compiler surface: 0-Core-Formalism/lean/Semantics/AGENTS.md
• Lakefile targets: 0-Core-Formalism/lean/Semantics/lakefile.toml
• Q16_16 / Q0_16 primitives: Semantics/FixedPoint.lean
• Receipt infrastructure: Semantics/ReceiptCore.lean
• RRC alignment gate: Semantics/RRC/Emit.lean
• Receipt density scoring: Semantics/RRC/ReceiptDensity.lean
• Logogram projection types: Semantics/RRCLogogramProjection.lean
• Sorry/TODO audit and porting queue: TODO_MAP.md (project root)
• Architecture and output boundary: ARCHITECTURE.md §7.1