mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
allaun
c121291c57
Theorem restated with crossInputGap hypothesis (no active bin from s adjacent to active bin from e). Without this, the theorem is false: counterexample s=[1,0,1,0,...] e=[0,0,0,1,0,1,...] has merge with adjacent active bins despite resonanceDegeneracy=0. Added to Spectrum.lean: - crossInputGap: cross-input adjacency check on adjacent bin pairs Added to GraphRank.lean: - boolGap8: boolean gap check on 8 explicit values - Complete mathematical proof sketch in docstring (4 steps) The sorry remains: the Q16_16↔Bool bridge for 8-element lists requires list-level induction on activeBins/verifySpectralGap/resonanceDegeneracy/ crossInputGap. The boolean kernel (boolGap8) is defined and ready for native_decide verification once the bridge is automated. Build: 3314 jobs, 0 errors (Compiler surface)
90 lines
4 KiB
Text
90 lines
4 KiB
Text
import Semantics.FixedPoint
|
||
import Semantics.GeneticCode
|
||
|
||
namespace Semantics.Spectrum
|
||
|
||
/-! # Spectral Encoding
|
||
Derived from the Erdős #1196 solution via piecewise eigenvector construction.
|
||
All scalars use Q16_16 fixed-point for hardware-native neuromorphic execution.
|
||
-/
|
||
|
||
/-- Default number of spectral bins. -/
|
||
def binCount : Nat := 8
|
||
|
||
/-- A spectral signature is a finite vector of amplitudes. -/
|
||
structure SpectralSignature where
|
||
bins : List Q16_16
|
||
deriving Repr, BEq, DecidableEq
|
||
|
||
namespace SpectralSignature
|
||
|
||
def empty : SpectralSignature := ⟨List.replicate binCount Q16_16.zero⟩
|
||
|
||
def activeBins (sig : SpectralSignature) : List (Nat × Q16_16) :=
|
||
(List.zip (List.range sig.bins.length) sig.bins).filter (λ p => p.2 != Q16_16.zero)
|
||
|
||
/-- Peak distance in bin index space. -/
|
||
def peakDistance (i j : Nat) : Nat :=
|
||
if i > j then i - j else j - i
|
||
|
||
/-- Erdős-Hooley constant δ ≈ 0.08607 as Q16_16.
|
||
Computed as 5643 / 65536 ≈ 0.08609 (within 0.02% of true value). -/
|
||
def erdosHooleyDelta : Q16_16 := Q16_16.ofRawInt 5643 -- 5643/65536 ≈ 0.08609 (within 0.02% of true δ ≈ 0.08607)
|
||
#eval erdosHooleyDelta -- Expected: raw 5643
|
||
|
||
/-- Verify no two active peaks are adjacent (minimum separation = 1 bin). -/
|
||
def verifySpectralGap (sig : SpectralSignature) : Bool :=
|
||
let active := sig.activeBins.map (λ p => p.1)
|
||
active.all (λ i => active.all (λ j => i == j || peakDistance i j > 1))
|
||
|
||
/-- Map an event to a discrete spectral signature (one peak per base).
|
||
Each base type (a, t, g, c) gets a unique spectral peak position.
|
||
This creates a spectral barcode for genetic event encoding. -/
|
||
def eventSpectrum : Semantics.GeneticCode.EventType → SpectralSignature
|
||
| Semantics.GeneticCode.EventType.a => { bins := [Q16_16.one, Q16_16.zero, Q16_16.zero,
|
||
Q16_16.zero, Q16_16.zero, Q16_16.zero,
|
||
Q16_16.zero, Q16_16.zero] }
|
||
| Semantics.GeneticCode.EventType.t => { bins := [Q16_16.zero, Q16_16.one, Q16_16.zero,
|
||
Q16_16.zero, Q16_16.zero, Q16_16.zero,
|
||
Q16_16.zero, Q16_16.zero] }
|
||
| Semantics.GeneticCode.EventType.g => { bins := [Q16_16.zero, Q16_16.zero, Q16_16.one,
|
||
Q16_16.zero, Q16_16.zero, Q16_16.zero,
|
||
Q16_16.zero, Q16_16.zero] }
|
||
| Semantics.GeneticCode.EventType.c => { bins := [Q16_16.zero, Q16_16.zero, Q16_16.zero,
|
||
Q16_16.one, Q16_16.zero, Q16_16.zero,
|
||
Q16_16.zero, Q16_16.zero] }
|
||
|
||
/-- Compute spectral overlap (inner product) between two signatures. -/
|
||
def spectralOverlap (sig1 sig2 : SpectralSignature) : Q16_16 :=
|
||
List.zipWith (λ a b => Q16_16.mul a b) sig1.bins sig2.bins
|
||
|>.foldl (λ acc x => Q16_16.add acc x) Q16_16.zero
|
||
|
||
/-- Piecewise eigenvector merge: superposition with saturation. -/
|
||
def piecewiseMerge (left right : SpectralSignature) : SpectralSignature :=
|
||
let merged := List.zipWith (λ a b => Q16_16.min Q16_16.one (Q16_16.add a b)) left.bins right.bins
|
||
⟨merged⟩
|
||
|
||
/-- Count resonance degeneracy (overlapping non-zero bins). -/
|
||
def resonanceDegeneracy (left right : SpectralSignature) : Nat :=
|
||
List.zipWith (λ a b => if a != Q16_16.zero && b != Q16_16.zero then 1 else 0) left.bins right.bins
|
||
|>.foldl Nat.add 0
|
||
|
||
/-- Density bound predicate: active bins must not exceed threshold. -/
|
||
def withinDensityBound (sig : SpectralSignature) (maxActive : Nat) : Bool :=
|
||
sig.activeBins.length ≤ maxActive
|
||
|
||
/-- Cross-input gap: no active bin in `left` is adjacent to an active bin in `right`.
|
||
For each adjacent pair (i, i+1), neither left[i]∧right[i+1] nor right[i]∧left[i+1]
|
||
may both be non-zero. -/
|
||
def crossInputGap (left right : SpectralSignature) : Bool :=
|
||
let la := left.bins.map (· != Q16_16.zero)
|
||
let lb := right.bins.map (· != Q16_16.zero)
|
||
let n := min la.length lb.length
|
||
(List.range (n - 1)).all fun i =>
|
||
match la[i]?, lb[i+1]?, lb[i]?, la[i+1]? with
|
||
| some a, some bNext, some b, some aNext => !(a && bNext) && !(b && aNext)
|
||
| _, _, _, _ => true
|
||
|
||
end SpectralSignature
|
||
|
||
end Semantics.Spectrum
|