Gravity Freudenthal Length Chain Endpoint Cert Snorm Zero 0 3

A zero in the dihedral table

The declaration snorm_zero_0_3 is a theorem in the framework's machine-checked library of formal theorems. It proves that a specific entry in a 6 by 6 table of geometric numbers is exactly zero. The table is built from the squared edge lengths of a tetrahedron, and each entry records a normalized contribution to a dihedral angle sum, a quantity from classical geometry.

The theorem states that the entry in the first row and fourth column, written as index pair (0, 3), evaluates to zero. This is not an approximation or a rounding; the proof computes the rational expression and simplifies it to the exact integer 0. The entry is one of many in a table that also contains values like 2, 4, 6, and negative numbers, so this particular zero is a specific structural fact, not a general property of the whole table.

In Recognition Science, this table is part of a larger effort to derive physical constants from a ledger of recognition events. The framework models geometric objects like tetrahedra as discrete records, and this theorem is a certificate that a particular summand in a dihedral angle calculation vanishes. The zero itself is a small but exact piece of that larger derivation, a check that the framework's geometric machinery produces clean, rational results at specific points.

What the theorem does not claim is just as precise. It does not say that all entries in the table are zero, nor does it say anything about the physical meaning of the zero. It is a statement about one number in a defined table, nothing more. The theorem's scope is the entry at index (0, 3); any broader conclusion about dihedral angles or the framework's constants would require additional theorems that are not part of this declaration.

theorem snorm_zero_0_3 :
    schlaefliPolySummandNorm freudenthalTetSqEdges 0 3 = 0 := 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 theorem does not claim that all entries in the table are zero. The theorem does not claim any physical interpretation for the zero value. The theorem does not claim that the dihedral angle sum itself is zero.

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: