Encyclopedia Gravity Gravity Freudenthal Length Chain Endpoint Cert Freudenthal Schlaefli Poly Summan

ARTICLE 3 claims 3 theorems

Gravity Freudenthal Length Chain Endpoint Cert Freudenthal Schlaefli Poly Summan

A machine-checked proof verifies that a 6 by 6 table of numbers, built from the geometry of a tetrahedron, is exactly the table that a certain geometric formula produces.

Verify this page

The certificate table

In geometry, a tetrahedron is the simplest solid: four triangular faces, six edges, and four corners. The declaration in question concerns a specific tetrahedron, one whose edge lengths are tied to the golden ratio. The framework's machine-checked library of formal theorems contains a definition of a 6 by 6 table of numbers, and a separate definition of a formula that takes a pair of edge indices and returns a number. The theorem, freudenthalSchlaefliPolySummandNorm_eq_table, states that for every one of the 36 possible pairs of edges, the formula's output is exactly the number stored in the table.

The formula itself is a Schläfli summand, a term from the geometry of polytopes. For a tetrahedron, it involves the dihedral angles between faces, which are the angles you would measure if you flattened two faces out onto a plane. The theorem's proof is not a hand-waving argument; it is a formal, machine-checked derivation. The library verifies that the formula, when evaluated with the tetrahedron's specific edge lengths, produces the table's values: for instance, the entry for edge 0 and edge 5 is 2, and the entry for edge 5 and edge 1 is -1. These are not approximate values; they are exact rational numbers.

The theorem also connects this table to a second quantity, the derivative of the dihedral angle with respect to an edge length. This derivative, called dihedralClosedDerivLength, is shown to equal the table's value multiplied by a ratio of square roots of the edge lengths. This is a separate theorem, freudenthalDihedralClosedDerivLength_snorm, and it means the table is not an isolated curiosity: it is a certificate, a compact record of how the tetrahedron's angles change as its edges stretch.

In Recognition Science, this certificate is part of a larger program. The framework derives physical constants and structures from a single principle: reality keeps a ledger of recognition events. This particular theorem is a step in that program, but it is a narrow one. It does not, by itself, prove anything about gravity, about the number of spatial dimensions, or about the value of any physical constant. It is a piece of the machinery, a verified computation about a specific geometric object.

What the theorem does not claim is equally important. It does not claim that this tetrahedron is the only one that matters, or that the table's values are universal. It does not claim that the formula is derived from the framework's cost function. The formula is a definition, a choice of how to compute a geometric quantity. The theorem only verifies that this definition, applied to this tetrahedron, produces this table. The physical significance of the tetrahedron, and its role in the larger theory, is a separate question that this declaration does not address.

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_0_5 · snorm_5_1 · IndisputableMonolith/Gravity/FreudenthalLengthChainEndpointCert.lean
snorm_0_5 · IndisputableMonolith/Gravity/FreudenthalLengthChainEndpointCert.lean:104 
theorem snorm_0_5 :
    schlaefliPolySummandNorm freudenthalTetSqEdges 0 5 = 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
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

What this page does not claim

The theorem does not assign any physical meaning to the tetrahedron or its edge lengths. The formula is a definition, not a derived consequence of the framework's cost function. The theorem does not prove anything about gravity or the number of spatial dimensions.

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