Preserved: 4 bit-narrowing Agda modules (36d04b5) on preserve/bit-narrowing-agda-2026-09-11, in no CI lane

[hyperpolymath]

What is preserved

Branch preserve/bit-narrowing-agda-2026-09-11 = commit 731f437b6346c3e4286a2e78098c99c04bf88e75 on main (9c4b72b5). Four Agda modules that exist on the unmerged branch chore/apply-foundation-ci-fixes-20260911 (source commit 36d04b5) and nowhere on main:

• proofs/agda/EchoBitNarrowingNumeric.agda (+89)
• proofs/agda/EchoExampleBitNarrowing.agda (+99)
• proofs/agda/EchoExampleTruncation.agda (+84 / −20 vs main)
• proofs/agda/NarrowingSmoke.agda (+31)

None of the four is reachable from All.agda or Smoke.agda, so the green Agda workflow on main says nothing about them. The branch is a plain commit on top of main (no CI files, no splice damage from the chore branch), opened as a branch only, no PR: it is a receipt, not a proposal.

Commit message of the preservation commit:

proofs(agda): preserve the bit-narrowing exhibits from unpushed commit 36d04b5

Four modules from the local 2026-09-11 mixed commit 36d04b5 ("fix(ci): apply
foundation CI/CD security fixes"), which exists on no remote branch. This
commit carries only its Agda content, none of its governance or workflow files.

- EchoExampleTruncation.agda: adds double, halve-double, halve-suc-double,
  echo-halve-even, echo-halve-odd, echo-halve-witnesses-distinct and
  echo-halve-classification-general; the header no longer says "pinned in
  Smoke.agda" (Smoke.agda on main does not import this module).
- EchoExampleBitNarrowing.agda and EchoBitNarrowingNumeric.agda: new.
- NarrowingSmoke.agda: new; imports all three.

All four typecheck locally under --safe --without-K with Agda 2.6.4.3 and
stdlib 2.1-4. None is reached by All.agda, Smoke.agda, characteristic/All.agda
or examples/All.agda, so the existing lanes do not check them; wiring
NarrowingSmoke into a lane and checking it under CI's stdlib v2.3 is the
acceptance criterion of the tracking issue.

Acceptance criteria

1. NarrowingSmoke (which imports the other three) is wired into a lane that CI runs under the stdlib the workflow clones (v2.3), either via Smoke.agda/All.agda or a named experimental lane with the same --safe --without-K flags, or the four modules are explicitly retired here with the reason.
2. The chosen lane is red when one of the four fails to typecheck (verify by a throwaway mutant, then revert).
3. Branch preserve/bit-narrowing-agda-2026-09-11 is deleted only after (1) lands on main.

🤖 Generated with Claude Code

https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57