fix(formal/coq): repair Coq mechanization so the safety core actually checks

The Coq formalization never compiled. Faults found and fixed:
- `omega` (removed in Coq 8.12+) -> `lia`.
- `value_eqb`/`phr_type_eqb` used a mutual `Fixpoint ... with` across phr_type
  and list, which Coq's guard checker rejects (not mutually inductive) ->
  rewritten with the nested-`fix` idiom.
- `value_eqb_refl` invoked a nonexistent phr_value_rect P0/P1 eliminator -> two
  strong (nested) induction principles phr_type_ind'/phr_value_ind' added.
- `phr_type_eq_dec`'s `decide equality` could not dispatch nested TRecord ->
  genuinely decidable now (this is the obligation that was unsound in Agda).
- `preservation` was missing the T_List case, elided the record-field case, and
  lost the empty context in the EVar case -> reproved by induction on
  evaluation (keeps [] concrete); T_List via a list helper; field case closed
  by stating VT_Record over field_lookup.
- `eval_deterministic` had a variable-name clash + miscalibrated bullets ->
  uniform IH-driven tactic.
- `no_system_calls` was unsound (ELit (VString "system") satisfied it) and
  ill-typed (untyped existential) -> honest by-construction sandbox_no_call_form.
- `totality` was malformed (Theorem ... with Fixpoint) and false as stated
  (no typing hypothesis) -> free_vars extracted; restated correctly and left as
  the lone explicit Admitted (termination, not yet mechanized, unused by core).

Result: `coqc Phronesis.v` exits 0. `Print Assumptions` on preservation,
eval_deterministic, type_safety, phr_type_eq_dec, subtype_trans, value_eqb_refl,
literal_preservation, sandbox_no_call_form = "Closed under the global context"
(axiom-free). SPDX header left unchanged.

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

Author: hyperpolymath