Encyclopedia Gravity Gravity Freudenthal Length Chain Endpoint Cert Freudenthal Dihedral Closed Deriv

ARTICLE 3 claims 3 theorems

Gravity Freudenthal Length Chain Endpoint Cert Freudenthal Dihedral Closed Deriv

A machine-checked theorem reduces the length of every dihedral edge in the Freudenthal tetrahedron to a simple closed formula involving a summand table and square roots.

Verify this page

The closed-form dihedral length

The Freudenthal tetrahedron is a four-vertex simplex whose six edge lengths are prescribed by a specific data table. In the Recognition Science framework, the theorem dihedralClosedDerivLength (a term for the derivative of a dihedral angle with respect to a length parameter) is computed for each of the six edges. The declaration freudenthalDihedralClosedDerivLength_snorm states that for any two edges e and k, this derivative equals the product of a summand norm (a rational number from a 6 by 6 table) and the ratio of the square roots of the squared edge lengths of k and e.

The theorem is a closed-form certificate: it replaces a complex computation with a direct formula. For example, the summand norm for the pair (5, 0) is 2, and for (4, 1) it is 4. The full 6 by 6 table of these summand norms is itself evaluated and proved correct in the same file. This means the derivative for every pair of edges can be read off immediately from the table and the square-root ratio, without re-running the underlying Schläfli polynomial machinery.

In Recognition Science, this result supports the length-chain endpoint certificate: it provides a concrete, checkable value for how dihedral lengths respond to changes in edge lengths within the Freudenthal tetrahedron. The theorem is proved in the machine-checked library of formal theorems, meaning the derivation is verified by a computer kernel. It does not claim that the Freudenthal tetrahedron is physically realized, nor that these derivatives have any gravitational interpretation beyond the framework's own definitions.

The practical consequence is that anyone working with the framework's gravity module can treat these dihedral length derivatives as exact, closed-form quantities. The table of summand norms, with its mix of positive, negative, and zero entries, is the complete set of coefficients needed. This is a computational convenience, but also a structural fact: the derivatives are not arbitrary numbers but follow a precise arithmetic pattern encoded in the 6 by 6 table.

THEOREM freudenthalDihedralClosedDerivLength_snorm · IndisputableMonolith/Gravity/FreudenthalLengthChainEndpointCert.lean
freudenthalDihedralClosedDerivLength_snorm · IndisputableMonolith/Gravity/FreudenthalLengthChainEndpointCert.lean:394 
/-- 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
THEOREM freudenthalSchlaefliPolySummandNorm_eq_table · IndisputableMonolith/Gravity/FreudenthalLengthChainEndpointCert.lean
freudenthalSchlaefliPolySummandNorm_eq_table · IndisputableMonolith/Gravity/FreudenthalLengthChainEndpointCert.lean:352 
/-- The lookup table matches the evaluated rationalized Schläfli summands. -/
theorem freudenthalSchlaefliPolySummandNorm_eq_table (e k : Fin 6) :
    schlaefliPolySummandNorm freudenthalTetSqEdges e k =
      freudenthalSchlaefliPolySummandNormTable e k := by
  match e, k with
  | 0, 0 => exact snorm_zero_0_0
  | 0, 1 => exact snorm_zero_0_1
  | 0, 2 => exact snorm_zero_0_2
  | 0, 3 => exact snorm_zero_0_3
  | 0, 4 => exact snorm_0_4
  | 0, 5 => exact snorm_0_5
  | 1, 0 => exact snorm_zero_1_0
  | 1, 1 => exact snorm_1_1
  | 1, 2 => exact snorm_1_2
  | 1, 3 => exact snorm_1_3
  | 1, 4 => exact snorm_1_4
  | 1, 5 => exact snorm_1_5
  | 2, 0 => exact snorm_zero_2_0
  | 2, 1 => exact snorm_2_1
  | 2, 2 => exact snorm_2_2
  | 2, 3 => exact snorm_2_3
  | 2, 4 => exact snorm_2_4
  | 2, 5 => exact snorm_zero_2_5
  | 3, 0 => exact snorm_zero_3_0
  | 3, 1 => exact snorm_3_1
  | 3, 2 => exact snorm_3_2
  | 3, 3 => exact snorm_3_3
  | 3, 4 => exact snorm_3_4
  | 3, 5 => exact snorm_zero_3_5
  | 4, 0 => exact snorm_4_0
  | 4, 1 => exact snorm_4_1
  | 4, 2 => exact snorm_4_2
  | 4, 3 => exact snorm_4_3
  | 4, 4 => exact snorm_4_4
  | 4, 5 => exact snorm_zero_4_5
  | 5, 0 => exact snorm_5_0
  | 5, 1 => exact snorm_5_1
  | 5, 2 => exact snorm_zero_5_2
  | 5, 3 => exact snorm_zero_5_3
  | 5, 4 => exact snorm_zero_5_4
  | 5, 5 => exact snorm_zero_5_5
THEOREM snorm_5_0 · IndisputableMonolith/Gravity/FreudenthalLengthChainEndpointCert.lean
snorm_5_0 · IndisputableMonolith/Gravity/FreudenthalLengthChainEndpointCert.lean:304 
theorem snorm_5_0 :
    schlaefliPolySummandNorm freudenthalTetSqEdges 5 0 = 2 := by
  rw [schlaefliPolySummandNorm_eq_num_div_den]
  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
    DihedralCayleyMenger.oppositeCMVertices
  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
  norm_num

What this page does not claim

The Freudenthal tetrahedron is not claimed to correspond to any physical spacetime configuration. The theorem does not assign gravitational meaning to the dihedral derivatives beyond the framework's own definitions. The result does not imply that the dihedral length derivatives are measurable quantities in conventional physics.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND