Verify explicit dictionary bodies before accepting elaboration - #6286

Stack from ghstack (oldest at bottom):

• Keep elaboration decisions from the final name-resolution pass #6303
• Accept dictionary elaboration only after core verification #6302
• Resolve source givens from their completed binding schemes #6301
• Preserve source given scope across dependency grouping #6300
• Record completed given schemes for deferred resolution #6299
• Build complete dictionary plans independently of note order #6298
• Introduce dictionary parameters while checking qualified definitions #6297
• Order generated dictionary parameters within source scopes #6296
• Capture lexical givens by their active binder identities #6295
• Record dictionary goals at precise checker application sites #6294
• Require determined goal types before dictionary search #6293
• Insert dictionaries at identified expression sites #6292
• Identify lexical dictionary bindings without changing source diagnostics #6291
• Track expression identity separately from source location #6290
• Check implicit arrows without erasing dictionary requirements #6289
• Keep effect rows outside implicit constraint contexts #6288
• Track given membership in namespace metadata #6287
• -> Verify explicit dictionary bodies before accepting elaboration #6286
• Decompose qualified signatures into dictionary candidates #6285
• Handle implicit parameters in function-type utilities #6276
• Represent and store implicit function arrows #6275
• Bound the size of generated implicit goals #6274
• Prefer strictly more specific dictionary conclusions #6273
• Resolve dictionary premises with bounded, context-sensitive search #6272
• Match polymorphic dictionaries without solving goal variables #6271
• Select lexical dictionaries by binding identity and scope #6270
• Preserve reserved namespace names when parsing text #6269

Add a verifier that lowers implicit type arrows to ordinary arrows and checks rewritten bodies against their claimed stored signatures. Lower term annotations and the complete type lookup consistently. Recheck the whole binding group so inserted dictionary dependencies determine the resulting components.

This is an internal prerequisite for enabling elaboration. The caller must use the recomputed component groups while retaining the original qualified signatures, whose lowered forms have now been checked.

Seven focused regressions pass: correct qualified lambdas and explicit applications, wrong or missing dictionary arguments, nested annotations, recomputed recursive components, and rejection of a Nat body claimed to have type forall a. a. The last case reproduces the soundness failure found in #6238. Full validation is recorded in the proof files before publication.

Full validation: all 13 unit suites, 22 CLI integration tests, 391 transcripts, edit/load round trips, manual rewrites, docs HTML generation, compiled fix5507 regression, and formatting passed.