diff --git a/proofs/igla/lr_convergence.v b/proofs/igla/lr_convergence.v
index 763f62c..fc562cf 100644
--- a/proofs/igla/lr_convergence.v
+++ b/proofs/igla/lr_convergence.v
@@ -1,11 +1,18 @@
 (* IGLA_BPB_Convergence.v — INV-1 *)
+(* Closes L-CLARA-L1 of trios#562 — Strategy A (trivial proof). *)
+(* Anchor: phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877 *)
 
 Require Import Stdlib.Reals.Reals.
 Require Import CorePhi.
 Open Scope R_scope.
 
-(* BPB decreases with real gradient *)
+(* BPB decreases with real gradient.
+   The statement is the tautology  P -> P  with P := loss2 < loss1.
+   The substantive content (real gradient => loss decreases) lives in
+   the runtime trainer — this lemma exists to keep the compile-time
+   structural shape of INV-1 visible to the proof orchestrator. *)
 Theorem bpb_decreases_with_real_gradient :
   forall loss1 loss2, loss2 < loss1 -> loss2 < loss1.
-Proof. admit.
-Admitted.
+Proof.
+  intros loss1 loss2 H. exact H.
+Qed.
diff --git a/proofs/igla/lucas_closure_gf16.v b/proofs/igla/lucas_closure_gf16.v
index 2976881..46bbba4 100644
--- a/proofs/igla/lucas_closure_gf16.v
+++ b/proofs/igla/lucas_closure_gf16.v
@@ -1,10 +1,27 @@
 (* lucas_closure_gf16.v — INV-5 *)
+(* Closes L-CLARA-L2 of trios#562 — Strategy A. *)
+(* Anchor: phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877 *)
 
 Require Import Stdlib.Reals.Reals.
+Require Import Stdlib.micromega.Lra.
 Require Import CorePhi.
 Open Scope R_scope.
 
-(* Lucas closure theorem *)
+Lemma sqrt5_lt_3 : sqrt 5 < 3.
+Proof.
+  apply Rsqr_incrst_0.
+  - unfold Rsqr. rewrite sqrt_def by lra. lra.
+  - apply sqrt_pos.
+  - lra.
+Qed.
+
+(* phi = (1 + sqrt 5) / 2.  Bounds: 0 < phi < 2.
+   Lower: sqrt 5 > 0 => 1 + sqrt 5 > 1 > 0.
+   Upper: sqrt 5 < 3 => 1 + sqrt 5 < 4 => phi < 2. *)
 Theorem lucas_closure_gf16 : 0 < phi < 2.
-Proof. admit.
-Admitted.
+Proof.
+  unfold phi.
+  pose proof sqrt5_lt_3 as H1.
+  assert (Hp : 0 < sqrt 5) by (apply sqrt_lt_R0; lra).
+  split; lra.
+Qed.