From 70bdfb5c2a55150a1df6e70ca74a9e65c263ee42 Mon Sep 17 00:00:00 2001 From: allaun Date: Mon, 22 Jun 2026 14:12:02 -0500 Subject: [PATCH] fix(lean): attempt canonicalize+native_decide for gap_pat_bridge MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit native_decide +revert fails on Q16_16 (Subtype Int, infinite type). gapQ16_canonical (verified) proves the computation works on {zero,one}. The bridge from arbitrary Q16_16 to canonical values requires proving predicate invariance under canonicalization — which is the same lemma. The fundamental chicken-and-egg: to use native_decide, we need finite values. To get finite values, we canonicalize. To prove canonicalization preserves predicates, we need the bridge. The bridge is the lemma we are trying to prove. 7 bridge sorries remain, all list-induction over 8 elements. Build: 3314 jobs, 0 errors --- 0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean b/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean index 7a39c688..5546d514 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean @@ -1,7 +1,6 @@ import Semantics.Spectrum -/-! -# GraphRank — Spectral-gap-gated ranking on social graphs +/-! # GraphRank — Spectral-gap-gated ranking on social graphs Maps the PageRank/HITS/Fiedler/PPR mathematical lineage onto the 8-bin Sidon spectral space from `Semantics.Spectrum`.