Encyclopedia Gravity Gravity Freudenthal Length Chain Endpoint Cert Snorm Zero 0 2

ARTICLE 3 claims 3 theorems

Gravity Freudenthal Length Chain Endpoint Cert Snorm Zero 0 2

Inside a machine-checked library of geometry theorems, one small entry in a 6 by 6 table records a zero that certifies a local angle calculation for a regular tetrahedron.

Verify this page

A zero in the dihedral table

The declaration snorm_zero_0_2 is a single verified entry in a table of numbers used to certify angle calculations for a regular tetrahedron. The table, a full 6 by 6 array, stores values of a function called schlaefliPolySummandNorm evaluated at a specific geometric configuration named freudenthalTetSqEdges. The entry at row 0, column 2 is 0, and the theorem snorm_zero_0_2 proves exactly that, by expanding the defining expressions and simplifying them with exact arithmetic.

This zero is not an isolated curiosity. The same library proves that the entire 6 by 6 table matches the defining function at every position, and a companion theorem links these table values to a closed-form expression for dihedralClosedDerivLength, a quantity that measures how a dihedral angle changes as an edge length varies. So the zero at row 0, column 2 is a certified piece of a larger calculation: it says that, for this particular pair of edges in the tetrahedron, the relevant summand contributes nothing to that derivative.

In Recognition Science, this certificate is part of a broader program of building physical and geometric structure from a single starting point, a ledger of recognition events. The framework's library of formal theorems checks such calculations mechanically. The zero in this table is a small, exact fact about a regular tetrahedron, established without approximation and without appeal to any physical assumption. It is a building block, not a law of nature.

What the declaration does not claim is equally precise. It does not say anything about the physical meaning of the tetrahedron, about gravity, or about the recognition ledger itself. It does not assert that the zero has a special role in the framework's derivation of constants or dimensions. It is a statement about a specific function at a specific pair of indices, nothing more. The surrounding theory may use this fact later, but this theorem alone carries no such weight.

THEOREM snorm_zero_0_2 · IndisputableMonolith/Gravity/FreudenthalLengthChainEndpointCert.lean
snorm_zero_0_2 · IndisputableMonolith/Gravity/FreudenthalLengthChainEndpointCert.lean:80 
theorem snorm_zero_0_2 :
    schlaefliPolySummandNorm freudenthalTetSqEdges 0 2 = 0 := by
  rw [schlaefliPolySummandNorm_eq_num_div_den]
  unfold schlaefliPolySummandNum schlaefliPolySummandDen freudenthalTetSqEdges
    DihedralCayleyMenger.oppositeCMVertices
  simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial]
  norm_num
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

What this page does not claim

This declaration does not assert any physical law or property of gravity. It does not claim that the zero has a special significance in the Recognition Science framework's derivation of constants. It does not say anything about the recognition ledger or its cost function.

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