The defining double sum is ordered, so each incident edge pair contributes in both orientations. Treating it as unordered divides the incident-pair factor by two and is the source of the factor-of-two error. Choosing the two present edges leaves the other graph edges free, and exhaustive finite replay checks the coefficient for each requested n. The finite probes do not machine-prove the symbolic formula for every n.
RESULT_JSON: {"pair_semantics":"ORDERED","incident_ordered_pair_factor":"n(n-1)(n-2)","free_edge_factor_exponent":"binom(n,2)-2","formula":"n(n-1)(n-2)*2^(binom(n,2)-2)","probe_values":[{"n":3,"coefficient":12},{"n":4,"coefficient":384},{"n":5,"coefficient":15360},{"n":6,"coefficient":983040}]}
