Three mechanical gaps in strata-check's body-expression pipeline,
scoped and ordered by prior research: literal inference and body-scope
const generics are prerequisites for Local lets to be useful, since a
real let almost always carries a literal or a const-generic operand.

- BodyChecker::expr/expr_type now take expected: Option<&TypeRef>,
  threaded from register reset(...), register updates, typed let
  initializers, and the outermost block's tail/return type. A bare
  integer literal synthesizes UInt<N>/Bits<N> when the expected width
  is provable (constant fit, or symbolic width via the existing
  symbolic_constructor_literal_proven path) — never a guessed default
  width. Coverage is single-hop only (direct site or one binary-op/
  method-arg hop); nested literals in deeper subexpressions still
  error as before, which is honest, not a regression.

- check_hir_bodies seeds each callable's body scope with its own const
  generic params so e.g. `DEPTH` resolves in body position instead of
  unresolved_value. A bare generic-as-value still has no arch-ir
  lowering (checked_kind returns None for BindingKind::Generic), so
  strata check accepts it but strata compile can't push it through
  yet — that boundary sits right next to the deferred mem/array gap.

- CheckedComponent gains lets: Vec<CheckedLocal>; strata-arch-ir gains
  Binding::Local(ValueId) and a lowering loop after params, reusing
  the ValueId when a later register update/output/return references
  it. Because lets and registers are flattened into separate arrays,
  only "let referenced by a later register/output" resolves — a let
  reading an earlier register isn't supported by this pass.

mem/array storage remains explicitly out of scope, deferred pending a
written memory-model decision.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>