proofs(agda): preserve the bit-narrowing exhibits from unpushed commi…

[hyperpolymath]

…t 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.

Claude-Session: https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57

Summary

Closes #

Type of change

• 🐛 Bug fix (non-breaking change that fixes an issue)
• ✨ New feature (non-breaking change that adds functionality)
• 💥 Breaking change (would change existing behaviour)
• 🕳️ Soundness fix (fixes a checker/proof false-negative)
• 📖 Documentation
• 🧹 Refactor / tech debt (behaviour-preserving)
• ⚡ Performance
• 🔧 Build / CI / tooling

How has this been verified?

Checklist

• My commits are signed (git commit -S).
• I ran the project's own checks/tests locally and they pass.
• New files carry the correct SPDX-License-Identifier (code/config MPL-2.0,
  prose CC-BY-SA-4.0); I did not relicense existing files.
• Docs are updated, and no public claim now overstates what the code does.
• I have not introduced a soundness hole (or I have flagged where I might have).

Notes for reviewers

[coderabbitai]

Navigate logical layers of code changes, visualize relationships, and explore their blast radius.

Note

Currently processing new changes in this PR. This may take a few minutes, please wait...

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: 6c6190fc-a97c-4dc0-be80-d3c25f8e2d03

📥 Commits

Reviewing files that changed from the base of the PR and between 9c4b72b and 731f437.

📒 Files selected for processing (4)

• proofs/agda/EchoBitNarrowingNumeric.agda
• proofs/agda/EchoExampleBitNarrowing.agda
• proofs/agda/EchoExampleTruncation.agda
• proofs/agda/NarrowingSmoke.agda

 _________________________________________
< Code review: now with 100% more rabbit. >
 -----------------------------------------
  \
   \   \
        \ /\
        ( )
      .( o ).

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}