Design note: InterfaceSummary + declared↔use arity family (one membrane: typecheck boundary, cache key, proof cut, seam basis, liveness root)

[briansrls]

Design note (docs-only): one artifact and one rule reconciling three converging lanes — the resolver's closure-denominated quadratic, the witness quadratic behind the CI opt-in inversion (#6232), and the unused/inert detection family.

Claims:

• InterfaceSummary — a derived, content-addressed summary of a module's exported surface — is one authority with five consumers: typecheck-against-summary boundary (S2a/S2b; the reintroduction wall structural-quadratic-wall-coverage-audit.md names as its only on-dial increment), Merkle key component / early cutoff (S2b + determinism §5 determinism mechanism P1: core axis, roster, compose algebra, witnesses #5941), Hoare proof cut for span-witness factorization, the shared seam basis that collapses the O(n²) span space onto O(n) segment witnesses, and the module-scale liveness root set.
• The declared↔use arity family (unused import / missing import / unused variable / inert module / inert lens) is ONE reachability rule over scoped root sets, homed on the existing inert-layer-lens engine (not forked). The import row is done by construction — import block as a projection of body use, enabled by the Constructor-owner ruling (§1c): binding-edge resolution, collision wall, scan deleted — the engine PR #6235 binding-edge ruling — so unused AND missing are unwritable at once; under-consumption stays out (Rice → redundancy lens, per inert-layer §1.1).
• Every deliverable folds into an existing lane; explicit non-goals: no second reachability engine, no new complexity oracle, no runtime span-aggregator, no thresholded selection arms.

Flags needing operator sign (§6): A — import-projection transport (recommend canonicalizer-first, wall later) · B — summary grain (recommend per-declaration + module rollup) · C — span/seam fact timing (recommend: rides the witness kind-modeling PR, advisory factorability) · D — contract slot v0 (signature-only; semantic cut-formulas ground seam-by-seam, typed-absent until then).

Draft-until-signed: stays draft until the flags carry a sign.

🤖 Generated with Claude Code

[gunbai-bot]

CI red @ 157d89f is infra-class, not the diff: the ci job hit the 10-minute timeout during the Rust build step (cold/degraded sccache path, CARGO_BUILD_JOBS=1 — still at 'Compiling v1-compiler' 8.5 min in; canceled before the floor pass started). The diff is a single docs/plans markdown file with no influence on the build. rust_tests passed (9m18s) on the same pool. Re-ran the failed job to land on a warm cache. — sent from gentle-owl-459