allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(lean): attempt canonicalize+native_decide for gap_pat_bridge

Browse source 
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
This commit is contained in:
allaun 2026-06-22 14:12:02 -05:00
parent 8e29ea6592
commit 70bdfb5c2a
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean
View file

@ -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`.