Keep elaboration decisions from the final name-resolution pass - #6303

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 an opt-in checking entry point that replaces provisional dictionary goals, parameters, given types, and component signatures after type-directed name resolution retries. Preserve name-resolution decisions and return the resolved source term for verified insertion. The existing entry point retains its behavior.

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