General-Relativistic Structure over Relational Reals

Michael Fillippini · UCF/GUTT · Coq 8.18.0

UCF/GUTT treats relations as primary and entities as emergent from relational patterns. This document reports one consequence of taking that seriously enough to mechanize it: the differential structure of general relativity can be rebuilt over a constructive, relational number system, and almost all of it holds exactly, with no classical axioms. The places where it does not hold exactly are not gaps in the argument. They fall along a single, principled line — and that line is itself a theorem.

The development is carried out entirely over the relational reals: a number tower built constructively from the rationals, with no excluded middle, no choice, and no Dedekind-real axioms. Differentiation is the discrete central difference at a spacing a. Every headline result is checked with Coq's Print Assumptions, and reported below only if that check returns Closed under the global context — the machine's confirmation that the result rests on nothing but its own construction.

The boundary between what is exact and what requires a continuum limit is not a scattering of caveats. It is one criterion: does the derivation differentiate a product?

Everything that does not — the connection, metric compatibility, the curvature commutator, the algebraic Bianchi identity, the conservation of any antisymmetric object, the conservation of every superpotential-form tensor — is exact at finite spacing, with zero axioms. Everything that must differentiate a product is a controlled limit, because the discrete Leibniz rule fails. By how much is not assumed: it is computed. The discrete product rule fails by exactly O(a²), and that exact failure is one of the proven results. So the scope of the work is drawn by a single proven line, not papered over.

Results are reported in three tiers, marked plainly. Nothing in a lower tier is allowed to borrow the standing of a higher one.

Exact at finite spacing, zero axioms. Each verified by Print Assumptions = "Closed under the global context."

• The number tower. Relational integers, rationals, and reals constructed over the rationals — no classical real-number axioms anywhere beneath the physics.
• The forced operators. The discrete Laplacian is the unique six-neighbour stencil compatible with locality, linearity, isotropy, and vanishing on constants — derived, not posited.
• The Levi-Civita connection. Given a symmetric metric with an exact inverse, the connection is torsion-free and metric-compatible (∇g = 0) exactly — no product is differentiated in the proof, so no continuum limit is needed.
• Curvature. The commutator of covariant derivatives is antisymmetric, vanishes on flat backgrounds, and satisfies the Jacobi (Bianchi) identity.
• The Einstein tensor. Ricci contraction, scalar curvature, and G = Ric − ½gR; the algebraic first Bianchi identity holds exactly; the Minkowski metric is an exact vacuum solution, G = 0.
• Conservation by structure. The divergence of any antisymmetric tensor vanishes identically — charge conservation and the linearized Bianchi identity as one fact, exactly.
• The superpotential theorem. Any tensor of the form ∂α∂βH, with H antisymmetric in its first index pair, is exactly divergence-free.
• Both superpotentials. The linearized Landau–Lifshitz superpotential and the full nonlinear superpotential (𝔤𝔤 − 𝔤𝔤, built from the contravariant metric density) carry the required antisymmetries definitionally, and are therefore exactly conserved — the nonlinear one for an arbitrary metric. Both reproduce the Minkowski vacuum exactly.
• The Leibniz theorem. The discrete product rule fails by exactly O(a²) — stated as an exact formula and proven, this is what makes the fault line of § 1 a theorem rather than a hope.

Convergent as relational reals, with explicit modulus. Shown for explicit cases; the rate of convergence is exhibited, not merely asserted.

• The d'Alembertian. The metric-weighted contraction of the second-difference operator collapses to the wave operator −∂t² + ∂x² + ∂y² + ∂z².
• The Laplacian limit. The discrete Laplacian of a quartic equals its smooth value plus an exact O(a²) term that vanishes along the geometric refinement.
• The superpotential divergence. The composed second difference at the heart of the nonlinear superpotential equals its smooth value plus an exact product-rule defect (… + 8a²); that defect is shown to vanish as a relational real. The discrete divergence converges to its smooth value — the fault line of § 1 closing, in the only form available once a product is differentiated.

Used as a bridge, not re-derived here. Named openly so the boundary of the formal work is unambiguous.

• The Landau–Lifshitz identity. That the smooth ∂α∂βH equals the Einstein tensor plus the gravitational pseudotensor — equivalently the smooth second Bianchi identity. This is the bridge from the Tier II limit to the phrase "the field equations." It is standard calculus, invoked by name, not claimed as a discrete result.

The figures below are not summaries of intent; they are the state of the source tree as it compiles. The discipline is that a result is reported here only after the assumption audit returns clean.

        20 modules   3,537 lines of Coq   73 closed-context results   0 axioms · admits · parameters    

$ coqc -Q . "" Top__Physics__*.v          # 20/20 OK

$ Print Assumptions  (every headline result)

    Closed under the global context       # × 73

$ grep -E '^(Axiom|Parameter|Admitted|admit|Conjecture)'

    (none)

The build is reproducible from a clean directory against Coq 8.18.0. The relational-reals foundation underneath it is the same one used throughout UCF/GUTT, and is independently auditable in the public library. (sorry... currently private... but probably released within a few months since it has no bearing on the IPR of related products. ;-)) 

This is a formalization of the structure of general relativity over a relational, constructive foundation, together with an exact internal account of where the continuum does the work. The connection, the curvature, the Einstein tensor, the conservation laws, and the explicit superpotentials — including the nonlinear, curved-space superpotential, conserved exactly for any metric — are theorems with no axioms beneath them.

It is not a claim to have derived the full nonlinear field equations as an exact discrete identity. By the Leibniz theorem in Tier I, that cannot be done at finite spacing — differentiating the metric product necessarily incurs the O(a²) defect — and the field-equation content is therefore reached as the continuum limit of Tier II, bridged by the cited identity of Tier III. The boundary is not hidden; it is the organizing principle of the whole development.

The intent is not to make the largest claim the work can be stretched to support, but the most precise claim it can be trusted to hold. Everything above is exactly what compiles — no more, and no less.
 

UCF/GUTT — Unified Conceptual Framework / Grand Unified Tensor Theory © 2023–2026 Michael Fillippini. Research & Evaluation License v1.1 (non-commercial, no derivatives). Source & assumption audits: github.com/relationalexistence/UCF-GUTT · relationalexistence.com