Releases · gift-framework/core

23 Apr 21:16

v3.4.13

ed8c86d

GIFT core 3.4.13 Latest

Latest

Axiom reduction in IntervalCertificates.lean: 22 → 11.

Eleven interval-certificate axioms eliminated by demoting opaque real constants to noncomputable defs of the four fundamental K3 eigenvalue axioms, and converting the corresponding bracket axioms to theorems proven by pure linear arithmetic.
Changed

GIFT/Foundations/IntervalCertificates.lean:

axiom K3_mean : ℝ → noncomputable def K3_mean as the arithmetic mean of the four eigenvalues.
axiom K3_ratio_i : ℝ (i = 0, 1, 2, 3) → noncomputable def K3_ratio_i as (λᵢ − mean) / (λ₃ − mean), with a helper lemma establishing positivity of the denominator.
axiom K3_sigma : ℝ → noncomputable def K3_sigma as (−3·λ₀ + λ₂ + 2·λ₃) / 7 (least-squares fit against the target (−3/2, 0, 1/2, 1); mean cancels since the target components sum to 0).
All six corresponding _bracketed axioms replaced by theorems (K3_mean_bracketed, K3_ratio_{0,1,2,3}_bracketed, K3_sigma_bracketed), each proven by linarith or le_div_iff₀ + linarith on the underlying eigenvalue bracket axioms.

GIFT/Foundations/MetricEigenvalues.lean:

axiom g_K3_rational_approximates_K3_mean → theorem of the same statement, proven via abs_le + linarith from K3_mean_bracketed and numerical evaluation of 64/77.

Remaining interval-certificate axioms (11)

The fundamental numerical inputs (externally certified by interval arithmetic):

det_g_at_half, K3_eigenvalue_0..3 — opaque real constants
det_g_at_half_bracketed, K3_eigenvalue_0..3_bracketed — bracket axioms (widths ~1.6 × 10⁻¹²)
PSLQ_null_in_TCS_basis — meta-level placeholder with no formal content

All other K3 quantities (mean, deviation ratios, anisotropy σ) and the derived bracket theorems now follow from these by pure arithmetic.
Sanity

Full lake build passes (8380 jobs, 0 warnings, 0 sorry).
Main prediction chain axiom count unchanged: 4.
All downstream theorems (r_i_ne_*, naive_pattern_falsified, dev_i_small, one_parameter_signature, interval_certificates_master) compile unchanged.

Assets 2

19 Apr 14:01

gift-framework

v3.4.12

e215477

GIFT core 3.4.12

Summary

Interval-arithmetic certificates from Phase 1b + Phase 3 imported as Lean axioms (Tier 1.1 of the Lean structural upgrade path).

The new GIFT/Foundations/IntervalCertificates.lean imports the outputs of two Colab interval-arith verification notebooks (Phase 1b + Phase 3) as formal Lean axioms with explicit numerical bracket content. This is strictly stronger than the pre-existing Category F axioms in MetricEigenvalues.lean, which proved only trivial integer identities via native_decide without physical interval content.

Main prediction chain unchanged: the 4 published axioms on the main prediction chain are preserved. The 22 new axioms are scoped to interval certificates on the K3 block of g* at s = 0.5 — a side-channel for numerical geometric claims, not the gauge / mass / coupling predictions.

Key derived theorems (all zero-sorry, proved via linarith on the bracket axioms):

det_g_at_half_near_65_32 — det(g(0.5)) = 65/32 to better than 10⁻¹²
K3_eigenvalues_positive — all four λᵢ strictly positive
K3_eigenvalues_strict_order — λ₀ < λ₁ < λ₂ < λ₃
r_0_ne_neg_three_halves, r_1_ne_zero, r_2_ne_one_half — the naive ratio pattern (-3/2, 0, 1/2, 1) is formally falsified (each target value lies outside the certified interval for its ratio)
naive_pattern_falsified — master rejection theorem
dev_0_small, dev_1_small, dev_2_small — 1-parameter signature bounds showing dev_2 ≤ 10⁻³ while dev_0, dev_1 ≈ 0.024
interval_certificates_master — conjunction certificate

Added

GIFT/Foundations/IntervalCertificates.lean — new file, 328 lines:

11 real-valued declarations (axiom K3_eigenvalue_i : ℝ, etc.)
11 interval bracket axioms (Category F, Colab-cert source cited, widths ~1.6 × 10⁻¹²)
1 PSLQ-null meta-axiom (placeholder)
12 derived theorems (pattern falsification, 1-parameter signature, master certificate)

GIFT/Foundations.lean — added import IntervalCertificates.

Assets 2

18 Apr 14:42

gift-framework

v3.4.11

b4dd209

GIFT core 3.4.11

Full Changelog: v3.4.10...v3.4.11

Assets 2

14 Apr 15:18

gift-framework

v3.4.10

348168e

v3.4.10 — TCS building block identification corrected

Mathematical honesty pass

The previous formalization incorrectly identified TCS building blocks as M₁ = Quintic in ℂP⁴ and M₂ = CI(2,2,2) in ℂP⁶. This has been corrected:

Quintic in ℂP⁴ is a CY3 (c₁ = 0), not semi-Fano (c₁ > 0) — cannot be a TCS building block
(b₂, b₃) = (21, 77) not in any known compact G₂ construction (2026-04-14)
Orthogonal TCS excluded by parity: b₂+b₃ = 98 even (CHNP Lemma 6.7)

Changes

M1_quintic → M1_candidate, M2_CI → M2_candidate (arithmetic placeholders only)
abbrev backward-compatible aliases — zero downstream breakage
New theorem: tcs_betti_arithmetic_existence (existential, arithmetic only)
New theorem: orthogonal_tcs_excluded (parity, CHNP Lemma 6.7)
Historical correction note in file header
Implemented and verified by Aristotle (project 4fa00cee)