§0 construction-justification rule (authoring-time): every lens records why its class can't be construction

[gunbai-bot]

What

ROADMAP §0 meta-item — the authoring-time construction-justification rule (DESIGN §5/§6), layered on top of the #5433 inert-lens backstop (it does not supersede it).

DESIGN §6: a lens is validation — it concedes the bad state is writable. So before adding a lens you must justify why the class can't be made unwritable by construction. This PR makes that judgment a recorded, fail-closed requirement.

Shape (the §7 recursion — construction applied to the rule itself)

The judgment (which §5 class + why) is unstructurable human residue. The requirement to have recorded one is structurable — so the missing-justification state is made unwritable:

• v2.lens.common.construction_justification — single-authority typed model: ConstructionClass = WallNow | WallAfterGrounding | RatchetForever (DESIGN §5's three buckets, reusing the expressibility-frontier §2 region names — not a parallel taxonomy) + ConstructionJustification { class, rationale }.
• All 35 top-level v2.lens.* modules now carry a data construction_justification: ConstructionJustification = … decl — the mark on the carrier (§3/§6), classified from each lens's existing header. Mirrors the extdeps_external_authority_anchor precedent.
• Fail-closed presence check in discover_floor_corpus_rows (sibling to the Lens hygiene: import-closure inert-lens backstop + promote 5 inert lenses to floor-discovered witnesses (§0) #5433 inert check; reuses is_top_level_lens_module so the two cover the same set). A top-level lens with no recorded justification fails the floor closed.

Why this layers on #5433, not over it

• Lens hygiene: import-closure inert-lens backstop + promote 5 inert lenses to floor-discovered witnesses (§0) #5433 backstop: is this lens wired? (runs over the corpus — the floor guarantee).
• This rule: should this be a lens at all, and why? (records the authoring-time judgment).

A judgment applied at authoring time executes nothing, so it can't replace a corpus check. Both run in floor discovery; neither subsumes the other.

Verification (green-by-execution)

• cargo test -p v1-compiler --lib construction_justification_hygiene_tests (3 tests: scan predicate, discriminating detector RED-on-missing/GREEN-on-recorded, whole-corpus green) + inert backstop tests still green.
• .dag resolution confirmed end-to-end by running real witnesses across all three variants: discrimination (WallAfterGrounding), cost (WallNow), synthesis (RatchetForever) — all resolved 32 sources → true.
• cargo fmt --all --check + cargo clippy -p v1-compiler --lib -- -D warnings clean.

Residue / follow-on (honest)

• The correctness of each recorded class is review, not gated (deciding decidability is itself ③).
• Modules recorded WallNow (cost, application_serializer) + support module affected_set_examples flag a §3 home question (computations/support filed under v2.lens.*); relocating them touches module resolution → marked follow-up.

Plan: docs/plans/construction-justification-rule.md.

🤖 Generated with Claude Code