A verified excerpt of the active UCF/GUTT™ Coq library is now available under Apache License 2.0:
https://github.com/relationalexistence/UCF-GUTT
This release provides independent auditors, researchers, and proof engineers with direct access to the formal foundations without requiring an NDA.
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.
What’s Included
- 30 Coq files · 25,487 lines of source
- 1,230 theorems & lemmas · 1,390 definitions/fixpoints
- Zero axioms, zero Admitted, zero Parameter declarations
- Verified under Coq 8.18–8.20
- Every major theorem closes with Print Assumptions: "Closed under the global context"
- Kernel re-verification: coqchk succeeds on the full library
Contents: Whole-completion & extension infrastructure, constructive number tower (ℕ → ℤ → ℚ → Cauchy ℝ), irrationality of √2, Propositions 01/02/04/05/10, Clock Hierarchy Coherence, and the full Relational Cubical Type Theory (RCTT) stack (Interval, PathType, NCube, J-rule, Kan canonical, relational univalence).
example/Ucf_math_demos.py provides exact-rational Python demonstrations that mirror verified theorems from the public Coq core.
- Demo 1 — √2 is irrational (Top__Numbers__RelationalIrrationals.v) Parity descent + Newton iteration in ℚ producing the canonical Cauchy sequence.
- Demo 2 — Infinitude of primes via iterated Euclid (Top__Numbers__Relational.v + RelationalIntegers.v)
- Demo 3 — Totalized division by zero with three relational contexts (Top__Numbers__RelationalDivision.v)
Zero third-party dependencies — uses only Python standard library (fractions.Fraction). All correctness claims use exact arithmetic; float appears only for human-readable magnitude display.
Full documentation and API usage examples: example/README.md.
These demos let you immediately see what the formal theorems compute on concrete inputs, with semantics that match the Coq Compute statements.
What’s Not Included (Remains Proprietary)
- Reality Engine™ internals and tensor-invariant applicability predicates
- fhoc™ (Formal Harmonic Overlap Certification) pipeline
- LANTOSE™ linguistic workbench and NRTML™
- Applications layer (Marcus electron-transfer chain, Layer-11 physics derivations, GRB photon time-delay, etc.)
- Relational Stability Function (Φ), Relational Connectivity Graph (RCG), and all NDA-level derivation chains
The active internal library (52 propositions, 180+ files, 130k+ lines) builds directly on this public kernel using the same zero-extra-axiom discipline.
Licensing
The 30 source files are released under Apache 2.0 (full text in LICENSE). This permits inspection, modification, and redistribution with proper attribution.
Trademarks (UCF/GUTT™, Reality Engine™, LANTOSE™, RCTT™, fhoc™, etc.) are not licensed under Apache 2.0. See TRADEMARKS.md in the repository.
AI/ML training, embedding, or RAG use of this material or the broader framework remains prohibited.
Next Steps
This release strengthens the public verification story but does not change the commercial licensing model for applied layers or industrial use.
UCF/GUTT™, Reality Engine™, LANTOSE™, NRTML™, RCTT™, fhoc™, and Relational Existence™ are trademarks of Michael Fillippini. © 2023–2026 Michael Fillippini.