docs: analyze Hemlock against the gradual guarantee and blame theorem

[nbeerbower]

Formalizes what Hemlock's optional annotations actually do (convert_to_type
is a lossy, effectful coercion rather than a cast) and tests the language
against the two standard gradual-typing correctness criteria:

• Static gradual guarantee: VIOLATED - inference pins unannotated bindings
  to rigid types, so erasing 'let a: array' introduces a type error.
• Dynamic gradual guarantee: VIOLATED - ascription converts values
  (3.99 -> 3, 3 -> true), annotation checks mutate shared aggregates in
  place (element coercion, optional-field materialization, nominal brands
  observed by match), and removing an annotation can introduce a crash.
  Separately documents the inherent numeric-semantics obstruction (i32/i64
  overflow policy) that justifies a weakened criterion.
• Blame theorem: FAILS - function-type casts are erased (no monitoring),
  boundary failures surface inside and are attributed to well-typed code,
  ref parameters skip checks entirely, and failure discipline is split
  across catchable/uncatchable/no-location regimes.

Includes 17 runnable witness programs (docs/design/gradual-typing/), all
verified against both backends; interpreter and compiler agree on every
witness except blame3_ref.hml, where the static checker rejects what the
interpreter runs. Closes with a repair taxonomy: which behaviors are
design (weaken the criterion), which are semantic choices to change, and
which are bugs under any reading.

Co-Authored-By: Claude Fable 5 noreply@anthropic.com
Claude-Session: https://claude.ai/code/session_01XBoD5i9DECci3pWURU1CTW