Add feature-indexed Agda conformance and capability expansion harness

[chboishabba]

What changed

• adds Agda2Lean.Support, a deterministic feature-indexed survey over canonical ModuleIR
• reports module imports, declaration- and term-level builtins, IR forms, declaration roles, features, mapping modes, reconstruction points and extension boundaries
• adds the agda2lean-support CLI for deterministic TSV support reports
• classifies outcomes using the stable public states:
  • supported-correspondence
  • reconstruction-boundary
  • deliberately-unsupported
  • unclassified
• detects unsupported standard builtin families and reflection/cubical/size/coinduction/IO surfaces from elaborated imports before those families receive semantic BuiltinIds
• adds a 19-case staged Agda corpus covering structural modules, computation, standard builtin families and semantic boundaries
• adds a machine-readable manifest and capability expansion ledger
• forbids promotion to supported-correspondence without a concrete Lean oracle
• adds unit regressions for registered builtins, reconstruction, deliberate cubical rejection, honest eliminator classification and deterministic TSV rendering
• adds corpus, manifest-policy and support-matrix scripts
• documents capability promotion gates, evidence layers and quantitative confidence metrics

Important semantic boundary

This PR does not pretend that adding a fixture implements cubical, reflection, sizes, coinduction, IO or arbitrary clause translation. Those remain deliberately unsupported until their own reviewed IR and lowering designs exist. The new harness makes each missing vertical slice explicit and prevents accidental acceptance or unsupported-feature confidence inflation.

Declared corpus state

• 19 of 19 cases classified
• 11 reconstruction-boundary cases
• 8 deliberately-unsupported cases
• 0 supported-correspondence cases until Lean oracles are added

Validation

No GitHub Actions run was requested or triggered because project Actions quota is constrained. The branch was reviewed structurally through the GitHub connector, but the new Cabal test suite and pinned Agda corpus runner still need execution in the local pinned environment before this PR should be marked ready.

[coderabbitai]

Important

Review skipped

Draft detected.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro Plus

Run ID: 95933738-b935-4df5-be07-2e646bcdc220

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch agent/feature-conformance-and-capability-expansion

---

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.}