Gravity Freudenthal Length Chain Endpoint Cert Snorm Zero 0 0

The zero entry

The declaration snorm_zero_0_0 is a single line in a larger formal computation. It states that a certain geometric quantity, called a Schläfli summand norm, evaluates to zero for the pair of indices (0, 0) when applied to the edge-length data of a regular tetrahedron. The quantity itself is a piece of a formula that describes how the dihedral angle of a tetrahedron changes when one of its edges is varied. The index pair (0, 0) refers to the first edge and the first vertex, so the statement says that this particular contribution vanishes.

The result is not a new physical law. It is a computational certificate, a checked arithmetic fact that supports a larger chain of reasoning about length chains in the framework's gravity module. The declaration is one of many such entries in a 6 by 6 table, and the table as a whole is used to build a closed-form expression for the derivative of the dihedral angle. The value zero for this entry means that the contribution from this particular edge-vertex pair drops out of the sum; it does not mean the edge itself is irrelevant or that the angle is constant.

What the declaration does not claim is equally precise. It does not claim that the dihedral angle itself is zero, nor that the tetrahedron is degenerate. It does not assert anything about the physical meaning of the zero value, such as a symmetry or a vanishing force. The statement is purely algebraic: given the specific edge lengths of the regular tetrahedron, this one term in a polynomial expression evaluates to zero. The proof is a direct computation, unfolding definitions and simplifying with arithmetic, not a conceptual argument about geometry or physics.

In the broader context of the framework, this certificate is a small brick in a wall. The wall is a machine-checked library of formal theorems, and the brick helps verify that a particular formula for the dihedral angle derivative is correct. The value zero is a fact about that formula, not a fact about the world. It gains meaning only when combined with the other entries in the table and the theorems that connect them to the geometry of the tetrahedron.

theorem snorm_zero_0_1 :
    schlaefliPolySummandNorm freudenthalTetSqEdges 0 1 = 0 := by
  rw [schlaefliPolySummandNorm_eq_num_div_den]
  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
    DihedralCayleyMenger.oppositeCMVertices
  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
  norm_num

theorem snorm_zero_0_1 :
    schlaefliPolySummandNorm freudenthalTetSqEdges 0 1 = 0 := by
  rw [schlaefliPolySummandNorm_eq_num_div_den]
  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
    DihedralCayleyMenger.oppositeCMVertices
  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
  norm_num

/-- Closed-form edge-length derivative from the evaluated rationalized summand. -/
theorem freudenthalDihedralClosedDerivLength_snorm (e k : Fin 6) :
    dihedralClosedDerivLength freudenthalTet e k =
      schlaefliPolySummandNorm freudenthalTetSqEdges e k *
        Real.sqrt (freudenthalTetSqEdges k) / (2 * Real.sqrt (freudenthalTetSqEdges e)) := by
  unfold dihedralClosedDerivLength
  rw [dihedralClosedDerivSq_eq_poly]
  have hsq : freudenthalTet.sqEdge = freudenthalTetSqEdges := by
    simp [freudenthalTet]
  have hbridge := schlaefliSummandBridge freudenthalTet e k
  have hcm : Real.sqrt (2 * cm3 freudenthalTetSqEdges) = 4 := by
    rw [cm3_freudenthalTetSqEdges]
    norm_num
  have hse_ne : Real.sqrt (freudenthalTetSqEdges e) ≠ 0 :=
    ne_of_gt (Real.sqrt_pos.mpr (freudenthalTet.sqEdge_pos e))
  have hinv :
      (1 / Real.sqrt (2 * cm3 freudenthalTetSqEdges)) = 1 / 4 := by
    rw [hcm]
  have hd_sq :
      dihedralClosedDerivSqPoly freudenthalTet e k =
        schlaefliPolySummandNorm freudenthalTetSqEdges e k /
          (4 * Real.sqrt (freudenthalTetSqEdges e)) := by
    simp only [hsq] at hbridge
    rw [hinv] at hbridge
    have hden_ne : 4 * Real.sqrt (freudenthalTetSqEdges e) ≠ 0 :=
      mul_ne_zero (by norm_num : (4 : ℝ) ≠ 0) hse_ne
    rw [eq_div_iff hden_ne]
    linarith
  calc
    2 * Real.sqrt (freudenthalTet.sqEdge k) * dihedralClosedDerivSqPoly freudenthalTet e k
        = 2 * Real.sqrt (freudenthalTetSqEdges k) * dihedralClosedDerivSqPoly freudenthalTet e k := by
            rw [hsq]
    _ = 2 * Real.sqrt (freudenthalTetSqEdges k) *
            (schlaefliPolySummandNorm freudenthalTetSqEdges e k /
              (4 * Real.sqrt (freudenthalTetSqEdges e))) := by
            rw [hd_sq]
    _ = schlaefliPolySummandNorm freudenthalTetSqEdges e k *
          Real.sqrt (freudenthalTetSqEdges k) / (2 * Real.sqrt (freudenthalTetSqEdges e)) := by
          field_simp [hse_ne]
          ring

What this page does not claim

The dihedral angle of the tetrahedron is zero. The tetrahedron is degenerate or has zero volume. The zero value indicates a physical symmetry or a vanishing force. The declaration says anything about the physical meaning of the zero value.

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/Gravity/FreudenthalLengthChainEndpointCert.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: