Skip to main content

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

Project description

GIFT Core

Formal Verification Python Tests PyPI Lean 4 Coq

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

Overview

This repository contains 180+ exact mathematical identities derived from topological invariants of E₈ gauge theory on G₂ holonomy manifolds.

Core Results

  • Explicit G₂ Metric: Closed-form solution g = (65/32)^{1/7} × I₇ with det(g) = 65/32 and zero torsion
  • E₈ Root System: Complete enumeration (240 = 112 + 128) with Weyl reflection theorems
  • G₂ Cross Product: 7D Lagrange identity ‖u × v‖² = ‖u‖²‖v‖² - ⟨u,v⟩² proven via coassociative 4-form
  • Joyce Existence: K₇ admits torsion-free G₂ structure (Banach fixed-point formalization)

Extensions

  • Sequence Embeddings: Fibonacci F₃–F₁₂ and Lucas L₀–L₉ map to GIFT constants
  • Prime Atlas: 100% coverage of primes < 200 via three generators (b₃, H*, dim_E₈)
  • Monstrous Moonshine: 196883 = 47 × 59 × 71, j-invariant 744 = 3 × dim_E₈
  • McKay Correspondence: E₈ ↔ Binary Icosahedral ↔ Golden Ratio

Infrastructure

  • Dual Verification: All theorems proven in Lean 4 + Coq
  • Blueprint: Dependency graph with 185 linked declarations (leanblueprint)
  • Python Package: giftpy with certified constants

Installation

pip install giftpy

Quick Start

from gift_core import *

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

Building Proofs

# Lean 4
cd Lean && lake build

# Coq
cd COQ && make

Documentation

Acknowledgments

Blueprint structure inspired by KakeyaFiniteFields.

License

MIT


GIFT Core v3.1.10

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

giftpy-3.1.10.tar.gz (253.1 kB view details)

Uploaded Source

Built Distribution

If you're not sure about the file name format, learn more about wheel file names.

giftpy-3.1.10-py3-none-any.whl (116.4 kB view details)

Uploaded Python 3

File details

Details for the file giftpy-3.1.10.tar.gz.

File metadata

  • Download URL: giftpy-3.1.10.tar.gz
  • Upload date:
  • Size: 253.1 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? Yes
  • Uploaded via: twine/6.1.0 CPython/3.13.7

File hashes

Hashes for giftpy-3.1.10.tar.gz
Algorithm Hash digest
SHA256 3522784e3b8a9cac444e692aaa702760982bfb7bc3c3a8187ed1e23bb9d2f072
MD5 a5fb6639ff370fdb4c09b982982e600b
BLAKE2b-256 58a0fdb806f21fc358e1e206e1d336aa32d3a1554253d8a916f044617c832d58

See more details on using hashes here.

Provenance

The following attestation bundles were made for giftpy-3.1.10.tar.gz:

Publisher: publish.yml on gift-framework/core

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file giftpy-3.1.10-py3-none-any.whl.

File metadata

  • Download URL: giftpy-3.1.10-py3-none-any.whl
  • Upload date:
  • Size: 116.4 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? Yes
  • Uploaded via: twine/6.1.0 CPython/3.13.7

File hashes

Hashes for giftpy-3.1.10-py3-none-any.whl
Algorithm Hash digest
SHA256 1877fbf8464fad40b73696016636c20dc3405df8f998b8645147730f86f4e024
MD5 2e93a1383036c3c4750ff6b203d285ee
BLAKE2b-256 69fcb5e9abfa7b7074921f6c15ef9c73c29ee7224c94ae77ced6c513f6835dc6

See more details on using hashes here.

Provenance

The following attestation bundles were made for giftpy-3.1.10-py3-none-any.whl:

Publisher: publish.yml on gift-framework/core

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

Supported by

AWS Cloud computing and Security Sponsor Datadog Monitoring Depot Continuous Integration Fastly CDN Google Download Analytics Pingdom Monitoring Sentry Error logging StatusPage Status page