plan: scope the axiom + syllogism lens — argument as the fourth reachability substrate (SCOPE-ONLY)

[briansrls]

SCOPE-ONLY design for the next expressibility-frontier instance: the axiom + syllogism lens (DESIGN open thread #1, ROADMAP §0). Builds nothing — adds docs/plans/axiom-syllogism-lens.md + its ROADMAP inbound link, for the parent review → operator build-nod.

What it delivers (the four asks)

1. Frontier partition of syllogism-enforcement (per docs/plans/expressibility-frontier.md):

   • ① wall — the argument is a rooted DAG: no orphan (reachability to the axiom set), no cycle (graph_has_multi_node_scc — the §4 acyclicity test turned on the argument itself), closed axiom set (no smuggled premise). Decidable graph facts; unwritable once claims are substrate nodes.
   • ② lens-residue — the prose↔model binding seam (a determined-fix reader; presents the missing premise, never picks).
   • ③ undecidable-review — inference soundness, argument completeness, axiom independence. Refusing to sell soundness as a wall is the §5 "never"-trap guard (③ priced as ① is the failure mode).

2. The .dag model — Axiom/Claim/Argument carriers that reuse std/graph.dag (cycle detection, DFS, adjacency) + std/logic.dag (syllogistic Classical) + std/induction.dag; the DESIGN §1–§7 chain transcribed as rows. No fork: this is the inert-layer-lens.md §8 reachability rule's fourth substrate (code · docs · lenses · argument), not a second reachability authority.

3. First target = DESIGN.md itself (the §7 recursion) — the doc checks its own serial structure is a real consequence-chain, with discriminating RED-on-revert witnesses (delete a because edge → orphan RED; add a forward edge → cycle RED; add a fourth root → smuggled-axiom RED; empty argument → non-vacuity RED).

4. Vertical slice — three carriers + a §1-only instance + one witness file, pure .dag, no host bridge (the argument's universe is the declared row set, so it's strictly cheaper than the doc-graph wall §0 reachability-completeness lens: doc-graph instance as first gating wall (generalize #5433, no fork); see docs/plans/inert-layer-lens.md §8 #5484). The smallest nod-able artifact that proves the wall on real claims.

Open questions flagged for the nod

Row authority (transcribed vs derived-from-prose), claim granularity, the independent-peer node kind (§1 allows peers, not only consequences — the one unsettled modeling decision), and first-target order (§1-only first vs whole chain).

Honors the doc-reachability wall (#5484): new docs/plans/X.md ships with its inbound link in the same PR.

🤖 Generated with Claude Code