From 08ef5932b916a8f7be3a6fad4bce65aa04bdff92 Mon Sep 17 00:00:00 2001 From: trinity-canonical Date: Thu, 30 Apr 2026 10:37:15 +0000 Subject: [PATCH] =?UTF-8?q?feat(canonical):=20=F0=9F=8C=BB=20Stub=20mirror?= =?UTF-8?q?=20files=20=E2=86=92=20Require=20Export=20Trinity.Canonical.*?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Companion PR to gHashTag/t27#569 (CANONICAL COQ HOME). After Coq census (trios#373) found 376 Qed across 65 canonical .v files in 3 repos, t27/proofs/canonical/ is now the single source of truth for all Trinity Coq theorems. This PR replaces 7 mirror files in trinity-clara/proofs/igla/ with thin stubs that 'Require Export Trinity.Canonical.Igla.' so downstream code keeps working. Stubs replaced (7 files): - proofs/igla/CorePhi.v → Trinity.Canonical.Sacred.CorePhi - proofs/igla/bpb_monotone_backward.v → Trinity.Canonical.Igla.INV1_BpbMonotoneBackward - proofs/igla/gf16_precision.v → Trinity.Canonical.Igla.INV3_Gf16Precision - proofs/igla/igla_asha_bound.v → Trinity.Canonical.Igla.INV2_IglaAshaBound - proofs/igla/lr_convergence.v → Trinity.Canonical.Igla.INV1b_LrPhiOptimality - proofs/igla/lucas_closure_gf16.v → Trinity.Canonical.Igla.INV5_LucasClosureGf16 - proofs/igla/nca_entropy_band.v → Trinity.Canonical.Igla.INV4_NcaEntropyBand Files NOT stubbed (canonical winners — proofs stay here as primary): - proofs/igla_asha_bound.v (root) — INV-2 winner (13 Qed) - proofs/igla/hybrid_qk_gain.v — INV-6 winner - proofs/igla/igla_found_criterion.v — INV-7 winner Each stub carries SPDX, bundle ID, PhD chapter slot, census reference. 'Require Export' preserves downstream import compatibility. Anchor: phi^2 + phi^-2 = 3 Census: github.com/gHashTag/trios/issues/373#issuecomment-4351659821 Co-authored-by: AI-assisted code generation --- proofs/igla/CorePhi.v | 38 ++--- proofs/igla/bpb_monotone_backward.v | 208 ++-------------------------- proofs/igla/gf16_precision.v | 27 ++-- proofs/igla/igla_asha_bound.v | 25 ++-- proofs/igla/lr_convergence.v | 26 ++-- proofs/igla/lucas_closure_gf16.v | 25 ++-- proofs/igla/nca_entropy_band.v | 26 ++-- 7 files changed, 110 insertions(+), 265 deletions(-) diff --git a/proofs/igla/CorePhi.v b/proofs/igla/CorePhi.v index 36f431a..4c65dbd 100644 --- a/proofs/igla/CorePhi.v +++ b/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. diff --git a/proofs/igla/bpb_monotone_backward.v b/proofs/igla/bpb_monotone_backward.v index 1580eec..b51a834 100644 --- a/proofs/igla/bpb_monotone_backward.v +++ b/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. diff --git a/proofs/igla/gf16_precision.v b/proofs/igla/gf16_precision.v index 59c32de..f78d0f2 100644 --- a/proofs/igla/gf16_precision.v +++ b/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. diff --git a/proofs/igla/igla_asha_bound.v b/proofs/igla/igla_asha_bound.v index dd0624e..174d50c 100644 --- a/proofs/igla/igla_asha_bound.v +++ b/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. diff --git a/proofs/igla/lr_convergence.v b/proofs/igla/lr_convergence.v index 763f62c..291a0cb 100644 --- a/proofs/igla/lr_convergence.v +++ b/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. diff --git a/proofs/igla/lucas_closure_gf16.v b/proofs/igla/lucas_closure_gf16.v index 2976881..78d0d03 100644 --- a/proofs/igla/lucas_closure_gf16.v +++ b/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. diff --git a/proofs/igla/nca_entropy_band.v b/proofs/igla/nca_entropy_band.v index 0952316..a1a29c8 100644 --- a/proofs/igla/nca_entropy_band.v +++ b/proofs/igla/nca_entropy_band.v @@ -1,13 +1,19 @@ -(* IGLA_NCA_Entropy.v — Formal NCA entropy band invariants *) +(* 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: -(* Entropy band [1.5, 2.8] *) -Definition entropy_min : R := 1.5. -Definition entropy_max : R := 2.8. + gHashTag/t27/proofs/canonical/igla/INV4_NcaEntropyBand.v + (logical path: Trinity.Canonical.Igla.INV4_NcaEntropyBand) -(* Theorem: Band non-empty *) -Theorem entropy_band_non_empty : entropy_min < entropy_max. -Proof. Admitted. + Bundle: INV-4 + Title: NCA Entropy Band 1.5..2.8 (81=3^4) + PhD chapter: Ch.10 Coq L1 / Ch.16 360-lane + 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 INV4_NcaEntropyBand.