heron_eval
plain-language theorem explainer
When the squared Heron polynomial of three real edge lengths equals a value x, the triangular hinge area equals the nonnegative square root of x. Cited by anyone evaluating explicit flat 4-simplex hinge areas from squared-edge seed data. Proof is a one-line simp that unfolds the area definition against the supplied equality.
Claim. For $a,b,c,x\in\mathbb{R}$, if the squared Heron quantity $(2ab+2bc+2ca-a^2-b^2-c^2)/16$ equals $x$, then the triangular hinge area equals $\sqrt{x}$.
background
In 4D Regge calculus curvature sits on triangular hinges. The area of each hinge multiplies the deficit angle in the action and appears as a coefficient in the Schläfli identity. The squared-area polynomial used here is
$$(2ab+2bc+2ca-a^2-b^2-c^2)/16,$$
the Cayley-Menger form when $a,b,c$ are the three squared edge lengths of a face. The hinge area is defined as the real square root of that quantity.
This module treats the Freudenthal/Kuhn 4-simplex pathwise Schläfli problem at the flat seed ($n_H=n_E=10$), mirroring the 3D Gate-A2 tetrahedron closed form. Explicit numerical hinge areas on the flat seed are required before the flat summand table, column-sum vanishing, and directional Schläfli kill can be stated.
proof idea
One-line wrapper. simp only unfolds the definition of hinge area (square root of the squared Heron polynomial) and rewrites with the hypothesis that the polynomial equals $x$, producing $\sqrt{x}$ at once.
why it matters
Supplies the rewrite step inside the eight flat-seed evaluations hingeAreaFlat_0 through hingeAreaFlat_7. Each of those theorems first proves a concrete numerical identity for the squared Heron polynomial on seed edge lengths, then applies this lemma and a square-root simplification (sqrt_one_quarter, sqrt_half, Real.sqrt_one, etc.).
Those explicit positive areas are THEOREM-tier inputs to the flat Schläfli summand table and the non-vacuous SchlaefliIdentityN witness at $n_H=n_E=10$. They sit under the Freudenthal 4-simplex pathwise program (Gate A2-style directional kill at flat). They do not close the still-open full pathwise identity off the flat seed, remapped derivatives for every hinge row, or $S_{RS}\to$ Einstein-Hilbert in 4D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.