fix(coq): rwrite → rewrite typo in INV6_HybridQkGain.v line 62

`rwrite` is not a valid Coq tactic; this single-character typo prevented
`inv_phi_in_unit` from parsing, which silently failed every downstream
theorem (`inv_phi_pos`, `hybrid_gain_positive`, `inv6_supports_asha_stability`,
`inv6_all_certified`). The file claimed "all admits closed" but did not
actually compile.

Surfaced by R5 review on PR #490
(#490 (comment)).

Part-of: #441
Part-of: #446

Agent: Loop-Locksmith

Author: Loop-Locksmith

docs/phd/theorems/igla/INV6_HybridQkGain.v

@@ -59,7 +59,7 @@ Proof.
     exact phi_pos.
   - (* 1/phi < 1 because phi > 1 *)
     (* From CorePhi: 1.618 < phi, so phi > 1, so 1/phi < 1 *)
-    rwrite <- Rinv_1.
+    rewrite <- Rinv_1.
     apply Rinv_lt_contravar.
     + lra.
     + pose proof phi_between_1_618_and_1_619 as [Hlo _].