aprender-core 0.29.2

// CONTRACT: graph-centrality-v1.yaml
// HASH: sha256:a1b2c3d4e5f67890
// Generated by: pv probar --binding
// DO NOT EDIT — regenerate with `pv probar --binding`

use aprender::graph::{Graph, GraphCentrality};
use proptest::prelude::*;

proptest! {
    /// FALSIFY-GC-001: Degree centrality bounded (C_D ∈ [0, 1])
    /// Formal: 0 ≤ C_D(v) ≤ 1 for all v
    #[test]
    fn prop_degree_centrality_bounded(
        n in 3usize..20,
        edge_count in 1usize..30
    ) {
        // Generate random edges for an undirected graph
        let edges: Vec<(usize, usize)> = (0..edge_count)
            .map(|i| (i % n, (i * 7 + 3) % n))
            .filter(|&(a, b)| a != b)
            .collect();
        if edges.is_empty() {
            return Ok(());
        }
        let g = Graph::from_edges(&edges, false);
        let centrality = g.degree_centrality();

        for (&node, &c_d) in &centrality {
            prop_assert!(
                c_d >= 0.0,
                "FALSIFY-GC-001: degree_centrality[{node}]={c_d} < 0"
            );
            prop_assert!(
                c_d <= 1.0 + 1e-10,
                "FALSIFY-GC-001: degree_centrality[{node}]={c_d} > 1"
            );
        }
    }

    /// FALSIFY-GC-002: Betweenness non-negative (C_B ≥ 0)
    /// Formal: C_B(v) ≥ 0 for all v
    #[test]
    fn prop_betweenness_non_negative(
        n in 3usize..12
    ) {
        // Create a random tree-like graph (path with extra edges)
        let mut edges: Vec<(usize, usize)> = (0..n - 1).map(|i| (i, i + 1)).collect();
        // Add a shortcut to make it interesting
        if n > 3 {
            edges.push((0, n - 1));
        }
        let g = Graph::from_edges(&edges, false);
        let betweenness = g.betweenness_centrality();

        for (i, &c_b) in betweenness.iter().enumerate() {
            prop_assert!(
                c_b >= 0.0,
                "FALSIFY-GC-002: betweenness[{i}]={c_b} < 0"
            );
        }
    }

    /// FALSIFY-GC-003: Eigenvector non-negativity (x_v ≥ 0 for connected graph)
    /// Formal: x_v ≥ 0 for all v in a connected undirected graph (Perron-Frobenius)
    #[test]
    fn prop_eigenvector_non_negative_connected(
        n in 3usize..15
    ) {
        // Create a connected graph: cycle ensures connectivity
        let mut edges: Vec<(usize, usize)> = (0..n).map(|i| (i, (i + 1) % n)).collect();
        // Add a chord for variety
        if n > 4 {
            edges.push((0, n / 2));
        }
        let g = Graph::from_edges(&edges, false);
        let eigenvec = g.eigenvector_centrality(200, 1e-8)
            .expect("eigenvector_centrality converges on connected graph");

        for (i, &x_v) in eigenvec.iter().enumerate() {
            prop_assert!(
                x_v >= -1e-10,
                "FALSIFY-GC-003: eigenvector[{i}]={x_v} < 0 on connected graph"
            );
        }
    }

    /// FALSIFY-GC-004: Complete graph symmetry (all nodes have equal centrality)
    /// Formal: K_n → C_D(v) = C_D(u) for all u, v
    #[test]
    fn prop_complete_graph_symmetry(
        n in 3usize..10
    ) {
        // Build complete graph K_n
        let mut edges = Vec::new();
        for i in 0..n {
            for j in (i + 1)..n {
                edges.push((i, j));
            }
        }
        let g = Graph::from_edges(&edges, false);

        // Degree centrality: all nodes must be equal (= 1.0 for K_n)
        let centrality = g.degree_centrality();
        let values: Vec<f64> = (0..n).map(|v| centrality[&v]).collect();
        let first = values[0];
        for (i, &val) in values.iter().enumerate() {
            prop_assert!(
                (val - first).abs() < 1e-10,
                "FALSIFY-GC-004: degree_centrality[{i}]={val} != degree_centrality[0]={first} in K_{n}"
            );
        }

        // Betweenness: all nodes must be equal in K_n
        let betweenness = g.betweenness_centrality();
        let b_first = betweenness[0];
        for (i, &b_val) in betweenness.iter().enumerate() {
            prop_assert!(
                (b_val - b_first).abs() < 1e-10,
                "FALSIFY-GC-004: betweenness[{i}]={b_val} != betweenness[0]={b_first} in K_{n}"
            );
        }

        // Eigenvector: all nodes must be equal in K_n
        let eigenvec = g.eigenvector_centrality(200, 1e-8)
            .expect("eigenvector_centrality converges on K_n");
        let e_first = eigenvec[0];
        for (i, &e_val) in eigenvec.iter().enumerate() {
            prop_assert!(
                (e_val - e_first).abs() < 1e-6,
                "FALSIFY-GC-004: eigenvector[{i}]={e_val} != eigenvector[0]={e_first} in K_{n}"
            );
        }

        // Harmonic: all nodes must be equal in K_n
        let harmonic = g.harmonic_centrality();
        let h_first = harmonic[0];
        for (i, &h_val) in harmonic.iter().enumerate() {
            prop_assert!(
                (h_val - h_first).abs() < 1e-10,
                "FALSIFY-GC-004: harmonic[{i}]={h_val} != harmonic[0]={h_first} in K_{n}"
            );
        }
    }

    /// FALSIFY-GC-005: Star graph degree (center has degree centrality = 1)
    /// Formal: S_n → C_D(center) = 1.0
    #[test]
    fn prop_star_graph_center_degree(
        n in 3usize..20
    ) {
        // Star graph: node 0 is the center, connected to all others
        let edges: Vec<(usize, usize)> = (1..n).map(|i| (0, i)).collect();
        let g = Graph::from_edges(&edges, false);
        let centrality = g.degree_centrality();

        let center_degree = centrality[&0];
        prop_assert!(
            (center_degree - 1.0).abs() < 1e-10,
            "FALSIFY-GC-005: star center degree_centrality={center_degree}, expected 1.0 for S_{n}"
        );

        // Leaf nodes should have degree centrality = 1/(n-1)
        let expected_leaf = 1.0 / (n - 1) as f64;
        for leaf in 1..n {
            let leaf_degree = centrality[&leaf];
            prop_assert!(
                (leaf_degree - expected_leaf).abs() < 1e-10,
                "FALSIFY-GC-005: star leaf[{leaf}] degree={leaf_degree}, expected {expected_leaf}"
            );
        }
    }

    /// FALSIFY-GC-006: Harmonic bounded (C_H ∈ [0, 1] when normalized)
    /// Formal: 0 ≤ H(v) / (n-1) ≤ 1 for all v
    /// Raw harmonic centrality is sum(1/d(v,u)) which has maximum n-1
    /// (when all nodes are at distance 1). Normalized: H(v)/(n-1) ∈ [0, 1].
    #[test]
    fn prop_harmonic_bounded(
        n in 3usize..15,
        edge_count in 1usize..30
    ) {
        // Generate random edges for an undirected graph
        let edges: Vec<(usize, usize)> = (0..edge_count)
            .map(|i| (i % n, (i * 11 + 5) % n))
            .filter(|&(a, b)| a != b)
            .collect();
        if edges.is_empty() {
            return Ok(());
        }
        let g = Graph::from_edges(&edges, false);
        let harmonic = g.harmonic_centrality();
        let num_nodes = harmonic.len();

        if num_nodes <= 1 {
            return Ok(());
        }

        let norm = (num_nodes - 1) as f64;

        for (i, &h_v) in harmonic.iter().enumerate() {
            // Raw harmonic must be non-negative
            prop_assert!(
                h_v >= -1e-10,
                "FALSIFY-GC-006: harmonic[{i}]={h_v} < 0"
            );
            // Normalized harmonic must be ≤ 1
            let h_normalized = h_v / norm;
            prop_assert!(
                h_normalized <= 1.0 + 1e-10,
                "FALSIFY-GC-006: harmonic[{i}]/{norm} = {h_normalized} > 1"
            );
        }
    }
}