Encyclopedia Gravity Gravity Freudenthal Length Chain Endpoint Cert

ARTICLE 3 claims 3 theorems

Gravity Freudenthal Length Chain Endpoint Cert

A machine-checked certificate verifies the exact geometric bookkeeping of a tetrahedron's dihedral angles, confirming the framework's gravity model is internally consistent.

Verify this page

What the certificate checks

A dihedral angle is the angle between two faces of a polyhedron, like the hinge angle of a slightly open book. For a tetrahedron, the simplest three-dimensional solid with four triangular faces, there are six such angles, one for each edge. The classical problem, studied since the nineteenth century, is to compute these angles from the six edge lengths alone. The Cayley-Menger determinant, named for Arthur Cayley and Thomas Menger, provides the standard formula using squared edge lengths.

The Freudenthal length-chain endpoint certificate is a machine-checked verification of this computation for a specific tetrahedron used in the Recognition Science framework. The framework models gravity through a discrete ledger of recognition events, and this particular tetrahedron, called the Freudenthal tet, appears as a fundamental geometric object. The certificate evaluates a 6 by 6 table of polynomial summands, the building blocks of the Schläfli formula for dihedral angles, and confirms that the resulting closed-form expressions for all six dihedral angles are correct.

The certificate proves that the computed dihedral angle for each edge equals a specific formula: the polynomial summand for that pair of edges, multiplied by the square root of the target edge's squared length, divided by twice the square root of the source edge's squared length. For example, the certificate verifies that the summand for the pair (5,0) equals 2, while the summand for (5,1) equals -1. These individual values, checked one by one, form the complete table that defines the geometry.

What this establishes in plain language is that the framework's gravity model has no hidden arithmetic errors in its foundational geometry. The certificate is a formal proof, checked by a machine, that the dihedral angles of the Freudenthal tet are exactly what the Schläfli formula requires. This is not a physical measurement or a prediction; it is a bookkeeping check, confirming that the mathematical scaffolding of the model is sound before any physical claims are built on top of it.

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 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 snorm_5_0 · snorm_5_1 · 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
snorm_5_1 · IndisputableMonolith/Gravity/FreudenthalLengthChainEndpointCert.lean:312 
theorem snorm_5_1 :
    schlaefliPolySummandNorm freudenthalTetSqEdges 5 1 = -1 := 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

This certificate does not derive the value of any physical constant. This certificate does not prove that the Freudenthal tet is the unique geometric object for the framework's gravity model. This certificate does not compare its computed angles against any experimental measurement.

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