This page gives two entry points into the public mathematical substrate of UCF/GUTT: three Python demonstrations that use only the standard library, and a separate Coq proof library that machine-checks the underlying theorems. The two paths answer different questions and neither replaces the other.
The point of the math layer isn't that all of the theorems are new; it's that they fall out of a relation-first substrate.
https://github.com/relationalexistence/UCF-GUTT/tree/main/example
Why Python and Coq are separate
Python exhibits the computational content of selected theorems on chosen inputs, using exact rational arithmetic — fractions.Fraction end to end, no float ever feeds a claim. Coq certifies that those theorems hold universally, without hidden assumptions. If you have a few minutes, the Python alone is enough to see what the framework does on concrete inputs. If you want to confirm the theorems are real, the Coq build is the separate verification step.
The Python requires Python 3.8 or later and the standard library only — fractions, dataclasses, enum, math, sys, typing. No pip install. The Coq build requires Coq 8.18 or later (verified through 8.20) and runs independently.
What this page does not cover
These demonstrations illustrate three results from the public math core. They do not exhibit the Reality Engine, the fhoc certification tool, LANTOSE, the Φ stability function, the physics derivations including the GRB time-delay prediction, the chemistry application layers, or the broader framework proposition catalogue beyond what each individual demo touches. Those components are either separately documented or not publicly released. Nothing on this page validates the full UCF/GUTT claim stack. The scope is deliberately narrow.
Demonstration 1 — Totalized division across three relational contexts
Most formal libraries treat division by zero as undefined or return a chosen sentinel value. UCF/GUTT routes it through relational context. For nonzero denominators every context reduces to ordinary rational division. For division by zero, three contexts return three different relational values: RC_Space → PinftyQ, RC_Time → FiniteQ 0, RC_Info → ExtNaNQ. Every cell of the table below returns a fully defined ExtendedQ; there is no partiality, no exception, no undefined region.
context a b a / b boundary?
---------- ---------- ---------- ---------------------- ---------
RC_Space 5/1 0/1 PinftyQ RS_Boundary
RC_Space 0/1 0/1 PinftyQ RS_Boundary
RC_Space 1/1 0/1 PinftyQ RS_Boundary
RC_Space 6/1 2/1 FiniteQ(3/1) RS_Related
RC_Space 1/3 2/1 FiniteQ(1/6) RS_Related
RC_Time 5/1 0/1 FiniteQ(0/1) RS_Boundary
RC_Time 0/1 0/1 FiniteQ(0/1) RS_Boundary
RC_Time 1/1 0/1 FiniteQ(0/1) RS_Boundary
RC_Time 6/1 2/1 FiniteQ(3/1) RS_Related
RC_Time 1/3 2/1 FiniteQ(1/6) RS_Related
RC_Info 5/1 0/1 ExtNaNQ RS_Boundary
RC_Info 0/1 0/1 ExtNaNQ RS_Boundary
RC_Info 1/1 0/1 ExtNaNQ RS_Boundary
RC_Info 6/1 2/1 FiniteQ(3/1) RS_Related
RC_Info 1/3 2/1 FiniteQ(1/6) RS_Related
To run this demo alone:
python3 Ucf_math_demos.py div
The conceptual content: boundary behavior in UCF/GUTT is not a universal failure state but a context-routed relational value. The same a/0 expression resolves to three different fully defined values depending on which relational context is active, while every nonzero denominator behaves conservatively. This is the demonstration that exhibits something a typical formal library does not.
Demonstration 2 — Constructive √2
Two complementary pieces: parity descent on candidate p/q, and exact-rational Newton iteration as a Cauchy witness for √2. Mirrors the Coq theorems sqrt2_cauchy_mod, sqrt2_sq_converges_to_2, sqrt2_not_rational_Z, and no_rational_squares_to_2. The underlying claim:
forall p q : nat, q <> 0 -> gcd p q = 1 -> p*p <> 2 * (q*q)
Parity descent on the canonical convergents shows the equation never holds:
input : p = 3, q = 2 -> 9 != 8
input : p = 7, q = 5 -> 49 != 50
input : p = 17, q = 12 -> 289 != 288
input : p = 577, q = 408 -> 332929 != 332928
Newton iteration x_{n+1} = (x_n + 2/x_n) / 2, entirely in Q:
n x_n (exact) x_n^2 - 2 (exact) |deficit| as float
--- ------------------------ ------------------------ ------------------
0 1/1 -1/1 1.000e+00
1 3/2 1/4 2.500e-01
2 17/12 1/144 6.944e-03
3 577/408 1/166464 6.007e-06
4 665857/470832 1/221682772224 4.511e-12
The full demo continues to n = 8, where the rational reaches roughly two hundred digits and the deficit drops to ≈ 8e-196. Every x_n is rational, every deficit x_n^2 - 2 is a nonzero rational, and the limit — √2 — is not in Q. The sequence is the canonical Cauchy witness for the irrational it represents.
To run with twelve iterations:
python3 Ucf_math_demos.py sqrt2 12
Demonstration 3 — Infinitude of primes via Euclid in N_rel
Iterated Euclidean construction over N_rel: at each step, take the product of all known primes, add one, and extract the smallest prime factor of the result. That factor is provably not in the input list (it divides product+1, but no input prime does), so the chain is unbounded by construction.
step input primes N = prod+1 new prime
---- ------------------------------ -------------------- ---------
1 2 3 3
2 2, 3 7 7
3 2, 3, 7 43 43
4 2, 3, 7, 43 1807 13
5 2, 3, 7, 43, 13 23479 53
6 2, 3, 7, 43, 13, 53 1244335 5
Note step 4: the smallest factor of 1807 is 13, not 1807 itself — the new prime is not necessarily N itself, only a witness extracted from it. That subtlety is what the constructive version makes visible. The no-maximal-prime result, reproduced as an actual construction rather than a contradiction proof.
To run, generating ten primes:
python3 Ucf_math_demos.py primes 10
Coq correspondence
The demonstrations correspond to theorems in the following Coq modules:
- Top__Numbers__Relational — natural numbers, N_rel
- Top__Numbers__RelationalIntegers — integers and divisibility, Z_rel
- Top__Numbers__RelationalRationals — rationals, Q_rel
- Top__Numbers__RelationalReals — Cauchy reals, R_cauchy
- Top__Numbers__RelationalIrrationals — constructive irrationality
- Top__Numbers__RelationalDivision — totalized division
Verifying the Coq core
The Python demonstrations show computational behavior. They do not certify the underlying theorems.
To verify the Coq side, install Coq 8.18 or later (verified through 8.20), then run:
git clone https://github.com/relationalexistence/UCF-GUTT
cd UCF-GUTT
make
Print Assumptions queries are embedded inline in the source files, so each embedded query prints
Closed under the global context
as make compiles its module. A successful build terminates with a summary banner of the form:
==========================================================
Build OK -- 30 files compiled (zero Admitted /
zero UCF axioms / zero Parameter declarations).
==========================================================
To count the in-source Closed under the global context results explicitly:
make audit
The audit terminates with a summary of the form:
==========================================================
AXIOM AUDIT SUMMARY
==========================================================
'Print Assumptions' calls embedded in sources: 80
'Closed under the global context' results: 80
Unclosed dependencies detected: 0
==========================================================
If you want to query individual theorems interactively under coqtop or coqide, the canonical examples are:
Print Assumptions Q_contextual_space_infty.
Print Assumptions Q_contextual_time_zero.
Print Assumptions Q_contextual_info_nan.
Print Assumptions Q_contextual_div_conservative.
Print Assumptions sqrt2_not_rational_Z.
Print Assumptions sqrt2_cauchy_mod.
Print Assumptions sqrt2_sq_converges_to_2.
Each should return Closed under the global context. This is the formal-certification step. It is independent of the Python demonstrations above.
What this is and is not
These three demonstrations are a starting point, not a survey. The public Coq library covers substantially more — including relational graph theory, hypergraph theory, integers, rationals, and additional proposition modules. Other UCF/GUTT components, including application-layer systems and physics derivation chains, are separately documented or not publicly released. The example directory is deliberately small: three results, each runnable in seconds, sufficient to answer the first skeptical question: whether there is executable computational content here, not only formal notation.
Licensing
The source files in this release are licensed under Apache 2.0. Trademarks and proprietary layers — including the Reality Engine, fhoc, LANTOSE, and the physics derivation chains — are licensed separately. Full terms and the complete release notice are on the GitHub Release page.