proof: dangerous pattern closure across 4 submodules

Audit and fix of dangerous patterns (Obj.magic, postulate, Admitted)
across the nextgen-languages monorepo:

- julia-the-viper: eliminated Obj.magic with type-safe VS Code binding
- ephapax: added ctx_mark_used_lookup_at lemma, closed T_Var_Lin
  consumption tracking admit, documented 4 remaining Admitted proofs
  with dependency chains
- oblibeny: annotated 4 FFI/funext postulates as intentional axioms
  with justification (cannot be proved — opaque C FFI boundary)
- phronesis: replaced 3 postulated operations with real implementations
  (value equality, integer less-than, list membership)

Remaining dangerous patterns: 3 Admitted in ephapax/formal/Semantics.v
(deeply interconnected proof obligations requiring new helper lemmas),
4 intentional axioms in oblibeny (FFI boundary + function extensionality).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath