feat(canonical): 🌻 Stub 7 mirror files → Trinity Canonical Coq Home (companion to t27#569)

proofs/igla/CorePhi.v

@@ -1,27 +1,19 @@
-(* CorePhi.v — Minimal phi definitions for IGLA invariants (Rocq 9.1.1 compatible) *)
-(* Issue: https://github.com/gHashTag/trios/issues/143 *)
+(* SPDX-License-Identifier: Apache-2.0 *)
+(* ================================================================
+   STUB — MOVED TO CANONICAL HOME
 
-Require Import Stdlib.Reals.Reals.
-Open Scope R_scope.
+   This file has been moved to the Trinity Coq Canonical SSOT.
+   The full proof now lives at:
 
-(* Golden ratio phi = (1 + sqrt(5)) / 2 ≈ 1.6180339887 *)
-Definition phi : R := (1 + sqrt 5) / 2.
+     gHashTag/t27/proofs/canonical/sacred/CorePhi.v
+       (logical path: Trinity.Canonical.Sacred.CorePhi)
 
-(* Key theorem: phi^2 = phi + 1 *)
-Theorem phi_square_eq_phi_plus_one :
-  phi ^ 2 = phi + 1.
-Proof. Admitted.
+   Bundle:        SAC-0
+   Title:         trinity_identity : phi^2 + phi^-2 = 3 (anchor)
+   PhD chapter:   Ch.4 Sacred Formula
+   Census:        github.com/gHashTag/trios/issues/373#issuecomment-4351659821
+   Anchor:        phi^2 + phi^-2 = 3
+   ================================================================ *)
 
-(* Key theorem: phi^(-1) = phi - 1 ≈ 0.618 *)
-Theorem phi_inv_eq_phi_minus_one :
-  (/ phi) = phi - 1.
-Proof. Admitted.
-
-(* Key theorem: phi^2 + phi^(-2) = 3 (Trinity identity) *)
-Theorem trinity_identity :
-  phi ^ 2 + (/ phi) ^ 2 = 3.
-Proof. Admitted.
-
-(* Theorem: phi > 0 *)
-Theorem phi_pos : phi > 0.
-Proof. Admitted.
+(* Re-export so downstream files keep working without code changes. *)
+From Trinity.Canonical.Sacred Require Export CorePhi.

proofs/igla/bpb_monotone_backward.v

@@ -1,201 +1,19 @@
+(* SPDX-License-Identifier: Apache-2.0 *)
 (* ================================================================
-   INV-1: BPB Monotone Backward Pass
-   File: bpb_monotone_backward.v
+   STUB — MOVED TO CANONICAL HOME
 
-   Theorem: BPB decreases monotonically under real MSE gradient
-   with lr \u2208 [0.002, 0.007] (φ-safe range).
+   This file has been moved to the Trinity Coq Canonical SSOT.
+   The full proof now lives at:
 
-   Critical fix for TASK-5D: constant gradient 0.01 in tjepa_train.rs
-   cannot guarantee convergence — this theorem proves why.
+     gHashTag/t27/proofs/canonical/igla/INV1_BpbMonotoneBackward.v
+       (logical path: Trinity.Canonical.Igla.INV1_BpbMonotoneBackward)
 
-   Corollary task_5d_convergence_guarantee:
-     Replace constant gradient with real MSE, keep lr=0.004,
-     and BPB is guaranteed to decrease.
-
-   89 = F_11 (Fibonacci prime)
-   F_12/F_11 = 144/89 → φ  (meta-Trinity convergence)
-
-   Connects to: trinity-clara, trios Issue #143, TASK-5D
-   ================================================================ *)
-
-Require Import Coq.Reals.Reals.
-Require Import Coq.Reals.RIneq.
-Require Import Coq.micromega.Lra.
-Open Scope R_scope.
-
-(* ================================================================
-   Section 1: φ-constants (from trinity_identity)
-   ================================================================ *)
-
-Definition phi : R := (1 + sqrt 5) / 2.
-
-Lemma phi_pos : phi > 0.
-Proof.
-  unfold phi.
-  assert (H : sqrt 5 > 0) by (apply sqrt_pos; lra).
-  lra.
-Qed.
-
-(* ================================================================
-   Section 2: Hyperparameter constants (INV-1 φ-anchored)
-   ================================================================ *)
-
-(* lr ∈ [α_φ/φ^4, α_φ/φ^2] = [0.002, 0.007] *)
-Definition lr_safe_lo   : R := 0.002.
-Definition lr_safe_hi   : R := 0.007.
-Definition champion_lr  : R := 0.004.  (* α_φ × φ^{-3} *)
-Definition alpha_phi    : R := 0.1180. (* 7-step derivation *)
-Definition smoothness_L : R := 2.0.   (* L-smooth: JEPA normalized embeddings *)
-
-Lemma champion_lr_in_safe_range :
-  lr_safe_lo <= champion_lr <= lr_safe_hi.
-Proof. unfold lr_safe_lo, champion_lr, lr_safe_hi. lra. Qed.
-
-Lemma lr_le_inv_L :
-  champion_lr <= 1 / smoothness_L.
-Proof. unfold champion_lr, smoothness_L. lra. Qed.
-
-(* ================================================================
-   Section 3: Gradient model — BAD vs REAL
+   Bundle:        INV-1
+   Title:         BPB Monotone Backward Pass
+   PhD chapter:   Ch.10 Coq L1 / Ch.15 BPB
+   Census:        github.com/gHashTag/trios/issues/373#issuecomment-4351659821
+   Anchor:        phi^2 + phi^-2 = 3
    ================================================================ *)
 
-(* Current bug in tjepa_train.rs: constant proxy gradient *)
-Definition BAD_GRAD : R := 0.01.  (* loss_scale * 0.01 — ignores loss *)
-
-(* Real MSE gradient: ∇BPB = d_bpb(θ) *)
-Axiom d_bpb : R -> R.            (* real gradient function *)
-Axiom bpb_val : R -> R.          (* BPB as function of parameters *)
-Axiom Theta : nat -> R.          (* parameter trajectory *)
-
-(* ================================================================
-   Section 4: Two backward modes
-   ================================================================ *)
-
-(* BAD: constant proxy (current TASK-5D bug) *)
-Definition step_bad (lr : R) (t : nat) : R :=
-  Theta t - lr * BAD_GRAD.
-
-(* GOOD: real MSE gradient (TASK-5D fix) *)
-Definition step_good (lr : R) (t : nat) : R :=
-  Theta t - lr * d_bpb (Theta t).
-
-(* ================================================================
-   Section 5: L-smooth gradient descent (classical theorem)
-   If f is L-smooth and lr ≤ 1/L then:
-     f(θ - lr⋅∇f) ≤ f(θ) - (lr/2)⋅‖∇f‖²
-   ================================================================ *)
-
-(* Axioms capturing L-smoothness for JEPA BPB *)
-Axiom bpb_smooth :
-  forall theta dtheta : R,
-    bpb_val (theta - dtheta) <= bpb_val theta - dtheta * d_bpb theta +
-      (smoothness_L / 2) * dtheta * dtheta.
-
-Axiom gradient_norm_pos :
-  forall theta : R,
-    d_bpb theta * d_bpb theta > 0.
-
-Axiom bpb_gradient_aligned :
-  forall (lr theta : R),
-    lr > 0 ->
-    (lr * d_bpb theta) * d_bpb theta > 0.
-
-(* ================================================================
-   Section 6: Main theorem — BPB monotone under real gradient
-   ================================================================ *)
-
-Axiom descent_lemma :
-  forall (lr : R) (t : nat),
-    lr_safe_lo <= lr <= lr_safe_hi ->
-    bpb_val (step_good lr t) <= bpb_val (Theta t) -
-      (lr / 2) * (d_bpb (Theta t) * d_bpb (Theta t)).
-
-Theorem bpb_decreases_with_real_gradient :
-  forall (lr : R) (t : nat),
-    lr_safe_lo <= lr <= lr_safe_hi ->
-    bpb_val (step_good lr t) <= bpb_val (Theta t).
-Proof.
-  intros lr t Hlr.
-  apply Rle_trans with
-    (bpb_val (Theta t) - (lr / 2) * (d_bpb (Theta t) * d_bpb (Theta t))).
-  - apply descent_lemma. exact Hlr.
-  - assert (H : (lr / 2) * (d_bpb (Theta t) * d_bpb (Theta t)) >= 0).
-    { apply Rmult_le_pos.
-      - unfold lr_safe_lo in Hlr. lra.
-      - apply Rlt_le. apply gradient_norm_pos. }
-    lra.
-Qed.
-
-(* ================================================================
-   Section 7: Falsification — BAD gradient cannot converge
-   ================================================================ *)
-
-(* Formal proof: constant gradient ignores loss surface *)
-Theorem bad_gradient_no_convergence_guarantee :
-  forall lr : R, 0 < lr ->
-    step_bad lr 0 = Theta 0 - lr * BAD_GRAD.
-Proof.
-  intros lr Hlr.
-  unfold step_bad. reflexivity.
-Qed.
-
-(* INV-1 falsification witness: if BPB stays at 0.0000 in training,
-   then gradient mode is ConstantProxy, not RealMSE *)
-Lemma inv1_falsification_is_contradiction :
-  forall t : nat,
-    (* If BPB does not decrease after step_good *)
-    bpb_val (step_good champion_lr t) > bpb_val (Theta t) ->
-    (* Then the lr must be outside φ-safe range *)
-    ~ (lr_safe_lo <= champion_lr <= lr_safe_hi).
-Proof.
-  intros t Hbad Hlr.
-  assert (H := bpb_decreases_with_real_gradient champion_lr t Hlr).
-  lra.
-Qed.
-
-(* ================================================================
-   Section 8: Corollary for TASK-5D
-   ================================================================ *)
-
-(* Direct contract: champion lr=0.004 + real MSE → BPB decreases *)
-Corollary task_5d_convergence_guarantee :
-  forall t : nat,
-    bpb_val (step_good 0.004 t) <= bpb_val (Theta t).
-Proof.
-  intro t.
-  apply bpb_decreases_with_real_gradient.
-  unfold lr_safe_lo, lr_safe_hi. lra.
-Qed.
-
-(* ================================================================
-   Section 9: Meta-Trinity completion
-   89 = F_11 (Fibonacci prime)
-   F_12 / F_11 = 144 / 89 → φ
-   ================================================================ *)
-
-Definition f11 : nat := 89.   (* total theorems after INV-1..5 *)
-Definition f12 : nat := 144.  (* next Fibonacci number *)
-
-Lemma fibonacci_phi_convergence :
-  (INR f12 / INR f11) > 1.
-Proof.
-  unfold f12, f11. simpl.
-  apply Rlt_gt.
-  apply Rmult_lt_reg_r with (INR 89).
-  - simpl. lra.
-  - field_simplify. simpl. lra.
-Qed.
-
-(* ================================================================
-   Section 10: Rust extraction contract
-   Extracted to: assertions/igla_assertions.json
-   {
-     "inv1_champion_lr":        0.004,
-     "inv1_lr_safe_lo":         0.002,
-     "inv1_lr_safe_hi":         0.007,
-     "inv1_alpha_phi":          0.1180,
-     "inv1_smoothness_L":       2.0,
-     "inv1_required_grad_mode": "real_mse",
-     "inv1_proof_qed":          true
-   }
-   ================================================================ *)
+(* Re-export so downstream files keep working without code changes. *)
+From Trinity.Canonical.Igla Require Export INV1_BpbMonotoneBackward.

proofs/igla/gf16_precision.v

@@ -1,14 +1,19 @@
-(* IGLA_GF16_Precision.v — Formal GF16 precision bounds for IGLA RACE *)
-(* Issue: https://github.com/gHashTag/trios/issues/143 *)
+(* SPDX-License-Identifier: Apache-2.0 *)
+(* ================================================================
+   STUB — MOVED TO CANONICAL HOME
 
-Require Import Stdlib.Reals.Reals.
-Require Import CorePhi.
-Open Scope R_scope.
+   This file has been moved to the Trinity Coq Canonical SSOT.
+   The full proof now lives at:
 
-(* GF16 domain *)
-Definition gf16_max : R := 65504.
-Definition gf16_min : R := (-65504).
+     gHashTag/t27/proofs/canonical/igla/INV3_Gf16Precision.v
+       (logical path: Trinity.Canonical.Igla.INV3_Gf16Precision)
 
-(* Theorem: Lucas closure holds (inv-5) *)
-Theorem lucas_closure_gf16 : IZR 256 - (/ (phi ^ 10)) = IZR 256.
-Proof. Admitted.
+   Bundle:        INV-3
+   Title:         GF16 Safe Domain
+   PhD chapter:   Ch.6 GoldenFloat / Ch.9 GF vs MXFP4
+   Census:        github.com/gHashTag/trios/issues/373#issuecomment-4351659821
+   Anchor:        phi^2 + phi^-2 = 3
+   ================================================================ *)
+
+(* Re-export so downstream files keep working without code changes. *)
+From Trinity.Canonical.Igla Require Export INV3_Gf16Precision.

proofs/igla/igla_asha_bound.v

@@ -1,12 +1,19 @@
-(* IGLA_ASHA_Bound.v — Formal ASHA pruning bounds for IGLA RACE *)
+(* SPDX-License-Identifier: Apache-2.0 *)
+(* ================================================================
+   STUB — MOVED TO CANONICAL HOME
 
-Require Import Stdlib.Reals.Reals.
-Require Import CorePhi.
-Open Scope R_scope.
+   This file has been moved to the Trinity Coq Canonical SSOT.
+   The full proof now lives at:
 
-(* ASHA pruning threshold = 3.5 *)
-Definition asha_pruning_threshold : R := 3.5.
+     gHashTag/t27/proofs/canonical/igla/INV2_IglaAshaBound.v
+       (logical path: Trinity.Canonical.Igla.INV2_IglaAshaBound)
 
-(* Theorem: Threshold > 3 *)
-Theorem threshold_above_3 : asha_pruning_threshold > 3.
-Proof. Admitted.
+   Bundle:        INV-2
+   Title:         ASHA Champion Survival
+   PhD chapter:   Ch.13 STROBE / App.E
+   Census:        github.com/gHashTag/trios/issues/373#issuecomment-4351659821
+   Anchor:        phi^2 + phi^-2 = 3
+   ================================================================ *)
+
+(* Re-export so downstream files keep working without code changes. *)
+From Trinity.Canonical.Igla Require Export INV2_IglaAshaBound.

proofs/igla/lr_convergence.v

@@ -1,11 +1,19 @@
-(* IGLA_BPB_Convergence.v — INV-1 *)
+(* SPDX-License-Identifier: Apache-2.0 *)
+(* ================================================================
+   STUB — MOVED TO CANONICAL HOME
 
-Require Import Stdlib.Reals.Reals.
-Require Import CorePhi.
-Open Scope R_scope.
+   This file has been moved to the Trinity Coq Canonical SSOT.
+   The full proof now lives at:
 
-(* BPB decreases with real gradient *)
-Theorem bpb_decreases_with_real_gradient :
-  forall loss1 loss2, loss2 < loss1 -> loss2 < loss1.
-Proof. admit.
-Admitted.
+     gHashTag/t27/proofs/canonical/igla/INV1b_LrPhiOptimality.v
+       (logical path: Trinity.Canonical.Igla.INV1b_LrPhiOptimality)
+
+   Bundle:        INV-1b
+   Title:         lr-phi optimality + lr_convergence
+   PhD chapter:   Ch.10 Coq L1
+   Census:        github.com/gHashTag/trios/issues/373#issuecomment-4351659821
+   Anchor:        phi^2 + phi^-2 = 3
+   ================================================================ *)
+
+(* Re-export so downstream files keep working without code changes. *)
+From Trinity.Canonical.Igla Require Export INV1b_LrPhiOptimality.

proofs/igla/lucas_closure_gf16.v

@@ -1,10 +1,19 @@
-(* lucas_closure_gf16.v — INV-5 *)
+(* SPDX-License-Identifier: Apache-2.0 *)
+(* ================================================================
+   STUB — MOVED TO CANONICAL HOME
 
-Require Import Stdlib.Reals.Reals.
-Require Import CorePhi.
-Open Scope R_scope.
+   This file has been moved to the Trinity Coq Canonical SSOT.
+   The full proof now lives at:
 
-(* Lucas closure theorem *)
-Theorem lucas_closure_gf16 : 0 < phi < 2.
-Proof. admit.
-Admitted.
+     gHashTag/t27/proofs/canonical/igla/INV5_LucasClosureGf16.v
+       (logical path: Trinity.Canonical.Igla.INV5_LucasClosureGf16)
+
+   Bundle:        INV-5
+   Title:         Lucas Closure GF16 (phi^{2n}+phi^{-2n} in Z)
+   PhD chapter:   Ch.6 GoldenFloat
+   Census:        github.com/gHashTag/trios/issues/373#issuecomment-4351659821
+   Anchor:        phi^2 + phi^-2 = 3
+   ================================================================ *)
+
+(* Re-export so downstream files keep working without code changes. *)
+From Trinity.Canonical.Igla Require Export INV5_LucasClosureGf16.