@@ -3,7 +3,7 @@
 # Clang is the authority for ordinary C++ semantics: parsing, name lookup,
 # overload resolution, conversions and target layout. This target translates
 # the facts C++L needs into C++L's own typed representation, and is the only
-# place in the project that includes a Clang header (ARCHITECTURE.md 12,
+# place in the project that includes a Clang header (ARCHITECTURE.md 11,
 # AGENTS.md 14).
 add_library(cppl_clang STATIC
     src/bridge.cpp)
 
@@ -18,7 +18,7 @@ namespace cppl::clangbridge {
 // Everything here is a *resolved* fact: types are canonical, calls name the
 // overload Clang selected, and references name the declaration Clang bound.
 // Nothing in this layer is recovered from source text, and no Clang data
-// structure or pointer escapes it (ARCHITECTURE.md 12).
+// structure or pointer escapes it (ARCHITECTURE.md 11).
 
 enum class TypeKind : std::uint8_t {
     Int,
 
@@ -3,14 +3,14 @@
 # `source` is added by the top-level CMakeLists because the VIR and the Clang
 # bridge depend on it and are configured before this directory.
 #
-# Dependency direction (ARCHITECTURE.md 44):
+# Dependency direction (ARCHITECTURE.md 95):
 #
 #   driver -> frontend / clang bridge -> elaboration -> vir
 #          -> obligations -> automation -> kernel
 #
 # `decomposition` sits beside elaboration on top of the VIR: it states what a
 # C++ representation's proof-visible states are, and is consumed by elaboration
-# and obligations (ARCHITECTURE.md 44).
+# and obligations (ARCHITECTURE.md 47).
 #
 # `refutation` is the arithmetic refutation search, below both obligations and
 # automation and above nothing but the kernel's types. It is untrusted: what it
 
@@ -2,7 +2,7 @@
 #
 # Automation is untrusted by construction: it can only hand a proof term to the
 # kernel, and the kernel decides. Solvers, tactics and search would be added
-# here, behind the same boundary (ARCHITECTURE.md 21).
+# here, behind the same boundary (ARCHITECTURE.md 54).
 add_library(cppl_automation STATIC
     src/arithmetic.cpp
     src/evidence.cpp
 
@@ -16,7 +16,7 @@ enum class Severity : std::uint8_t {
 
 // What kind of failure this is. Categories are structured data: policy,
 // tooling and reports consume the category, never the rendered wording
-// (ARCHITECTURE.md 38, 40).
+// (ARCHITECTURE.md 74, 75).
 enum class Category : std::uint8_t {
     CpplSyntax,           // malformed C++L construct
     CppSemantic,          // Clang rejected the C++
 
@@ -2,7 +2,7 @@
 #
 # The driver orchestrates stages and owns the exit status. The library holds
 # the implementation so the command-line tool does not become the compiler
-# (ARCHITECTURE.md 43).
+# (ARCHITECTURE.md 5).
 add_library(cppl_driver STATIC
     src/buffer_compile.cpp
     src/crash.cpp
 
@@ -43,7 +43,7 @@ struct BufferCompileOutcome {
     // Whether the buffer was recognized as containing any C++L syntax at
     // all. When false, the buffer is ordinary C++ and was (or would be)
     // compiled directly by Clang with no projection involved
-    // (ARCHITECTURE.md 29).
+    // (ARCHITECTURE.md 81).
     bool has_cppl = false;
 
     // The preprocessed text `tokens` and `syntax` were recognized from. They
 
@@ -17,7 +17,7 @@ struct Input {
 //
 // Everything C++L does not own is preserved in order and handed to Clang
 // unchanged: include paths, defines, warnings, target flags, optimization,
-// linker arguments (ARCHITECTURE.md 50).
+// linker arguments (ARCHITECTURE.md 80).
 struct Options {
     std::vector<std::string> arguments;
     std::vector<Input> inputs;
 
@@ -72,7 +72,7 @@ std::optional<std::string> read_file(const std::filesystem::path& path) {
 
 // The user's command line with the parts that select output and inputs removed,
 // so the same configuration can drive preprocessing and semantic analysis.
-// Everything that affects C++ meaning is kept (ARCHITECTURE.md 51).
+// Everything that affects C++ meaning is kept (ARCHITECTURE.md 80).
 std::vector<std::string> base_arguments(const Options& options) {
     std::vector<bool> is_input(options.arguments.size(), false);
     for (const Input& input : options.inputs) {
 
@@ -66,7 +66,7 @@ PipelineOutcome run_pipeline(const PipelineRequest& request, diagnostics::Engine
     }
 
     if (syntax.empty()) {
-        // Ordinary C++: nothing to verify (ARCHITECTURE.md 29).
+        // Ordinary C++: nothing to verify (ARCHITECTURE.md 81).
         outcome.tokens = std::make_unique<frontend::TokenStream>(stream);
         outcome.syntax = std::make_unique<frontend::Syntax>(std::move(syntax));
         if (request.check_ordinary_cpp_with_clang) {
Original file line number	Diff line number	Diff line change
`@@ -3,14 +3,14 @@`
`3`	`3`	# `source` is added by the top-level CMakeLists because the VIR and the Clang
`4`	`4`	`# bridge depend on it and are configured before this directory.`
`5`	`5`	`#`
`6`		`-# Dependency direction (ARCHITECTURE.md 44):`
	`6`	`+# Dependency direction (ARCHITECTURE.md 95):`
`7`	`7`	`#`
`8`	`8`	`# driver -> frontend / clang bridge -> elaboration -> vir`
`9`	`9`	`# -> obligations -> automation -> kernel`
`10`	`10`	`#`
`11`	`11`	# `decomposition` sits beside elaboration on top of the VIR: it states what a
`12`	`12`	`# C++ representation's proof-visible states are, and is consumed by elaboration`
`13`		`-# and obligations (ARCHITECTURE.md 44).`
	`13`	`+# and obligations (ARCHITECTURE.md 47).`
`14`	`14`	`#`
`15`	`15`	# `refutation` is the arithmetic refutation search, below both obligations and
`16`	`16`	`# automation and above nothing but the kernel's types. It is untrusted: what it`
Original file line number	Diff line number	Diff line change
`@@ -2,7 +2,7 @@`
`2`	`2`	`#`
`3`	`3`	`# Automation is untrusted by construction: it can only hand a proof term to the`
`4`	`4`	`# kernel, and the kernel decides. Solvers, tactics and search would be added`
`5`		`-# here, behind the same boundary (ARCHITECTURE.md 21).`
	`5`	`+# here, behind the same boundary (ARCHITECTURE.md 54).`
`6`	`6`	`add_library(cppl_automation STATIC`
`7`	`7`	`src/arithmetic.cpp`
`8`	`8`	`src/evidence.cpp`
Original file line number	Diff line number	Diff line change
`@@ -2,7 +2,7 @@`
`2`	`2`	`#`
`3`	`3`	`# The driver orchestrates stages and owns the exit status. The library holds`
`4`	`4`	`# the implementation so the command-line tool does not become the compiler`
`5`		`-# (ARCHITECTURE.md 43).`
	`5`	`+# (ARCHITECTURE.md 5).`
`6`	`6`	`add_library(cppl_driver STATIC`
`7`	`7`	`src/buffer_compile.cpp`
`8`	`8`	`src/crash.cpp`
Original file line number	Diff line number	Diff line change
`@@ -66,7 +66,7 @@ PipelineOutcome run_pipeline(const PipelineRequest& request, diagnostics::Engine`
`66`	`66`	`}`
`67`	`67`
`68`	`68`	`if (syntax.empty()) {`
`69`		`- // Ordinary C++: nothing to verify (ARCHITECTURE.md 29).`
	`69`	`+ // Ordinary C++: nothing to verify (ARCHITECTURE.md 81).`
`70`	`70`	`outcome.tokens = std::make_unique<frontend::TokenStream>(stream);`
`71`	`71`	`outcome.syntax = std::make_unique<frontend::Syntax>(std::move(syntax));`
`72`	`72`	`if (request.check_ordinary_cpp_with_clang) {`