giftpy 1.0.0

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

GIFT Core

Formally verified mathematical constants from the GIFT framework.

Install

pip install giftpy

Usage

from gift_core import *

print(SIN2_THETA_W)  # Fraction(3, 13)
print(B2, B3)        # 21 77
print(DET_G)         # Fraction(65, 32)

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

What's inside

Constant	Value	Proven
sin^2(theta_W)	3/13	Lean + Coq
tau	3472/891	Lean + Coq
det(g)	65/32	Lean + Coq
kappa_T	1/61	Lean + Coq
delta_CP	197	Lean + Coq
m_tau/m_e	3477	Lean + Coq
m_s/m_d	20	Lean + Coq
Q_Koide	2/3	Lean + Coq
lambda_H_num	17	Lean + Coq
H*	99	Lean + Coq
p2	2	Lean + Coq
N_gen	3	Lean + Coq
dim(E8xE8)	496	Lean + Coq

13 relations total, all proven in both Lean 4 and Coq.

Verification

# Lean
cd Lean && lake build

# Coq
cd COQ && make

Links

• Full framework: gift-framework/GIFT
• Publications: gift_2_3_main.md

MIT License | gift-framework