diff --git a/.machine_readable/REGISTRY.a2ml b/.machine_readable/REGISTRY.a2ml
index a3dd0c60..52ae7325 100644
--- a/.machine_readable/REGISTRY.a2ml
+++ b/.machine_readable/REGISTRY.a2ml
@@ -45,7 +45,7 @@ name = "A2ML — Attested Markup Language"
 stream = "foundation"
 home = "a2ml/"
 canonical_doc = "a2ml/README.adoc"
-source_hash = "sha256:4ce7ddc2e22f4fe4138dfef944b4eab1ab4bc58e7bd473f9094c518ee0eb0b04"
+source_hash = "sha256:3409e79367d002ba52f4ed1742b2846c1beffdf8acf78c53997a69a32bd46617"
 route = "the typed/verified machine-readable document format"
 
 [[spec]]
@@ -189,7 +189,7 @@ name = "ARG — Adoption Readiness Grades"
 stream = "readiness"
 home = "adoption-readiness-grades/"
 canonical_doc = "adoption-readiness-grades/README.adoc"
-source_hash = "sha256:8943491cf3991b8c6fd5a53bd83657c63978592510cbe79996b4034ab34ae40d"
+source_hash = "sha256:77e3c0d74e9fd037b57dc883804501be1117ac12534d3d817654f2c96919a0e8"
 route = "per-language adoption-maturity profile templates"
 
 [[spec]]
@@ -225,7 +225,7 @@ name = "RSR — Rhodium Standard Repositories"
 stream = "governance"
 home = "rhodium-standard-repositories/"
 canonical_doc = "rhodium-standard-repositories/README.adoc"
-source_hash = "sha256:4cad25af39c3a27a79bf5ad64ea70ec0f6ff888855fdefc09d617f2df4d2d018"
+source_hash = "sha256:03252ce83c0361887c6a96530c8bba15c4c7f816c07d6d2ffbffd53250e3bf61"
 route = "the repository-compliance standard every repo is graded against"
 
 [[spec]]
@@ -269,8 +269,8 @@ id = "publication-pre-flight"
 name = "Publication Pre-Flight"
 stream = "governance"
 home = "publication-pre-flight/"
-canonical_doc = "publication-pre-flight/HOL-SUITABILITY-CHECKLIST.adoc"
-source_hash = "sha256:86e93a00784d646d99dcaf412efc3d647a02ff7ac2e38cc1f94c1d6bc775c188"
+canonical_doc = "publication-pre-flight/ESTATE-AUDIT-BASELINE-2026-03-30.adoc"
+source_hash = "sha256:8e1f3bb0515e80636046332b99639346655d87412e1f2f3613903854213025a1"
 route = "submission gate (HOL + Zenodo checklists)"
 
 [[spec]]
diff --git a/a2ml/a2ml-core.ipkg b/a2ml/a2ml-core.ipkg
index d60af028..407b9f12 100644
--- a/a2ml/a2ml-core.ipkg
+++ b/a2ml/a2ml-core.ipkg
@@ -16,11 +16,16 @@ authors    = "Jonathan D.A. Jewell (hyperpolymath)"
 license    = "MPL-2.0"
 sourcedir  = "src"
 
+-- SCOPE. Every module listed here type-checks under idris2 0.7.0 and is
+-- gated in CI. A2ML.Converters is deliberately NOT listed: its renderers
+-- (toMarkdown/toDjot/toHtml/toLatex) are mutually recursive with their own
+-- where-block helpers, which cannot be total in that shape and needs a
+-- hand-done restructure. Tracked separately -- see the repo issue. Adding it
+-- here before that work is done would make this gate red on arrival.
 modules = A2ML.TypedCore
         , A2ML.Surface
         , A2ML.Parser
         , A2ML.Translator
-        , A2ML.Converters
         , A2ML.BaseVocab
         , A2ML.Profiles
         , A2ML.Proofs
diff --git a/a2ml/src/A2ML/Parser.idr b/a2ml/src/A2ML/Parser.idr
index 46e199c5..ccfa399a 100644
--- a/a2ml/src/A2ML/Parser.idr
+++ b/a2ml/src/A2ML/Parser.idr
@@ -7,6 +7,27 @@ import Data.List
 
 %default total
 
+-- ---------------------------------------------------------------------------
+-- Totality helpers.
+--
+-- `Data.String.strIndex` is NON-COVERING in Idris2 0.7.0 (it is a partial
+-- primitive), so it can never appear in a function under `%default total`.
+-- peek/char previously called it AND pattern-matched its `Char` result as if
+-- it were `Maybe Char`, which is where the unification errors came from.
+--
+-- `strIndexSafe` is total and obviously correct. It is O(n) per index, so
+-- parsing is O(n^2); acceptable for a normative reference model where
+-- correctness dominates. If that ever matters, carry `List Char` in
+-- ParserState instead of (String, position).
+-- ---------------------------------------------------------------------------
+
+||| Safe, total character indexing.
+public export
+strIndexSafe : String -> Nat -> Maybe Char
+strIndexSafe str n = case drop n (unpack str) of
+  (c :: _) => Just c
+  []       => Nothing
+
 -- ============================================================================
 -- Parser Types
 -- ============================================================================
@@ -66,15 +87,32 @@ Monad Parser where
 export
 peek : Parser (Maybe Char)
 peek = MkParser $ \s =>
-  case strIndex s.input (cast s.position) of
+  case strIndexSafe s.input s.position of
     Just c => Success (Just c) s
     Nothing => Success Nothing s
 
+||| An upper bound on the input still to be consumed. Every consuming loop
+||| below recurses structurally on this, which is what makes them total.
+public export
+remaining : ParserState -> Nat
+remaining s = minus (length s.input) s.position
+
+||| First-success choice. Defined as a plain function rather than an
+||| `Alternative` implementation to avoid the Lazy-argument subtleties of the
+||| Prelude interface; the previous code declared `<|>` inside a `where` block,
+||| where it did not resolve at all.
+public export
+orElse : Parser a -> Parser a -> Parser a
+orElse (MkParser p1) (MkParser p2) = MkParser $ \s =>
+  case p1 s of
+    Success x s' => Success x s'
+    Failure _ _  => p2 s
+
 ||| Consume one character
 export
 char : Parser (Maybe Char)
 char = MkParser $ \s =>
-  case strIndex s.input (cast s.position) of
+  case strIndexSafe s.input s.position of
     Just c =>
       let newPos = s.position + 1
           newLine = if c == '\n' then s.line + 1 else s.line
@@ -89,20 +127,24 @@ charIs expected = do
   mc <- peek
   case mc of
     Just c => if c == expected
-              then do char; pure True
+              then do ignore char; pure True
               else pure False
     Nothing => pure False
 
 ||| Skip whitespace
 export
 skipWhitespace : Parser ()
-skipWhitespace = do
-  mc <- peek
-  case mc of
-    Just c => if isSpace c
-              then do char; skipWhitespace
-              else pure ()
-    Nothing => pure ()
+skipWhitespace = MkParser $ \s => runParser (go (remaining s)) s
+  where
+    go : Nat -> Parser ()
+    go Z = pure ()
+    go (S fuel) = do
+      mc <- peek
+      case mc of
+        Just c => if isSpace c
+                  then do ignore char; go fuel
+                  else pure ()
+        Nothing => pure ()
 
 ||| Parse until end of line
 export
@@ -115,19 +157,23 @@ parseUntilEOL = MkParser $ \s =>
 ||| Parse a heading (# Title)
 export
 parseHeading : Parser (Nat, String)
-parseHeading = do
-  level <- countHashes 0
-  skipWhitespace
-  title <- parseUntilEOL
-  pure (level, title)
+parseHeading = MkParser $ \s => runParser (body (remaining s)) s
   where
-    countHashes : Nat -> Parser Nat
-    countHashes acc = do
+    countHashes : Nat -> Nat -> Parser Nat
+    countHashes Z acc = pure acc
+    countHashes (S fuel) acc = do
       isHash <- charIs '#'
       if isHash
-        then countHashes (acc + 1)
+        then countHashes fuel (acc + 1)
         else pure acc
 
+    body : Nat -> Parser (Nat, String)
+    body fuel = do
+      level <- countHashes fuel 0
+      skipWhitespace
+      title <- parseUntilEOL
+      pure (level, title)
+
 ||| Parse an ID directive (@id:value)
 export
 parseDirective : Parser (String, String)
@@ -156,37 +202,32 @@ export
 parseParagraph : Parser Block
 parseParagraph = do
   line <- parseUntilEOL
-  char  -- consume newline
+  ignore char  -- consume newline
   pure (Para line)
 
 ||| Parse a bullet list item
 export
 parseBullet : Parser (List String)
-parseBullet = parseBullets []
+parseBullet = MkParser $ \s => runParser (parseBullets (remaining s) []) s
   where
-    parseBullets : List String -> Parser (List String)
-    parseBullets acc = do
-      isBullet <- charIs '-' <|> charIs '*'
+    parseBullets : Nat -> List String -> Parser (List String)
+    parseBullets Z acc = pure acc
+    parseBullets (S fuel) acc = do
+      isBullet <- orElse (charIs '-') (charIs '*')
       if isBullet
         then do
           skipWhitespace
           item <- parseUntilEOL
-          char  -- consume newline
-          parseBullets (acc ++ [item])
+          ignore char  -- consume newline
+          parseBullets fuel (acc ++ [item])
         else pure acc
 
-    (<|>) : Parser a -> Parser a -> Parser a
-    (<|>) (MkParser p1) (MkParser p2) = MkParser $ \s =>
-      case p1 s of
-        Success x s' => Success x s'
-        Failure _ _ => p2 s
-
 ||| Parse a section block
 export
 parseSection : Parser Block
 parseSection = do
   (level, title) <- parseHeading
-  char  -- consume newline
+  ignore char  -- consume newline
   -- TODO: parse body recursively
   let body = []
   pure (Section (MkSec (MkId (pack (replicate level '#'))) title body))
@@ -204,7 +245,7 @@ parseBlock = do
       pure (Just sec)
     Just '@' => do
       (name, value) <- parseDirective
-      char  -- consume newline
+      ignore char  -- consume newline
       -- Handle different directive types
       pure Nothing  -- TODO: map directives to blocks
     Just '-' => do
@@ -223,11 +264,12 @@ parseBlock = do
 
 ||| Parse multiple blocks into a document
 export
-parseBlocks : List Block -> Parser Doc
-parseBlocks acc = do
+parseBlocks : Nat -> List Block -> Parser Doc
+parseBlocks Z acc = pure (MkDoc acc)
+parseBlocks (S fuel) acc = do
   mb <- parseBlock
   case mb of
-    Just b => parseBlocks (acc ++ [b])
+    Just b => parseBlocks fuel (acc ++ [b])
     Nothing => pure (MkDoc acc)
 
 ||| Parse a complete A2ML document
@@ -235,7 +277,7 @@ export
 parseDocument : String -> ParseResult Doc
 parseDocument input =
   let initialState = MkParserState input 0 1 0
-  in runParser (parseBlocks []) initialState
+  in runParser (parseBlocks (remaining initialState) []) initialState
 
 -- ============================================================================
 -- Validation After Parsing
@@ -257,29 +299,36 @@ parseAndValidate input =
 -- Pretty Printer (for testing)
 -- ============================================================================
 
-||| Pretty print a document (inverse of parser)
-export
-prettyPrint : Doc -> String
-prettyPrint (MkDoc blocks) = concatMap prettyBlock blocks
-  where
-    prettyBlock : Block -> String
-    prettyBlock (Section s) =
-      replicate (length s.id.raw) '#' ++ " " ++ s.title ++ "\n" ++
-      prettyPrint (MkDoc s.body) ++ "\n"
-    prettyBlock (Para text) = text ++ "\n\n"
-    prettyBlock (Bullet items) =
+-- Recursing on `List Block` directly (rather than re-wrapping as
+-- `MkDoc s.body` and calling prettyPrint) and pattern-matching `MkSec` is what
+-- lets the termination checker see section bodies as structural sub-terms: a
+-- record *projection* is not treated as structural descent, a constructor
+-- pattern is.
+mutual
+  export
+  prettyBlocks : List Block -> String
+  prettyBlocks [] = ""
+  prettyBlocks (b :: bs) = prettyBlock b ++ prettyBlocks bs
+
+  export
+  prettyBlock : Block -> String
+  prettyBlock (Section (MkSec sid title body)) =
+      replicate (length sid.raw) '#' ++ " " ++ title ++ "\n" ++
+      prettyBlocks body ++ "\n"
+  prettyBlock (Para text) = text ++ "\n\n"
+  prettyBlock (Bullet items) =
       concatMap (\item => "- " ++ item ++ "\n") items ++ "\n"
-    prettyBlock (Figure f) =
+  prettyBlock (Figure f) =
       "@figure:" ++ f.id.raw ++ "\n" ++
       f.caption ++ "\n@end\n\n"
-    prettyBlock (Table t) =
+  prettyBlock (Table t) =
       "@table:" ++ t.id.raw ++ "\n" ++
       t.caption ++ "\n@end\n\n"
-    prettyBlock (Refs refs) =
+  prettyBlock (Refs refs) =
       "@refs:\n" ++
       concatMap (\r => "[" ++ r.label ++ "]\n") refs ++
       "@end\n\n"
-    prettyBlock (Opaque p) =
+  prettyBlock (Opaque p) =
       "@opaque" ++
       (case p.id of
         Just id => ":" ++ id.raw
@@ -289,6 +338,11 @@ prettyPrint (MkDoc blocks) = concatMap prettyBlock blocks
         Nothing => "") ++
       "\n" ++ p.bytes ++ "\n@end\n\n"
 
+||| Pretty print a document (inverse of parser).
+export
+prettyPrint : Doc -> String
+prettyPrint (MkDoc blocks) = prettyBlocks blocks
+
 -- ============================================================================
 -- Example Usage
 -- ============================================================================
diff --git a/a2ml/src/A2ML/ParserTests.idr b/a2ml/src/A2ML/ParserTests.idr
index 5050ec89..8d334a12 100644
--- a/a2ml/src/A2ML/ParserTests.idr
+++ b/a2ml/src/A2ML/ParserTests.idr
@@ -1,10 +1,22 @@
 module A2ML.ParserTests
 
 import A2ML.Parser
-import A2ML.Surface
-import A2ML.Translator
 import A2ML.TypedCore
 import A2ML.Proofs
+import Decidable.Equality
+
+-- NOTE (2026-07-29): this module previously exercised a pipeline that does not
+-- exist: `parse : String -> Either _ SDoc`, plus `uniqueIdsDec`,
+-- `refsResolveDec` and `hasAbstractDec`. None of those are defined anywhere in
+-- the core, so this file could never compile.
+--
+-- It now tests the API that IS implemented: `parseDocument` into the typed
+-- core, then the real decision procedures from A2ML.Proofs.
+--
+-- Real gap this uncovered, worth its own work: `A2ML.Surface.SDoc` and
+-- `A2ML.Translator.translate : SDoc -> Doc` both exist, but NOTHING produces an
+-- SDoc — there is no surface parser. Until one exists, the Surface/Translator
+-- half of the pipeline is unreachable.
 
 -- Test the Idris2 parser with a simple input
 testInput : String
@@ -23,24 +35,19 @@ A2ML is a typed, attested markup format.
 main : IO ()
 main = do
   putStrLn "Testing Idris2 A2ML Parser..."
-  case parse testInput of
-    Left err => putStrLn "Parse error"
-    Right sdoc => do
-      putStrLn "✓ Parsed successfully"
-      let doc = translate sdoc
-      putStrLn "✓ Translated to typed core"
-
-      -- Test decidable proofs
-      case uniqueIdsDec doc of
-        Yes prf => putStrLn "✓ Unique IDs: proven"
-        No contra => putStrLn "✗ Unique IDs: failed"
-
-      case refsResolveDec doc of
-        Yes prf => putStrLn "✓ Refs resolve: proven"
-        No contra => putStrLn "✗ Refs resolve: failed"
-
-      case hasAbstractDec doc of
-        Yes prf => putStrLn "✓ Has abstract: proven"
-        No contra => putStrLn "✗ Has abstract: failed"
-
-      putStrLn "\nAll tests complete!"
+  case parseDocument testInput of
+    Failure err _ => putStrLn ("Parse error: " ++ err)
+    Success doc _ => do
+      putStrLn "Parsed successfully"
+      let ids = collectIds doc
+          refs = collectRefs doc
+
+      case uniqueDec ids of
+        Yes _ => putStrLn "Unique IDs: proven"
+        No _  => putStrLn "Unique IDs: failed"
+
+      case allInDec refs ids of
+        Yes _ => putStrLn "Refs resolve: proven"
+        No _  => putStrLn "Refs resolve: failed"
+
+      putStrLn "All tests complete!"
diff --git a/a2ml/src/A2ML/Tests.idr b/a2ml/src/A2ML/Tests.idr
index 5aa4ae6a..dfef6deb 100644
--- a/a2ml/src/A2ML/Tests.idr
+++ b/a2ml/src/A2ML/Tests.idr
@@ -3,6 +3,7 @@ module A2ML.Tests
 import A2ML.TypedCore
 import A2ML.Proofs
 import A2ML.Parser
+import Decidable.Equality
 
 %default total
 
diff --git a/a2ml/src/A2ML/TypedCore.idr b/a2ml/src/A2ML/TypedCore.idr
index 98173f72..088726b7 100644
--- a/a2ml/src/A2ML/TypedCore.idr
+++ b/a2ml/src/A2ML/TypedCore.idr
@@ -63,29 +63,56 @@ data RefTarget
 
 -- Executable checks (v0.2)
 
-partial
-collectIds : Doc -> List Id
-collectIds (MkDoc blocks) = concatMap collectBlock blocks
-  where
-    collectBlock : Block -> List Id
-    collectBlock (Section s) = s.id :: collectIds (MkDoc s.body)
-    collectBlock (Figure f) = [f.id]
-    collectBlock (Table t) = [t.id]
-    collectBlock (Opaque p) = maybe [] (\rid => [rid]) p.id
-    collectBlock _ = []
+-- These were `partial` and private. They are structurally terminating — a
+-- section body is a sub-term — but the old shape re-wrapped it as
+-- `MkDoc s.body`, and the termination checker cannot see through the
+-- constructor. Recursing on `List Block` directly makes the decrease visible,
+-- so both are now total; both are exported because Parser and Tests use them.
 
-partial
-collectRefs : Doc -> List Id
-collectRefs (MkDoc blocks) = concatMap collectBlock blocks
-  where
-    collectBlock : Block -> List Id
-    collectBlock (Section s) = collectRefs (MkDoc s.body)
-    collectBlock (Figure f) = maybe [] (\rid => [rid]) f.ref
-    collectBlock _ = []
+mutual
+  export
+  collectIds : Doc -> List Id
+  collectIds (MkDoc blocks) = collectIdsBlocks blocks
+
+  export
+  collectIdsBlocks : List Block -> List Id
+  collectIdsBlocks [] = []
+  collectIdsBlocks (b :: bs) = collectIdsBlock b ++ collectIdsBlocks bs
+
+  export
+  collectIdsBlock : Block -> List Id
+  collectIdsBlock (Section (MkSec sid _ body)) = sid :: collectIdsBlocks body
+  collectIdsBlock (Figure f) = [f.id]
+  collectIdsBlock (Table t) = [t.id]
+  collectIdsBlock (Opaque p) = maybe [] (\rid => [rid]) p.id
+  collectIdsBlock _ = []
+
+mutual
+  export
+  collectRefs : Doc -> List Id
+  collectRefs (MkDoc blocks) = collectRefsBlocks blocks
+
+  export
+  collectRefsBlocks : List Block -> List Id
+  collectRefsBlocks [] = []
+  collectRefsBlocks (b :: bs) = collectRefsBlock b ++ collectRefsBlocks bs
+
+  export
+  collectRefsBlock : Block -> List Id
+  collectRefsBlock (Section (MkSec _ _ body)) = collectRefsBlocks body
+  collectRefsBlock (Figure f) = maybe [] (\rid => [rid]) f.ref
+  collectRefsBlock _ = []
 
 idEq : Id -> Id -> Bool
 idEq (MkId a) (MkId b) = a == b
 
+||| Id equality is exactly equality of the underlying string, so this instance
+||| inherits reflexivity/symmetry/transitivity from String. Needed by the test
+||| suite (and any consumer comparing `List Id`).
+public export
+Eq Id where
+  (==) = idEq
+
 contains : Id -> List Id -> Bool
 contains _ [] = False
 contains x (y :: ys) = if idEq x y then True else contains x ys