mul_div_cancel_area
plain-language theorem explainer
For each of the ten triangle hinges of the Freudenthal 4-simplex at the flat seed, the flat hinge area cancels against division by itself: area times (x over area) equals x. Gate-A2 directional Schläfli proofs cite this to strip area weights from the Jacobian rows. The argument is a one-line nonzero-division cancellation using positivity of the flat areas.
Claim. For every hinge index $h\in\{0,\ldots,9\}$ and every real $x$, writing $A_h$ for the flat area of hinge $h$, one has $A_h\cdot(x/A_h)=x$.
background
The module develops the Freudenthal (Kuhn) 4-simplex pathwise Schläfli identity at $n_H=n_E=10$, mirroring the 3D Gate-A2 tetrahedron input. At the flat seed, each of the ten triangle hinges carries a strictly positive area $A_h$ obtained by feeding the three squared edge lengths of that hinge into the Heron-style area formula.
The flat closed-form theorem already shows that every column of the summand table sums to zero: $\sum_h$ flatSchlaefliSummand$(h,e)=0$. Directional versions weight those summands by $A_h$ after dividing by $A_h$ inside the angle Jacobian, so a clean cancellation $A_h\cdot(s/A_h)=s$ is needed before the column-sum identity can be reapplied.
Positivity of each flat hinge area is recorded separately; this lemma only consumes that fact to justify division.
proof idea
One-line term proof. Apply the standard field lemma that $a\cdot(x/a)=x$ whenever $a\neq 0$, supplying the nonzero witness ne_of_gt of the already-proved positivity statement for the flat hinge area at $h$. No case split on hinges and no arithmetic beyond that cancellation.
why it matters
Parent theorems are the flat directional Schläfli kill along every squared-edge velocity through the seed, and its coordinate specialisation: both rewrite the area-weighted directional angle sum as $\sum_h A_h\cdot(\sum_e v_e\cdot s_{he}/A_h)$ and need this cancellation to recover $\sum_h s_{he}$, which vanishes by the flat closed-form column sums.
That directional identity is the module's Gate-A2-style input at flat, the 4D analog of the 3D pathwise Schläfli kill along edge directions. It sits under the THEOREM tier for flat directional Schläfli; the OPEN items (full pathwise identity off the flat seed, elevation to the continuum candidate, $S_{RS}\to$ Einstein-Hilbert in 4D) remain untouched. The lemma is pure real arithmetic scaffolding inside that Gate-A2 chain, not a new geometric claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.