valuebridge-tdfloat

Triadic Dot Float (TDFloat) — exact rational arithmetic as a single Python integer, with a Rust backend and Coq-verified foundations.

from valuebridge.tdfloat import td, frac

td('0.1') + td('0.2') == td('0.3')        # True — always
(a + b) + c == a + (b + c)                  # True — for any a, b, c

---

Why This Matters for Explainable AI

Modern AI systems — language models, recommendation engines, fairness audits, financial models — all perform millions of arithmetic operations. Every one of those operations runs on IEEE 754 floating-point, a format designed in 1985 for numerical simulation, not for systems that need to be explained, audited, or trusted.

TDFloat replaces floating-point approximation with provably exact rational arithmetic. The consequences for explainable AI are direct.

1. Computations Are Reproducible — Exactly

IEEE 754 arithmetic is non-deterministic across platforms, compilers, and thread orderings. TDFloat arithmetic is deterministic by construction. The same inputs always produce the same output, encoded as the same integer. AI outputs become auditable: you can replay any computation and verify it step by step.

2. Associativity is a Theorem, Not a Hope

In IEEE 754:

(a + b) + c  ≠  a + (b + c)   for many values

Simply reordering additions in a neural network — which optimising compilers do routinely — can change the model's output.

TDFloat's associativity is formally proved in Coq (proofs/tdfloat_ieee_resolution.v).

3. Every Number Has an Interpretable Identity

In IEEE 754, 3.141592653589793 is just a 64-bit pattern. In TDFloat:

x = td('3.14')
x.as_fraction()   # (157, 50)  — exact numerator and denominator
x.info_bit        # 1          — half-step axis (has a dot)
x.dot_pos         # 2          — two decimal places

Every intermediate result is fully inspectable as an exact rational.

4. Fairness Audits Can Be Verified

If two computations produce the same rational value, their encodings are equal. If different, provably different. There is no grey zone of "close enough." Fairness claims can be verified arithmetically, not just statistically.

---

Quick Start

from valuebridge.tdfloat import td, frac, TDFloat, PI, E, PHI
from valuebridge.tdfloat.math import sqrt, circle_area, cosine_similarity

# Exact arithmetic
assert td('0.1') + td('0.2') == td('0.3')

# Exact (legacy-rational) constants
print(PI)                          # 22/7
print(E)                           # 19/7
print(circle_area(td(7)))         # 154 — exact integer

# Exact vector similarity
u = [td(3), td(4)]
v = [td(4), td(3)]
print(cosine_similarity(u, v))    # 24/25 — exact

IEEE 754 / MPFR-accurate constants

For numerically-accurate values of irrational constants (π, e, √2, ln 2, …), use the parallel ieee754 namespace:

from valuebridge.tdfloat import ieee754

ieee754.PI()                      # π at 200 bits (default)
ieee754.PI(bits=53)               # π at IEEE 754 double precision
ieee754.E(bits=128)
ieee754.SQRT2(bits=256)
ieee754.LN2(bits=64)
ieee754.EULER_GAMMA()

Each constant is computed by GNU MPFR (via gmpy2) at the requested precision and returned as a TDFloat rational approximation. The legacy PI = 22/7 stays unchanged for backward compat.

gmpy2 is a development-group dependency; install with uv sync --group dev to enable.

---

Installation

# With uv (recommended)
uv add valuebridge-tdfloat

# With pip
pip install valuebridge-tdfloat

For the Rust backend (optional; accelerates large-operand arithmetic):

cd tdfloat_core
maturin develop --release

---

Architecture

  Coq specification                 proofs/*.v
     │   HelixBit → BigInt → helix-closed arithmetic
     ▼   (formal refinement)
  Rust backend                      tdfloat_core/
     │   TDBigInt { sign, Arc<[u64]> limbs } + 5 ops
     ▼   (PyO3 boundary)
  Python surface                    valuebridge/tdfloat/
     │   TDFloat exact rational p/q, dot-axis encoding
     │   math funcs, vector ops
     ▼
  IEEE 754 reference layer          valuebridge/tdfloat/ieee754/
      MPFR-backed irrational constants at configurable precision

Each layer has one job. Each arrow is a formal refinement that preserves the observable behavior of the layer above it.

See:

• docs/mathematics.md — the triadic geometry, half-step encoding, NAND double helix, how all five arithmetic operators are grounded in one bit-level construction.
• docs/implementation.md — how the Python surface, Rust backend, and Coq proofs fit together; testing, benchmarks, development loop.

---

Formal Verification

The mathematical foundations are proved in Coq. Every .v file has a companion .md explaining it in prose.

Proof file	What it proves
encoding_any_symbol.v	The abstract half-step encoding is injective and reversible
tdfloat_dot_encoding.v	The "." IS the info-bit; integer and fractional encodings never collide
tdfloat_ieee_resolution.v	TDFloat addition is associative; IEEE 754 addition provably is not
NANDDoubleHelix.v	A bit is two perpendicular strands; all gates derive from NAND
BitwiseArbitraryInt.v	Complete BigInt library (or/and/xor/not/shl/shr/add/mul/compare) with 10 invariants
HelixArithClosed.v	Subtraction (a + ¬a + 1 ≡ 0 mod 2ⁿ), division (shift-and-subtract with invariant), modulo

These are machine-checked proofs, not documentation claims. The Rust backend is a refinement of the Coq spec — its get_bit(k) returns the same value as the Coq get_bit, so every theorem lifts observationally.

Run with:

coqc proofs/*.v

---

Development

git clone https://github.com/valuebridge-ai/tdfloat
cd tdfloat

# Python layer
uv sync --group dev
uv run pytest tests/ -q
# 268 passed, 15 xfailed, 4 xpassed

# Rust backend
cd tdfloat_core
VIRTUAL_ENV=../.venv maturin develop --release
cargo test --release --lib
# 27 passed; 0 failed

# Benchmark Rust vs Python
uv run python tests/bench_rust_vs_python.py

# Compile proofs
cd ../proofs
coqc *.v

---

Project Layout

valuebridge-tdfloat/
├── valuebridge/tdfloat/    Python surface (TDFloat, math, ieee754)
├── tdfloat_core/           Rust backend (PyO3 + maturin)
├── proofs/                 Coq specifications + .md explanations
├── tests/                  pytest (268 tests) + benchmark
├── docs/                   mathematics.md, implementation.md
└── pyproject.toml

---

License

MIT — Copyright 2026 Tushar Dadlani / Valuebridge AI