Witness geometry

A direct force-magnitude form of the one-dimensional barrier-asymmetry claim: at equal distances from the minimum, different quadratic curvatures give different restoring-force magnitudes.

theorem barrier_asymmetry_direct (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a ≠ b) (x : ℝ) (hx : 0 < x) : |-2 * a * -x| ≠ |-2 * b * x|

Direct force-magnitude form of the one-dimensional barrier-asymmetry claim: at equal distances from the minimum, different quadratic curvatures produce different restoring-force magnitudes.