diff --git a/assertions/igla_assertions.json b/assertions/igla_assertions.json index aedefa900a..72d1c5c113 100644 --- a/assertions/igla_assertions.json +++ b/assertions/igla_assertions.json @@ -140,7 +140,8 @@ "invariant_count": 9, "last_updated": "2026-04-25T16:50:00Z", "last_updated_by": "perplexity-computer-l13", - "scaffold_inv_13_15_added": "#465 App.K Agent Memory scaffold (status=wip; admitted_budget=5/5 LOCKED; no Coq files created)" + "scaffold_inv_13_15_added": "#465 App.K Agent Memory scaffold (status=wip; admitted_budget=5/5 LOCKED; no Coq files created)", + "inv_6_hybrid_qk_gain_added": "#441 Phase-5 scaffold via PR #490 (status=wip; 3 axioms recorded; admitted_budget=5/5 LOCKED preserved)" }, "trinity_identity": "\u03c6\u00b2 + \u03c6\u207b\u00b2 = 3", "nca_loss_weight": 0.25, @@ -348,6 +349,31 @@ "ema_decay_upper": 1.0 } }, + { + "id": "INV-6-HybridQkGain", + "name": "hybrid_qk_gain_phi_bound", + "coq_theorem": "inv6_hybrid_qk_gain_from_axiom", + "coq_file": "docs/phd/theorems/igla/INV6_HybridQkGain.v", + "status": "wip", + "axioms_used": [ + "hybrid_gain_phi_bound", + "gain_baseline_nonneg", + "gain_hybrid_nonneg" + ], + "description": "Hybrid-QK attention gain is phi-bounded from below: gain_hybrid(k) >= gain_baseline(k) * phi^(-1). Phase-5 #441 entity. Distinct from the existing Proven INV-6 ema_decay_valid \u2014 the id suffix '-HybridQkGain' disambiguates the collision until Phase-5 settles on a final number.", + "note": "CIRCULAR: theorem inv6_hybrid_qk_gain_from_axiom restates the axiom hybrid_gain_phi_bound (proof body is `exact (axiom k)`). The functional invariant is postulated, not derived. Phase-5 #441 closure replaces the axiom with a sqrt_le_compat derivation per the strategy in the issue body; until then, status remains `wip`. admitted_budget=5/5 LOCKED untouched (axioms != Admitted, but axioms_used is recorded explicitly).", + "phase": "5-scaffold-only", + "issue_ref": "https://github.com/gHashTag/trios/issues/441", + "scaffold_pr": "https://github.com/gHashTag/trios/pull/490", + "follow_up_pr": "TBD \u2014 must replace Axiom hybrid_gain_phi_bound with derivation", + "trinity_link": "Connects to architectural floor proof (arch_floor_bpb = 2 + phi^(-2)) per #441 corollary", + "runtime_check": { + "action": "warn", + "message": "INV-6-HybridQkGain: hybrid_gain_phi_bound is an axiom, not a derived theorem" + }, + "runtime_target": "crates/trios-igla-race/src/bin/qk_gain_check.rs (Rust guard already binding)", + "naming_collision": "id 'INV-6' already taken by ema_decay_valid (Proven). Issue #441 titled this work 'INV-6 HybridQkGain' but it is a separate entity; the suffix preserves both." + }, { "id": "INV-7", "name": "igla_found_criterion", diff --git a/docs/phd/theorems/igla/INV6_HybridQkGain.v b/docs/phd/theorems/igla/INV6_HybridQkGain.v new file mode 100644 index 0000000000..0784807164 --- /dev/null +++ b/docs/phd/theorems/igla/INV6_HybridQkGain.v @@ -0,0 +1,214 @@ +(* INV6_HybridQkGain.v — Formal proof of Hybrid Qk Gain invariant *) +(* Issue: https://github.com/gHashTag/trios/issues/441 *) +(* Author: Trinity Research Group | Date: 2026-05-02 *) +(* *) +(* INVARIANT 6: HybridQkGain *) +(* The hybrid attention gain Q_k satisfies: *) +(* gain_hybrid(k) >= gain_baseline(k) * phi^(-1) *) +(* where phi = (1 + sqrt(5)) / 2 is the golden ratio. *) +(* This formalizes that Hybrid-QK never loses more than 1/phi *) +(* relative to the baseline attention mechanism. *) +(* ==================================================================== *) + +Require Import Coq.Reals.Reals. +Require Import Coq.Reals.ROrderedType. +Require Import Coq.micromega.Lra. +Require Import CorePhi. +(* CorePhi exports: phi, phi_pos, phi_nonzero, phi_quadratic, *) +(* phi_square, phi_inv, phi_inv_sq, trinity_identity, *) +(* phi_between_1_618_and_1_619 *) +Open Scope R_scope. + +(* ==================================================================== *) +(* SECTION 1: Definitions *) +(* ==================================================================== *) + +(* Attention gain for a single key k under baseline mechanism *) +Parameter gain_baseline : nat -> R. + +(* Attention gain for a single key k under hybrid mechanism *) +Parameter gain_hybrid : nat -> R. + +(* Baseline gains are non-negative *) +Axiom gain_baseline_nonneg : forall k : nat, gain_baseline k >= 0. + +(* Hybrid gains are non-negative *) +Axiom gain_hybrid_nonneg : forall k : nat, gain_hybrid k >= 0. + +(* Phi lower bound for hybrid gain — this is the core invariant *) +Axiom hybrid_gain_phi_bound : + forall k : nat, + gain_hybrid k >= gain_baseline k * (/ phi). + +(* ==================================================================== *) +(* SECTION 2: Core Lemmas *) +(* ==================================================================== *) + +(* Lemma: phi is positive — directly from CorePhi.phi_pos *) +Lemma phi_pos_local : phi > 0. +Proof. + exact phi_pos. +Qed. + +(* Lemma: 1/phi is strictly between 0 and 1 *) +Lemma inv_phi_in_unit : 0 < / phi < 1. +Proof. + split. + - (* 0 < 1/phi because phi > 0 *) + apply Rinv_pos. + exact phi_pos. + - (* 1/phi < 1 because phi > 1 *) + (* From CorePhi: 1.618 < phi, so phi > 1, so 1/phi < 1 *) + rewrite <- Rinv_1. + apply Rinv_lt_contravar. + + lra. + + pose proof phi_between_1_618_and_1_619 as [Hlo _]. + lra. +Qed. + +(* Lemma: 1/phi > 0 (convenience) *) +Lemma inv_phi_pos : / phi > 0. +Proof. + exact (proj1 inv_phi_in_unit). +Qed. + +(* Lemma: Hybrid gain never drops to zero if baseline is positive *) +Lemma hybrid_gain_positive : + forall k : nat, + gain_baseline k > 0 -> + gain_hybrid k > 0. +Proof. + intros k H_pos. + apply Rlt_le_trans with (gain_baseline k * (/ phi)). + - apply Rmult_gt_0_compat. + + exact H_pos. + + exact inv_phi_pos. + - exact (hybrid_gain_phi_bound k). +Qed. + +(* ==================================================================== *) +(* SECTION 3: Main Invariant Theorem *) +(* ==================================================================== *) + +(* Theorem INV6 (CIRCULAR): Hybrid Qk Gain is phi-bounded from below. *) +(* *) +(* HONEST DISCLOSURE (R5): *) +(* The proof body is `exact (hybrid_gain_phi_bound k)` — i.e. this *) +(* theorem restates the homonymous Axiom from Section 1. The Qed *) +(* tells us nothing beyond what Axiom already postulates. The naming *) +(* suffix `_from_axiom` documents this in-source so reviewers cannot *) +(* mistake it for a derived result. *) +(* *) +(* Phase-5 #441 closure replaces `Axiom hybrid_gain_phi_bound` with a *) +(* real derivation from `gain(d) = sqrt(d) / sqrt(d_model_min)` via *) +(* `Coq.Reals.sqrt_le_compat` plus INV-3 `d >= d_model_min`. Until *) +(* that follow-up PR lands, status remains `wip` in *) +(* `assertions/igla_assertions.json::INV-6-HybridQkGain`. *) +Theorem inv6_hybrid_qk_gain_from_axiom : + forall k : nat, + gain_hybrid k >= gain_baseline k * (/ phi). +Proof. + intro k. + exact (hybrid_gain_phi_bound k). +Qed. + +(* Theorem: Hybrid gain degradation ratio is bounded by 1/phi *) +Theorem hybrid_gain_degradation_bounded : + forall k : nat, + gain_baseline k > 0 -> + gain_hybrid k / gain_baseline k >= / phi. +Proof. + intros k H_pos. + unfold Rdiv. + apply Rmult_le_reg_r with (gain_baseline k). + - exact H_pos. + - rewrite Rmult_assoc, Rinv_l, Rmult_1_r. + + exact (hybrid_gain_phi_bound k). + + lra. +Qed. + +(* ==================================================================== *) +(* SECTION 4: Monotonicity *) +(* ==================================================================== *) + +(* If baseline gains are ordered, hybrid gain at k1 + times phi is bounded by hybrid gain at k2 plus baseline at k2 *) +Lemma hybrid_monotone_from_baseline : + forall k1 k2 : nat, + gain_baseline k1 <= gain_baseline k2 -> + gain_hybrid k1 * phi <= gain_hybrid k2 * phi + gain_baseline k2. +Proof. + intros k1 k2 H_mono. + (* gain_hybrid k1 >= gain_baseline k1 * /phi + gain_hybrid k2 >= gain_baseline k2 * /phi + We want: gain_hybrid k1 * phi <= gain_hybrid k2 * phi + gain_baseline k2. + It suffices to show: + (gain_baseline k1 * /phi) * phi <= (gain_baseline k2 * /phi) * phi + gain_baseline k2 + = gain_baseline k1 <= gain_baseline k2 + gain_baseline k2 + = gain_baseline k1 <= 2 * gain_baseline k2, which follows from + gain_baseline k1 <= gain_baseline k2 <= 2 * gain_baseline k2 *) + apply Rle_trans + with (gain_baseline k1 * (/ phi) * phi). + - (* gain_hybrid k1 * phi >= gain_baseline k1 * /phi * phi *) + apply Rmult_le_compat_r. + + lra. + + exact (hybrid_gain_phi_bound k1). + - (* gain_baseline k1 * /phi * phi = gain_baseline k1 *) + rewrite <- Rmult_assoc, Rinv_l, Rmult_1_l + by exact phi_nonzero. + (* goal: gain_baseline k1 <= gain_hybrid k2 * phi + gain_baseline k2 *) + apply Rle_trans with gain_baseline k2. + + exact H_mono. + + (* gain_baseline k2 <= gain_hybrid k2 * phi + gain_baseline k2 *) + lra. +Qed. + +(* ==================================================================== *) +(* SECTION 5: Connection to IGLA *) +(* ==================================================================== *) + +(* The IGLA scheduler relies on INV6 to guarantee that + hybrid attention heads don't collapse during training. + This theorem bridges INV6 to the ASHA pruning bound (INV2). *) +Theorem inv6_supports_asha_stability : + forall k : nat, + gain_baseline k > 0 -> + exists eps : R, eps > 0 /\ gain_hybrid k >= eps. +Proof. + intros k H_pos. + exists (gain_baseline k * (/ phi)). + split. + - apply Rmult_gt_0_compat. + + exact H_pos. + + exact inv_phi_pos. + - exact (hybrid_gain_phi_bound k). +Qed. + +(* ==================================================================== *) +(* Export / Certification *) +(* ==================================================================== *) + +(* HONEST DISCLOSURE (R5): *) +(* `inv6_theorems_certified` is satisfied modulo the three Section 1 *) +(* axioms (`hybrid_gain_phi_bound`, `gain_baseline_nonneg`, *) +(* `gain_hybrid_nonneg`). No `Admitted.` remains, but the central *) +(* bound is postulated rather than derived. Phase-5 #441 closure *) +(* replaces the bound axiom with a derivation; until then the catalog *) +(* tracks status=wip in `assertions/igla_assertions.json` *) +(* under id `INV-6-HybridQkGain`. *) +Definition inv6_theorems_certified : Prop := + (forall k, gain_hybrid k >= gain_baseline k * (/ phi)) /\ + (forall k, gain_baseline k > 0 -> gain_hybrid k > 0) /\ + (forall k, gain_baseline k > 0 -> + exists eps : R, eps > 0 /\ gain_hybrid k >= eps). + +Lemma inv6_all_certified : inv6_theorems_certified. +Proof. + unfold inv6_theorems_certified. + repeat split. + - intro k. exact (hybrid_gain_phi_bound k). + - intros k H. exact (hybrid_gain_positive k H). + - intros k H. exact (inv6_supports_asha_stability k H). +Qed. + +(* QED — INV6 fully certified *) diff --git a/docs/phd/theorems/igla/_CoqProject b/docs/phd/theorems/igla/_CoqProject index eebb49ebd0..6defc2de39 100644 --- a/docs/phd/theorems/igla/_CoqProject +++ b/docs/phd/theorems/igla/_CoqProject @@ -8,4 +8,5 @@ igla/IGLA_BPB_Convergence.v igla/IGLA_ASHA_Bound.v igla/IGLA_GF16_Precision.v igla/IGLA_NCA_Entropy.v +igla/INV6_HybridQkGain.v igla/IGLA_Catalog.v