Kernel / proof role lab

This role lab is generated from the shared four-stage contract. Page identity, route, prerequisites, first-edit seams, and gates are manifest-owned; prose, checks, the fixture, and additional seams are content-owned.

Prerequisites

• Common journey evidence
• Choose a contributor route
• Current architecture

1. Retrieve and predict

Start from the frozen public claim, not from a tactic guess. Read Bang.subst_value in Bang/Spec.lean, state its claim in plain language, then locate subst_value_proof in Bang/Core/Soundness.lean. Predict the kernel trust result before consulting Audit. Changing the statement or adding a hypothesis is outside this bounded exercise; use the proof-discipline note when you need the rule rather than copying it here.

Retrieve:

• Locate the frozen Bang.subst_value statement in Bang/Spec.lean.
• Locate subst_value_proof in Bang/Core/Soundness.lean and the Bang.subst_value enrollment in Bang/Audit.lean.
• Open docs/notes/spec-proof-discipline.md for the repository proof rules.

Predict before running:

• Explain in plain language what substitution preserves and how the grade changes.
• Predict whether the current Audit result is trusted-three-only or flagged before running the census.
• Predict why changing the frozen statement or adding a hypothesis would evade rather than solve the exercise.

2. Trace the seam

Ownership is explicit: Spec owns the public statement; Soundness owns its proof; tools/check.sh owns the fast local elaboration gate; Audit owns the enrolled repository census. A local #print axioms answers only for the named scratch theorem, while just axioms runs the enrolled Audit census. Its trusted three are propext, Classical.choice, and Quot.sound: they are the maximum permitted dependencies of enrolled theorems, not axioms contributors may add. Source search and the marker-removal grep navigate or check workflow state; neither is proof evidence.

Checks:

• Name the statement owner, implementation owner, fast elaboration gate, and kernel trust evidence owner.
• Explain why a successful file check and an acceptable axiom report establish different facts.
• Use the tactics survey to interpret Lean suggestions without treating a suggested tactic as trusted evidence.

Tracked seams:

• Bang/Spec.lean
• Bang/Core/Semantics.lean
• Bang/Core/Soundness.lean
• Bang/Audit.lean
• docs/notes/spec-proof-discipline.md
• docs/notes/tactics-survey.md
• tools/check.sh

3. Practise in isolation

Create the root-level disposable fixture below; no production file imports it. Predict the nil and cons induction cases, then run direct Lean once and inspect the unique Try this: line produced by exact?. Manually replace only that marker with Lean's current one-line suggestion. Do not copy a stored answer and do not use simp?: the verified rewrite setup is what leaves a deterministic closing suggestion. The displayed grep then checks only that this workflow edit happened; it says nothing about axioms. Only after it passes run the clean check, the scratch theorem's local report, and the enrolled repository census.

Start from the clean, ready checkout used for the common journey. The project helper creates an independent full clone at its exact commit; all writes and gates below happen there.

set -euo pipefail
root="$(git rev-parse --show-toplevel)"
test -z "$(git -C "$root" status --porcelain)"
base="$(git -C "$root" rev-parse HEAD)"
parent="$(mktemp -d)"
lane="$parent/repo"
branch="practice/kernel-proof-$(date +%s)-$$"
"$root/tools/new-worktree.sh" "$lane" "$branch" "$base"
cd "$lane"
practice="$lane/KernelProofLab.lean"
bundle="$parent/evidence"
mkdir "$bundle"
cat > "$practice" <<'BANG'
import Bang.Core.Soundness
 
namespace Bang
namespace GradeVec
 
variable {M : Type}
 
theorem zero_smul_scratch [MulZeroClass M] (γ : GradeVec M) :
    GradeVec.smul 0 γ = GradeVec.zeros γ.length := by
  induction γ with
  | nil => rfl
  | cons a γ ih =>
    rw [smul_cons, zero_mul, List.length_cons, GradeVec.zeros,
      List.replicate_succ, ← GradeVec.zeros]
    exact?
 
#print axioms Bang.GradeVec.zero_smul_scratch
 
end GradeVec
end Bang
BANG

Run every step in order:

nix develop --command lake build Bang.Core.Soundness
nix develop --command lake env lean "$practice" 2>&1 | tee "$bundle/scratch-suggestion.txt"
if grep -Fq 'exact?' "$practice"; then printf '%s\n' 'STOP: replace exact? with Lean current suggestion before continuing.' >&2; false; fi
nix develop --command just check "$practice" 2>&1 | tee "$bundle/scratch-check.txt"
nix develop --command lake env lean "$practice" 2>&1 | tee "$bundle/scratch-axioms.txt"
nix develop --command just test-role-lab-kernel-proof 2>&1 | tee "$bundle/harness.txt"
nix develop --command just axioms 2>&1 | tee "$bundle/audit-axioms.txt"
cp "$practice" "$bundle/KernelProofLab.lean"
rm "$practice"
test -z "$(git status --porcelain)"

Bounded outcome: The disposable theorem closes without sorry, its own kernel report is empty, Bang.subst_value remains within the trusted-three baseline, and no production Lean source or import changes.

4. Inspect evidence and select live work

Keep the completed scratch source and kernel reports as the evidence bundle. Known-bad proofs that compile through sorry or a scratch-only declared axiom must fail because parsed #print axioms output exposes their dependencies, not because their source text was searched. Select live work read-only only after you can name the statement owner, proof owner, and smallest falsifying gate.

Evidence checks:

• Confirm the frozen statement and all production sources are unchanged.
• Confirm the completed scratch source has no suggestion placeholder and differs only at that marker.
• Require exactly one scratch theorem report with an empty axiom set.
• Require compiling sorryAx and unexpected scratch-axiom variants to be rejected from parsed kernel output.
• Require the current Bang.subst_value report to be a subset of the trusted three and contain no sorryAx.
• Record the real narrow and full gate exit statuses; a skipped gate is not a pass.

Narrow gate:

nix develop --command bash -lc 'just check Bang/Core/Soundness.lean && just axioms'

Full gate:

nix develop --command just verify

Read-only issue selection:

Run gh issue list --repo phibkro/bang --state open --search "proof OR soundness OR kernel"; set issue=<candidate-number> and inspect it with gh issue view "$issue" --repo phibkro/bang. Recommend one only after naming its statement owner, proof owner, and smallest falsifying gate; do not claim, comment on, or mutate it.