Function is_proof_net 

pub fn is_proof_net(
    n_nodes: usize,
    fixed_edges: &[(usize, usize)],
    par_switches: &[((usize, usize), (usize, usize))],
) -> bool

Danos-Regnier check: is the proof structure a proof net? n_nodes formula occurrences, the always-present fixed_edges (axiom / cut / ⊗ links), and the par_switches (each a pair of candidate edges for one ⅋, one chosen per switching). Returns true iff EVERY switching graph is a tree. Bounded by MAX_PN_NODES / MAX_PN_PARS.