fix(a2ml-core): make sectionTitlesOf total (trusted-base gate)

The governance / Trusted-base reduction policy flagged Profiles.idr:207 as
an undocumented `partial` escape hatch. Rather than document new proof debt,
eliminate it: sectionTitlesOf now recurses only on the block-list tail and
extracts TOP-LEVEL section titles, which is total by construction and exact
for the flat record dialects (the 6a2 family). Nested-section extraction for
general markup remains the translator's responsibility (it supplies DocFacts
directly), so conformance never depended on the recursive walk.

Verified locally: scripts/check-trusted-base.sh . exits 0 (15 pre-existing
documented hatches; zero new). No escape hatches in the new a2ml-core modules.

https://claude.ai/code/session_01XZhw6Fq27eoeyEB4LR3a2c

Author: claude

a2ml/src/A2ML/Profiles.idr

@@ -200,17 +200,21 @@ checkProfile pd f =
 -- Fact extraction from the v1.0 core (section titles)
 -- ============================================================================
 
-||| Recursively collect every Section title. Marked partial for the same reason
-||| as TypedCore.collectIds: the walk recurses through the section-body wrapper.
-||| Decidability of conformance does not depend on this being total.
+||| Collect the TOP-LEVEL Section titles of a document. Total by construction:
+||| it recurses only on the block-list tail and never descends through section
+||| bodies, so it introduces no escape hatch (cf. TypedCore.collectIds, which is
+||| `partial`). Flat record dialects — the entire 6a2 family — have only
+||| top-level sections, so this is exact for them. Nested-section extraction for
+||| general markup is the translator's responsibility: the translator supplies
+||| `DocFacts` directly, so conformance never relies on this helper recursing.
 export
-partial
 sectionTitlesOf : Doc -> List String
-sectionTitlesOf (MkDoc blocks) = concatMap go blocks
+sectionTitlesOf (MkDoc blocks) = collect blocks
   where
-    go : Block -> List String
-    go (Section s) = s.title :: sectionTitlesOf (MkDoc s.body)
-    go _           = []
+    collect : List Block -> List String
+    collect []                = []
+    collect (Section s :: bs) = s.title :: collect bs
+    collect (_ :: bs)         = collect bs
 
 -- ============================================================================
 -- Composition: union of constraints (SPEC Section 8.1)