/// Lean 4 → Safe Rust transpilation
/// Source: HeytingLean.HossenfelderNoGo.Networks
/// Provenance: Apoth3osis verified transpilation pipeline

use crate::spacetime::{SpacetimeDisplacement, minkowski_interval, product_norm};

/// A spacetime network with node positions and adjacency.
pub struct SpacetimeNetwork {
    pub positions: Vec<SpacetimeDisplacement>,
    pub adjacency: Vec<Vec<usize>>,
}

impl SpacetimeNetwork {
    /// Relative displacement between nodes u and v.
    pub fn neighbor_displacement(&self, u: usize, v: usize) -> SpacetimeDisplacement {
        SpacetimeDisplacement {
            delta_t: self.positions[v].delta_t - self.positions[u].delta_t,
            delta_x: self.positions[v].delta_x - self.positions[u].delta_x,
        }
    }

    /// Count links from node u within bounded region of radius R.
    pub fn count_links_in_ball(&self, u: usize, radius: f64) -> usize {
        self.adjacency[u]
            .iter()
            .filter(|&&v| {
                let p = &self.positions[u];
                product_norm(p.delta_t, p.delta_x) <= radius
                    && v < self.positions.len()
            })
            .count()
    }

    /// Check if the network satisfies UniformOnHyperbolae for edge (u, v).
    /// Returns false (no finite network can satisfy this for nonzero alpha).
    pub fn check_uniform_on_hyperbolae(&self, u: usize, v: usize) -> bool {
        let d = self.neighbor_displacement(u, v);
        let alpha = minkowski_interval(&d);
        if alpha == 0.0 {
            return true;
        }
        // The theorem proves this is impossible for locally finite networks:
        // the hyperbola has infinitely many points but the network has only
        // finitely many neighbors.
        false
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_neighbor_displacement() {
        let net = SpacetimeNetwork {
            positions: vec![
                SpacetimeDisplacement { delta_t: 0.0, delta_x: 0.0 },
                SpacetimeDisplacement { delta_t: 1.0, delta_x: 2.0 },
            ],
            adjacency: vec![vec![1], vec![0]],
        };
        let d = net.neighbor_displacement(0, 1);
        assert!((d.delta_t - 1.0).abs() < 1e-12);
        assert!((d.delta_x - 2.0).abs() < 1e-12);
    }

    #[test]
    fn test_uniform_on_hyperbolae_impossible() {
        let net = SpacetimeNetwork {
            positions: vec![
                SpacetimeDisplacement { delta_t: 0.0, delta_x: 0.0 },
                SpacetimeDisplacement { delta_t: 0.0, delta_x: 1.0 },
            ],
            adjacency: vec![vec![1], vec![0]],
        };
        // Nonzero interval => impossible
        assert!(!net.check_uniform_on_hyperbolae(0, 1));
    }
}