vertexConformal_rectangle_log_strain_forces_square
plain-language theorem explainer
If four vertex potentials induce equal opposite-edge averages on a rectangle (horizontal mean h, vertical mean v), then necessarily h = v. Anyone separating the conformal scalar slice from pure shear in the weak-field Regge sector cites this obstruction. The proof is a one-line linear-arithmetic identity on the four averaging equations.
Claim. Let $\xi_a,\xi_b,\xi_c,\xi_d,h,v\in\mathbb{R}$. If $(\xi_a+\xi_b)/2=h$, $(\xi_c+\xi_d)/2=h$, $(\xi_b+\xi_c)/2=v$, and $(\xi_d+\xi_a)/2=v$, then $h=v$.
background
Track 1.D isolates the tensor/shear sector of the discrete weak-field metric. Track 1.B assigns one real potential to each vertex and induces edge log-strains by averaging the two endpoint potentials. That conformal ansatz is a scalar slice: it cannot represent pure shear, so it cannot by itself cover transverse-traceless gravitational-wave modes.
Here a conformal edge log-strain on an edge is exactly the arithmetic mean of the two endpoint potentials. For a quadrilateral labeled a-b-c-d, the two opposite "horizontal" edges are forced to a common mean $h$ and the two opposite "vertical" edges to a common mean $v$. The elementary algebraic question is whether $h$ and $v$ can differ.
The module separates independent edge perturbations from vertex-conformal ones and records this rectangle obstruction as the first hard constraint on the conformal ansatz.
proof idea
Four real averaging equations are given. Linear arithmetic (linarith) closes the goal $h=v$ directly: adding the two horizontal equations and the two vertical equations yields the same sum of all four potentials on each side, so the means coincide. No geometric lemmas are invoked; the identity is pure equational reasoning on $\mathbb{R}$.
why it matters
This is the elementary rectangle obstruction that starts the tensor/shear track. Its immediate parent is the negation form: a nontrivial rectangle/shear strain ($h\neq v$) admits no vertex-conformal potential realization. That parent converts the equality into the statement that pure shear lies outside the conformal ansatz.
In the broader Recognition gravity program the result marks why a scalar vertex potential is insufficient for the full weak-field metric sector, and why independent edge (tensor) degrees of freedom must be introduced before transverse-traceless modes can be represented on the discrete complex. It does not yet construct those modes; it only forces the split between conformal and shear sectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.