Geometry Cayley Menger Polynomial Cm3 Scaling

Scaling under uniform stretch

The Cayley-Menger polynomial is a classical object in geometry: a single formula in the six squared edge lengths of a tetrahedron whose value equals 288 times the square of the tetrahedron's volume. For a unit regular tetrahedron the value is 4; for a right-angle tetrahedron with three orthogonal unit edges it is 8. The polynomial carries all metric information about the tetrahedron, and its smoothness in the edge lengths is what later derivative computations rely on.

One structural property follows immediately from the formula's form. If every squared edge length is multiplied by a common factor s, the whole polynomial multiplies by s cubed. The declaration cm3_scaling in the framework's machine-checked library of formal theorems proves exactly this: cm3(s·a) = s³ · cm3(a). This matches the classical volume behavior: a uniform stretch by factor √s in each length multiplies volume by s^{3/2}, hence volume-squared by s³. The proof is a direct algebraic expansion using the ring tactic.

In Recognition Science, this scaling law is not a standalone curiosity. The framework models physical structure through a discrete record of recognition events, and geometric quantities like volume-squared appear as derived objects. The scaling theorem provides a structural sanity check on the polynomial definition: it behaves under uniform stretch exactly as the classical volume-squared it represents. The library also derives a corollary: for a tetrahedron with all squared edge lengths equal to s, the Cayley-Menger value is 4s³.

The theorem does not claim that the polynomial defines a volume for non-Euclidean edge data, nor that it establishes any physical law. It is a pure algebraic identity about a polynomial's behavior under scaling. The classical relation 288V² = cm3 holds for genuine Euclidean tetrahedra; the scaling theorem is verified on the regular and right-angle test points, and the smoothness result holds for all real edge assignments. The framework's contribution here is a formal proof of a classical fact, not a new physical prediction.

theorem cm3_scaling (a : SqEdges) (s : ℝ) :
    cm3 (fun e => s * a e) = s ^ 3 * cm3 a := by
  unfold cm3
  ring

/-- A trivial but useful corollary: the regular CM value at common
squared-length `s` equals `s³ · 4`. -/
theorem cm3_constSq (s : ℝ) : cm3 (fun _ => s) = 4 * s ^ 3 := by
  have h := cm3_scaling regularUnitSqEdges s
  have h1 : cm3 regularUnitSqEdges = 4 := cm3_regular_unit
  have h2 : (fun e : Fin 6 => s * regularUnitSqEdges e) = (fun _ : Fin 6 => s) := by
    funext e
    unfold regularUnitSqEdges
    ring
  have h3 : cm3 (fun _ : Fin 6 => s) = s ^ 3 * cm3 regularUnitSqEdges := by
    rw [← h2]; exact h
  rw [h3, h1]
  ring

What this page does not claim

The theorem does not prove that the polynomial equals 288V² for arbitrary non-Euclidean edge assignments. It does not establish any physical law about tetrahedra in space. It does not claim the framework derives the Cayley-Menger polynomial from first principles; it defines it directly.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/CayleyMengerPolynomial.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: