giftpy 3.0.0

GIFT mathematical core - Formally verified constants (Lean 4 + Coq)

GIFT Core

Formally verified mathematical relations from the GIFT (Geometric Information Field Theory) framework. All relations are proven in both Lean 4 and Coq.

What is this?

This repository contains 165+ exact mathematical identities derived from topological invariants of E8 × E8 gauge theory on G2 holonomy manifolds. Each relation is:

• An exact rational or integer value (no fitting or approximation)
• Independently verified in two proof assistants
• Available as Python constants via giftpy

Note: The physical interpretation of these relations remains conjectural. This package proves mathematical identities only.

Installation

pip install giftpy

Quick Start

from gift_core import *

# Access certified constants
print(SIN2_THETA_W)   # Fraction(3, 13)
print(KAPPA_T)        # Fraction(1, 61)
print(GAMMA_GIFT)     # Fraction(511, 884)

# List all proven relations
for r in PROVEN_RELATIONS:
    print(f"{r.symbol} = {r.value}")

What's New in v3.0

Joyce Existence Theorem: K7 admits a torsion-free G2 structure, proven via Banach fixed-point:

from gift_core.analysis import JoyceCertificate
cert = JoyceCertificate.verify()
assert cert.is_valid()  # Torsion < threshold with 20x margin

Building Proofs

# Lean 4
cd Lean && lake build

# Coq
cd COQ && make

Documentation

• giftpy usage guide: docs/USAGE.md — all constants, K7 pipeline, examples
• Changelog: CHANGELOG.md
• Full framework: gift-framework/GIFT
• Lean Blueprint: Interactive visualization

License

MIT

---

GIFT Core v3.0.0 — 165+ certified relations + Joyce existence theorem