roadmap: Dedukti bridge real (Stage 6b — λΠ modulo as lingua franca)

[hyperpolymath]

Origin

docs/ROADMAP.md Stage 6 ("Cross-prover semantics — translation actually works"), row 6b:

    6b  Dedukti bridge real                 λΠ modulo as lingua franca

Stage 6 is Q3-Q4 2026. Per the long-tail enumeration this is ~12 PRs of work.

Scope

Real Dedukti .dk emitter + ingester at src/rust/exchange/:

• Encode ECHIDNA core::Term into λΠ modulo (rewrite rules + dependent function types)
• Parse .dk files into core::Term
• Round-trip tests against the Dedukti standard distribution (Logipedia exports)
• Conformance against Dedukti CI

Estimated ~12 PRs (per long-tail roadmap enumeration).

Dependencies

• Stage 5 (Cap'n Proto IPC + Chapel + Tier-4 CI) — same as Stage 6a
• OpenTheory bridge (roadmap: OpenTheory bridge real (Stage 6a — bidirectional term translation) #190) is a sibling; the two are independent technically but share the exchange/ crate's shape

Why filed

To make the ROADMAP.md Stage 6b commitment trackable; today it lives only as a single ASCII-art row with no issue, no milestone, no owner. λΠ modulo is the more expressive of the two cross-prover lingua francas and is the harder of the two implementations — deserves a visible separate tracker.