Ramos and Sun conjectured that a failure of log-concavity in a tree's independence sequence at distance β below N/2 forces the independence number to be at least N/2+β+1. The task is to construct trees with perfect matchings that fail log-concavity at prescribed, or at several simultaneous, distances from the independence number α.

Trees are built from a directed label tree by doubling each label into a matched pair and adding an edge for each arrow. Independent sets are then counted through sign assignments over empty matching pairs. Explicit exponential estimates on these counts give the failures, and a general sufficient condition is stated in terms of a fixed oriented core tree and leaf multiplicities. The parameterized results, their quantitative bounds, and the 90-vertex example are formalized in Lean 4 with Mathlib.

For every k≥1 there is a family of trees with α=N/2 that fails log-concavity at α−k, with a witness of order O(k^2 log k). For every t≥2 a single tree fails at α−1, α−3, …, α−(2t−1), with a witness of order O(t^3). These trees refute Conjecture 4.2 of Ramos and Sun, and the log-concavity ratio decays geometrically as the trees grow. The explicit 90-vertex counterexample has a_44^2 − a_43·a_45 < 0.