diff --git a/.github/workflows/verify-consistency.yml b/.github/workflows/verify-consistency.yml index d832c94c..e7f7c303 100644 --- a/.github/workflows/verify-consistency.yml +++ b/.github/workflows/verify-consistency.yml @@ -52,10 +52,5 @@ jobs: - name: Check blueprint sync run: ./scripts/check_blueprint_sync.sh - - name: Check no sorry in Lean files - run: | - if grep -rn "sorry" GIFT/ GIFTTest/ --include="*.lean" | grep -v "^.*:.*--.*sorry" | grep -v "REMOVED\|eliminated\|no.*sorry\|zero.*sorry\|all goals closed"; then - echo "::error::Found 'sorry' in Lean files" - exit 1 - fi - echo "✓ Zero sorry" + - name: Check proof inventory + run: python3 scripts/proof_inventory.py --check diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 4f7b68f5..4e6ac572 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -2,40 +2,51 @@ name: Formal Verification on: push: - branches: [main] - paths: ['GIFT/**', 'GIFTTest/**', 'lakefile.lean', 'lean-toolchain'] + branches: [main, codex/lean-modernization] pull_request: branches: [main] workflow_dispatch: workflow_call: +concurrency: + group: lean-${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + jobs: lean: name: Lean 4 Verification runs-on: ubuntu-latest + env: + LEAN_NUM_THREADS: 2 steps: - uses: actions/checkout@v4 - - name: Install elan run: | - curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y - echo "$HOME/.elan/bin" >> $GITHUB_PATH - - - name: Cache .lake + curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + - name: Cache dependencies uses: actions/cache@v4 with: path: .lake - key: lean-${{ hashFiles('lakefile.lean') }} - - - name: Build + key: lean-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.lean', 'lake-manifest.json') }} + - name: Source checks run: | - lake update - lake exe cache get || true - lake build - - - name: Verify zero sorry + python3 scripts/test_proof_inventory.py + python3 scripts/proof_inventory.py --check --write docs/proof-inventory.json + python3 scripts/update_verification_imports.py --check + git diff --exit-code -- docs/proof-inventory.json + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build and audit proof dependencies run: | - if grep -r "sorry" GIFT/ GIFTTest/ --include="*.lean"; then - echo "ERROR: Found sorry!" - exit 1 - fi + set -o pipefail + lake build + lake build Verification | tee axiom-audit.log + git diff --exit-code -- lake-manifest.json + - name: Upload verification log + if: always() + uses: actions/upload-artifact@v4 + with: + name: axiom-audit + path: axiom-audit.log + if-no-files-found: ignore diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 5deb35ea..332450f7 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -9,15 +9,21 @@ bound, a statement found to say less than it appears to. Org-wide rules (what helps, what does not, house style) are in the [organization CONTRIBUTING](https://github.com/arithmon/.github/blob/main/CONTRIBUTING.md). -This file covers the four procedures this repository owns. +This file covers the procedures this repository owns. + +Use standard mathematical names that describe the actual Lean type. Keep docstrings +for hypotheses, conventions and proof ideas; put research histories in accompanying +documents. Existing public names may be kept as compatibility aliases. + +Routine builds use the committed lockfile. Run `lake update` only during an +intentional dependency migration and commit the updated manifest. ## Build before you open anything -Continuous integration runs `lake build` and then refuses any occurrence of -`sorry` in the Lean sources. A branch that does not build is not reviewable, +Continuous integration runs `lake build` and audits transitive axiom dependencies and rejects proof holes. A branch that does not build is not reviewable, and the policy is not negotiated per pull request. -1. `lake update && lake exe cache get && lake build` must succeed locally. +1. `lake exe cache get && lake build && lake build Verification` must succeed locally. 2. No `sorry`, and no axiom introduced to avoid one. An incomplete proof is better opened as an issue than merged behind a placeholder. 3. Mathlib is the default source of standard results. Restating one locally diff --git a/GIFT.lean b/GIFT.lean index b9783b27..bfafc3d9 100644 --- a/GIFT.lean +++ b/GIFT.lean @@ -1,11 +1,3 @@ --- GIFT: Geometric Integration of Fundamental Topologies --- Main entry point for Lean 4 formalization --- Version: 3.5 (213 certificate conjuncts across 10 master certificates, 15 classified axioms (A-F taxonomy, of which 4 external data packages), 0 sorry) - --- ═══════════════════════════════════════════════════════════════════════════════ --- CORE & RELATIONS --- ═══════════════════════════════════════════════════════════════════════════════ - import GIFT.Core import GIFT.Relations import GIFT.Relations.GaugeSector @@ -13,36 +5,17 @@ import GIFT.Relations.NeutrinoSector import GIFT.Relations.LeptonSector import GIFT.Relations.Cosmology import GIFT.Relations.CompactificationCorrection - --- ═══════════════════════════════════════════════════════════════════════════════ --- MATHEMATICAL FOUNDATIONS --- ═══════════════════════════════════════════════════════════════════════════════ - import GIFT.Foundations import GIFT.Algebraic import GIFT.Geometry - --- Joyce existence theorem import GIFT.Sobolev import GIFT.DifferentialForms import GIFT.ImplicitFunction import GIFT.IntervalArithmetic import GIFT.Joyce - --- Dimensional hierarchy & golden ratio import GIFT.Foundations.GoldenRatioPowers import GIFT.Hierarchy - --- ═══════════════════════════════════════════════════════════════════════════════ --- OBSERVABLES & SPECTRAL THEORY --- ═══════════════════════════════════════════════════════════════════════════════ - import GIFT.Observables import GIFT.Spectral import GIFT.Predictions.CP.DeltaCPNuBarConjecture - --- ═══════════════════════════════════════════════════════════════════════════════ --- CERTIFICATE (modular: Foundations / Predictions / Spectral) --- ═══════════════════════════════════════════════════════════════════════════════ - import GIFT.Certificate.Core diff --git a/GIFT/Algebraic/BettiNumbers.lean b/GIFT/Algebraic/BettiNumbers.lean index bb772e4e..7101d3de 100644 --- a/GIFT/Algebraic/BettiNumbers.lean +++ b/GIFT/Algebraic/BettiNumbers.lean @@ -1,64 +1,31 @@ -/- - GIFT Algebraic Foundations: Betti Numbers from Octonions - ======================================================== - - Betti numbers from octonion combinatorics. - - THIS IS THE KEY FILE: We derive the Betti numbers b₂ and b₃ - from the octonion structure, rather than defining them arbitrarily. - - Main results: - - b₂ = C(|Im(𝕆)|, 2) = C(7,2) = 21 - - b₃ = 3 × b₂ + dim(G₂) = 3 × 21 + 14 = 77 - - H* = b₂ + b₃ + 1 = 99 - - These are NOT arbitrary numbers - they DERIVE from: - - The 7 imaginary units of 𝕆 - - The 14-dimensional automorphism group G₂ --/ - import Mathlib.Data.Nat.Choose.Basic import Mathlib.Tactic.Ring import GIFT.Algebraic.Octonions import GIFT.Algebraic.G2 -namespace GIFT.Algebraic.BettiNumbers - -open Octonions G2 - /-! -## b₂ from Octonion Structure +Arithmetic definitions of the framework parameters b₂, b₃ and H*. +These computations do not identify the parameters with the cohomology of a constructed manifold. +-/ -b₂ = C(7,2) = 21 +namespace GIFT.Algebraic.BettiNumbers -This counts pairs of imaginary units in 𝕆. -Geometrically: 2-forms on a G₂ 7-manifold decompose into -Ω²₇ ⊕ Ω²₁₄ with dimensions 7 + 14 = 21. --/ +open Octonions G2 /-- b₂ defined from octonion imaginary pairs -/ def b2 : ℕ := Nat.choose imaginary_count 2 /-- b₂ = 21 -/ -theorem b2_eq : b2 = 21 := by native_decide +theorem b2_eq : b2 = 21 := by decide /-- b₂ derives from octonion structure -/ theorem b2_from_octonions : b2 = Nat.choose 7 2 := rfl -/-- Alternative: b₂ = Ω²₇ + Ω²₁₄ (G₂ decomposition of 2-forms) -/ +/-- Equality of the arithmetic parameter with the sum of the declared dimensions. -/ theorem b2_from_G2_forms : b2 = G2.omega2_7 + G2.omega2_14 := rfl -/-! -## E₇ Fundamental Representation - -The 56-dimensional fundamental representation of E₇ appears -in the derivation of b₃. - -fund(E₇) = 56 = 2 × b₂ + dim(G₂) = 2 × 21 + 14 --/ - /-- Fundamental representation dimension of E₇ -/ def fund_E7 : ℕ := 56 @@ -72,18 +39,6 @@ theorem fund_E7_decomposition : theorem fund_E7_forms : fund_E7 = imaginary_count + b2 + b2 + imaginary_count := rfl -/-! -## b₃ from Octonion and G₂ Structure - -b₃ = 3 × b₂ + dim(G₂) = 3 × 21 + 14 = 77 - -This formula encodes: -- 3 copies of b₂ (from triple structure in TCS construction) -- Plus the G₂ dimension (from holonomy) - -Equivalently: b₃ = b₂ + fund(E₇) --/ - /-- b₃ defined from b₂ and dim(G₂) -/ def b3 : ℕ := 3 * b2 + dim_G2 @@ -100,14 +55,6 @@ def N_gen : ℕ := 3 theorem b3_with_Ngen : b3 = N_gen * b2 + dim_G2 := rfl -/-! -## H* = Total Hodge Number - -H* = b₂ + b₃ + 1 = 21 + 77 + 1 = 99 - -The "+1" comes from the trivial cohomology H⁰. --/ - /-- Total effective degrees of freedom -/ def H_star : ℕ := b2 + b3 + 1 @@ -121,12 +68,6 @@ theorem H_star_formula : H_star = 4 * b2 + dim_G2 + 1 := rfl theorem H_star_from_octonions : H_star = 4 * Nat.choose imaginary_count 2 + 2 * imaginary_count + 1 := rfl -/-! -## Key Relations - -Verifying that everything is consistent. --/ - /-- b₃ > b₂ (third Betti larger than second) -/ theorem b3_gt_b2 : b3 > b2 := by decide @@ -136,12 +77,6 @@ theorem b3_minus_b2 : b3 - b2 = fund_E7 := rfl /-- H* - 1 = b₂ + b₃ -/ theorem H_star_minus_one : H_star - 1 = b2 + b3 := rfl -/-! -## Ratio Relations (for GIFT constants) - -These ratios are used for physical predictions in GIFTConstants. --/ - /-- b₂ / imaginary_count = 3 (each imaginary appears in 3 pairs) -/ theorem b2_per_imaginary : b2 / imaginary_count = 3 := rfl @@ -150,27 +85,12 @@ theorem denominator_sin2_theta : b3 + dim_G2 = 91 := rfl /-- GCD(21, 91) = 7 (simplifies to 3/13) -/ -theorem sin2_theta_gcd : Nat.gcd 21 91 = 7 := by native_decide +theorem sin2_theta_gcd : Nat.gcd 21 91 = 7 := by decide /-- dim(G₂) / b₂ = 14/21 = 2/3 (Koide ratio) -/ theorem koide_numerator : dim_G2 = 14 := rfl theorem koide_denominator : b2 = 21 := b2_eq -theorem koide_gcd : Nat.gcd 14 21 = 7 := by native_decide - -/-! -## Summary: Derivation Chain - -ℍ → 𝕆 → G₂ → b₂, b₃ → GIFT - -1. 𝕆 has 7 imaginary units (from Cayley-Dickson) -2. G₂ = Aut(𝕆) has dimension 14 = 2×7 -3. b₂ = C(7,2) = 21 (pairs of imaginary units) -4. fund(E₇) = 56 = 2×21 + 14 (from E₇ representation theory) -5. b₃ = b₂ + fund(E₇) = 21 + 56 = 77 -6. H* = b₂ + b₃ + 1 = 99 - -These are DERIVED from algebraic structure, not arbitrary inputs! --/ +theorem koide_gcd : Nat.gcd 14 21 = 7 := by decide /-- Master derivation theorem -/ theorem betti_from_octonions : @@ -180,6 +100,6 @@ theorem betti_from_octonions : b3 = b2 + fund_E7 ∧ H_star = b2 + b3 + 1 ∧ b2 = 21 ∧ b3 = 77 ∧ H_star = 99 := - ⟨rfl, rfl, rfl, rfl, rfl, by native_decide, rfl, rfl⟩ + ⟨rfl, rfl, rfl, rfl, rfl, by decide, rfl, rfl⟩ end GIFT.Algebraic.BettiNumbers diff --git a/GIFT/Algebraic/CayleyDickson.lean b/GIFT/Algebraic/CayleyDickson.lean index 4ae4f7c9..814cc54d 100644 --- a/GIFT/Algebraic/CayleyDickson.lean +++ b/GIFT/Algebraic/CayleyDickson.lean @@ -126,21 +126,21 @@ This decomposes the 21 = C(7,2) pairs of octonion imaginaries. -/ /-- C(3,2) = 3 : pairs within ℍ imaginaries -/ -theorem pairs_in_H : Nat.choose 3 2 = 3 := by native_decide +theorem pairs_in_H : Nat.choose 3 2 = 3 := by decide /-- C(4,2) = 6 : pairs within new imaginaries -/ -theorem pairs_in_new : Nat.choose 4 2 = 6 := by native_decide +theorem pairs_in_new : Nat.choose 4 2 = 6 := by decide /-- 3 × 4 = 12 : mixed pairs (one from ℍ, one new) -/ theorem mixed_pairs : 3 * 4 = 12 := rfl /-- Total: 3 + 6 + 12 = 21 = b₂ -/ theorem pairs_decomposition : - Nat.choose 3 2 + Nat.choose 4 2 + 3 * 4 = 21 := by native_decide + Nat.choose 3 2 + Nat.choose 4 2 + 3 * 4 = 21 := by decide /-- This equals C(7,2) -/ theorem pairs_total : - Nat.choose 3 2 + Nat.choose 4 2 + 3 * 4 = Nat.choose 7 2 := by native_decide + Nat.choose 3 2 + Nat.choose 4 2 + 3 * 4 = Nat.choose 7 2 := by decide /-! ## Quaternion Subalgebras in 𝕆 diff --git a/GIFT/Algebraic/G2.lean b/GIFT/Algebraic/G2.lean index 42a02572..51230cf2 100644 --- a/GIFT/Algebraic/G2.lean +++ b/GIFT/Algebraic/G2.lean @@ -1,37 +1,15 @@ -/- - GIFT Algebraic Foundations: G₂ as Aut(𝕆) - ========================================= - - G₂ = Aut(𝕆): automorphism group of octonions. - - G₂ is defined as the automorphism group of the octonions: - G₂ = Aut(𝕆) - - Key facts: - - G₂ is one of the 5 exceptional simple Lie groups - - dim(G₂) = 14 - - rank(G₂) = 2 - - G₂ acts transitively on S⁶ ⊂ Im(𝕆) - - G₂ is the holonomy group of 7-manifolds with special geometry - - The dimension 14 = 2 × 7 is NOT a coincidence: - - 7 = |Im(𝕆)| - - G₂ preserves a 3-form and 4-form on ℝ⁷ --/ - import Mathlib.Data.Nat.Basic import GIFT.Algebraic.Octonions +/-! +Declared dimensions and arithmetic identities associated with G₂ representations. +The Lie algebra and stabilizer computations are developed in the dedicated tensor modules. +-/ + namespace GIFT.Algebraic.G2 open Octonions -/-! -## G₂ Definition and Basic Properties - -G₂ is the automorphism group of 𝕆, preserving both addition and multiplication. --/ - /-- Dimension of G₂ -/ def dim_G2 : ℕ := 14 @@ -42,17 +20,6 @@ def rank_G2 : ℕ := 2 theorem rank_G2_eq : rank_G2 = 2 := rfl -/-! -## The Fundamental Relation: dim(G₂) = 2 × 7 - -This is not arbitrary! G₂ acts on the 7-sphere S⁶ ⊂ Im(𝕆). -The dimension 14 comes from: -- G₂ preserves a cross product on ℝ⁷ -- This is equivalent to preserving octonion multiplication -- The stabilizer of a point in S⁶ is SU(3), with dim = 8 -- dim(G₂) = dim(S⁶) + dim(SU(3)) = 6 + 8 = 14 --/ - /-- Key relation: dim(G₂) = 2 × |Im(𝕆)| -/ theorem dim_G2_from_imaginary : dim_G2 = 2 * imaginary_count := rfl @@ -66,24 +33,14 @@ def dim_SU3 : ℕ := 8 theorem dim_G2_fibration : dim_G2 = dim_S6 + dim_SU3 := rfl -/-! -## G₂ and Differential Forms - -G₂ can be characterized by the forms it preserves on ℝ⁷: -- A 3-form φ (the "associative" form) -- A 4-form *φ (the "coassociative" form) - -The space of G₂-invariant forms gives GIFT's b₂ and b₃! --/ - /-- On a G₂-manifold, Ω² splits as Ω²₇ ⊕ Ω²₁₄ -/ def omega2_7 : ℕ := 7 def omega2_14 : ℕ := 14 theorem omega2_decomposition : omega2_7 + omega2_14 = 21 := rfl -/-- This is b₂! The 21 comes from 2-forms on a G₂ 7-manifold -/ -theorem omega2_total_eq_b2 : omega2_7 + omega2_14 = Nat.choose 7 2 := by native_decide +/-- The declared summands add to the number of coordinate two-form components. -/ +theorem omega2_total_eq_b2 : omega2_7 + omega2_14 = Nat.choose 7 2 := by decide /-- On a G₂-manifold, Ω³ splits as Ω³₁ ⊕ Ω³₇ ⊕ Ω³₂₇ -/ def omega3_1 : ℕ := 1 @@ -92,45 +49,13 @@ def omega3_27 : ℕ := 27 theorem omega3_decomposition : omega3_1 + omega3_7 + omega3_27 = 35 := rfl -theorem omega3_total : omega3_1 + omega3_7 + omega3_27 = Nat.choose 7 3 := by native_decide - -/-! -## G₂ Holonomy and 7-Manifolds - -A 7-manifold with G₂ holonomy has special properties: -- Ricci-flat (hence good for physics) -- Parallel spinor (supersymmetry) -- Betti numbers constrained by G₂ structure - -The K₇ manifolds in GIFT have G₂ holonomy! --/ +theorem omega3_total : omega3_1 + omega3_7 + omega3_27 = Nat.choose 7 3 := by decide /-- K₇ manifold dimension -/ def K7_dim : ℕ := 7 theorem K7_dim_eq_imaginary : K7_dim = imaginary_count := rfl --- G₂ holonomy constrains Betti numbers --- For a compact G₂ manifold M: --- b₁(M) = 0 (from holonomy) --- b₂(M) = number of linearly independent 2-forms in Ω²₇ --- b₃(M) = b₄(M) from Poincaré duality - -/-! -## Connection to E-Series - -G₂ is part of the exceptional series: -G₂ ⊂ F₄ ⊂ E₆ ⊂ E₇ ⊂ E₈ - -Dimensions: -- G₂: 14 -- F₄: 52 -- E₆: 78 -- E₇: 133 -- E₈: 248 - -G₂ appears as a subgroup in all larger exceptionals. --/ /-- Exceptional group dimensions -/ def dim_F4 : ℕ := 52 @@ -145,20 +70,6 @@ theorem F4_from_Jordan : dim_F4 = 52 := rfl theorem exceptional_relation : dim_E8 - dim_E7 - dim_G2 = 101 := rfl -/-! -## G₂ and the Fano Plane - -G₂ is the symmetry group of the Fano plane PG(2,2). -The Fano plane has: -- 7 points (= imaginary units of 𝕆) -- 7 lines (= quaternionic subalgebras) -- Each point on 3 lines -- Each line through 3 points - -|Aut(Fano)| = 168 = 3 × 56 = 3 × fund(E₇) -This is PSL(2,7), closely related to G₂. --/ - /-- Order of PSL(2,7) = Aut(Fano plane) -/ def order_PSL27 : ℕ := 168 @@ -172,19 +83,6 @@ theorem order_PSL27_alt : order_PSL27 = 3 * 56 := rfl Note: Using literals to avoid circular import with BettiNumbers -/ theorem magic_168 : order_PSL27 = 8 * 21 := rfl -/-! -## Summary: Why dim(G₂) = 14 - -Multiple derivations: -1. Aut(𝕆) preserving multiplication: 14 independent generators -2. Acting on S⁶: dim(G₂) = dim(S⁶) + dim(stabilizer) = 6 + 8 -3. Lie algebra structure: rank 2, with root system giving dim = 14 -4. From imaginary units: 2 × |Im(𝕆)| = 2 × 7 = 14 - -This is NOT an arbitrary constant - it's determined by the -algebraic structure of the octonions. --/ - /-- Master theorem: dim(G₂) derives from octonion structure -/ theorem dim_G2_derived : dim_G2 = 2 * imaginary_count ∧ diff --git a/GIFT/Algebraic/GIFTConstants.lean b/GIFT/Algebraic/GIFTConstants.lean index 0c0e5185..ff205563 100644 --- a/GIFT/Algebraic/GIFTConstants.lean +++ b/GIFT/Algebraic/GIFTConstants.lean @@ -51,7 +51,7 @@ theorem sin2_theta_W_den_eq : sin2_theta_W_den = 91 := rfl theorem sin2_theta_W_fraction : sin2_theta_W_num * 91 = 21 * sin2_theta_W_den := rfl /-- GCD(21, 91) = 7, so simplified form is 3/13 -/ -theorem sin2_theta_W_gcd : Nat.gcd 21 91 = 7 := by native_decide +theorem sin2_theta_W_gcd : Nat.gcd 21 91 = 7 := by decide /-- sin²θ_W simplified: 21/91 = 3/13 (cross-multiply check) -/ theorem sin2_theta_W_simplified : 21 * 13 = 3 * 91 := rfl @@ -64,7 +64,7 @@ def sin2_theta_W_den_simp : ℕ := 13 theorem sin2_theta_W_simp : sin2_theta_W_num / Nat.gcd 21 91 = sin2_theta_W_num_simp ∧ sin2_theta_W_den / Nat.gcd 21 91 = sin2_theta_W_den_simp := by - constructor <;> native_decide + constructor <;> decide /-! ## Koide Ratio: Q = 2/3 @@ -83,7 +83,7 @@ theorem Q_Koide_num_eq : Q_Koide_num = 14 := rfl theorem Q_Koide_den_eq : Q_Koide_den = 21 := rfl /-- GCD(14, 21) = 7 -/ -theorem Q_Koide_gcd : Nat.gcd 14 21 = 7 := by native_decide +theorem Q_Koide_gcd : Nat.gcd 14 21 = 7 := by decide /-- Q = 14/21 = 2/3 (cross-multiply check) -/ theorem Q_Koide_simplified : 14 * 3 = 2 * 21 := rfl @@ -152,7 +152,7 @@ theorem kappa_T_inv_eq : kappa_T_inv = 61 := rfl theorem kappa_T_inv_formula : kappa_T_inv = BettiNumbers.fund_E7 + Octonions.imaginary_count - 2 := rfl /-- 61 is prime! -/ -theorem kappa_T_inv_prime : Nat.Prime 61 := by native_decide +theorem kappa_T_inv_prime : Nat.Prime 61 := by decide /-! ## γ_GIFT (Master Ratio) @@ -181,7 +181,7 @@ theorem gamma_denominator_eq : gamma_denominator = 884 := rfl theorem gamma_denominator_formula : gamma_denominator = 10 * G2.dim_G2 + 3 * dim_E8 := rfl /-- GCD(511, 884) = 1 (already in lowest terms) -/ -theorem gamma_irreducible : Nat.gcd 511 884 = 1 := by native_decide +theorem gamma_irreducible : Nat.gcd 511 884 = 1 := by decide /-! ## Additional GIFT Ratios @@ -194,7 +194,7 @@ theorem alpha_strong_num : BettiNumbers.H_star - BettiNumbers.b2 = 78 := rfl theorem alpha_strong_E6 : BettiNumbers.H_star - BettiNumbers.b2 = G2.dim_E6 := rfl /-- Dark matter ratio: b₂/rank(E₈) = 21/8 (in lowest terms) -/ -theorem dark_matter_gcd : Nat.gcd BettiNumbers.b2 rank_E8 = 1 := by native_decide +theorem dark_matter_gcd : Nat.gcd BettiNumbers.b2 rank_E8 = 1 := by decide /-! ## Complete Derivation Chain diff --git a/GIFT/Algebraic/Quaternions.lean b/GIFT/Algebraic/Quaternions.lean index 8aae8a00..317ee092 100644 --- a/GIFT/Algebraic/Quaternions.lean +++ b/GIFT/Algebraic/Quaternions.lean @@ -38,11 +38,11 @@ instance K4_DecidableRel : DecidableRel K4.Adj := fun v w => else isTrue h /-- K₄ has 6 edges = C(4,2) -/ -theorem K4_card_edges : K4.edgeFinset.card = 6 := by native_decide +theorem K4_card_edges : K4.edgeFinset.card = 6 := by decide /-- Each vertex of K₄ has degree 3 -/ theorem K4_degree (v : Fin 4) : K4.degree v = 3 := by - fin_cases v <;> native_decide + fin_cases v <;> decide /-! ## Quaternion Dimension Constants @@ -93,13 +93,13 @@ Perfect matchings in K₄: -/ /-- K₄ has C(4,2) = 6 edges -/ -theorem K4_edges_eq_choose : K4.edgeFinset.card = Nat.choose 4 2 := by native_decide +theorem K4_edges_eq_choose : K4.edgeFinset.card = Nat.choose 4 2 := by decide /-- C(4,2) = 6 -/ -theorem choose_4_2 : Nat.choose 4 2 = 6 := by native_decide +theorem choose_4_2 : Nat.choose 4 2 = 6 := by decide /-- 6 edges, 3 pairs of opposite edges = 3 imaginary units -/ -theorem K4_opposite_pairs : Nat.choose 4 2 / 2 = imaginary_count := by native_decide +theorem K4_opposite_pairs : Nat.choose 4 2 / 2 = imaginary_count := by decide /-- Each imaginary corresponds to a pair of opposite edges -/ theorem matching_count : 3 = imaginary_count := rfl diff --git a/GIFT/Algebraic/SO16Decomposition.lean b/GIFT/Algebraic/SO16Decomposition.lean index c6a20ee2..1ab680a3 100644 --- a/GIFT/Algebraic/SO16Decomposition.lean +++ b/GIFT/Algebraic/SO16Decomposition.lean @@ -28,13 +28,13 @@ dim(SO(n)) = n(n-1)/2 def dim_SO (n : ℕ) : ℕ := n * (n - 1) / 2 /-- SO(16) has dimension 120 -/ -theorem dim_SO16 : dim_SO 16 = 120 := by native_decide +theorem dim_SO16 : dim_SO 16 = 120 := by decide /-- SO(7) has dimension 21 -/ -theorem dim_SO7 : dim_SO 7 = 21 := by native_decide +theorem dim_SO7 : dim_SO 7 = 21 := by decide /-- SO(8) has dimension 28 -/ -theorem dim_SO8 : dim_SO 8 = 28 := by native_decide +theorem dim_SO8 : dim_SO 8 = 28 := by decide /-! ## Spinor Representations @@ -49,7 +49,7 @@ def spinor_SO16 : ℕ := 128 theorem spinor_SO16_eq : spinor_SO16 = 128 := rfl /-- Spinor dimension from octonions: 2^|Im(O)| = 2^7 = 128 -/ -theorem spinor_from_octonions : (2 : ℕ) ^ imaginary_count = 128 := by native_decide +theorem spinor_from_octonions : (2 : ℕ) ^ imaginary_count = 128 := by decide /-! ## Geometric Part: Topology of K₇ @@ -69,7 +69,7 @@ def geometric_part : ℕ := b2 + b3 + G2.dim_G2 + rank_E8 /-- Geometric part equals dim(SO(16)) = 120 -/ theorem geometric_is_SO16 : geometric_part = 120 := by unfold geometric_part b2 b3 G2.dim_G2 rank_E8 - native_decide + decide /-- Geometric part equals dim(SO(16)) directly -/ theorem geometric_eq_dim_SO16 : geometric_part = dim_SO 16 := by @@ -88,7 +88,7 @@ def spinorial_part : ℕ := 2 ^ imaginary_count /-- Spinorial part equals 128 -/ theorem spinorial_is_128 : spinorial_part = 128 := by unfold spinorial_part imaginary_count - native_decide + decide /-- Spinorial part equals SO(16) spinor -/ theorem spinorial_eq_spinor_SO16 : spinorial_part = spinor_SO16 := by @@ -104,18 +104,18 @@ dim(E₈) = 248 = 120 + 128 = geometric + spinorial theorem E8_SO16_decomposition : dim_E8 = geometric_part + spinorial_part := by unfold dim_E8 geometric_part spinorial_part - native_decide + decide /-- Alternative: dim(E₈) = dim(SO(16)) + spinor(SO(16)) -/ theorem E8_equals_SO16_plus_spinor : dim_E8 = dim_SO 16 + spinor_SO16 := by unfold dim_E8 dim_SO spinor_SO16 - native_decide + decide /-- Physical interpretation: geometry → gauge bosons, octonions → fermions -/ theorem gauge_fermion_split : dim_E8 = (b2 + b3 + G2.dim_G2 + rank_E8) + 2^imaginary_count := by - native_decide + decide /-! ## Detailed Component Breakdown @@ -128,7 +128,7 @@ theorem geometric_breakdown : 21 + 77 + 14 + 8 = 120 := rfl theorem total_breakdown : 120 + 128 = 248 := rfl /-- The split preserves E₈ dimension -/ -theorem split_preserves_dim : dim_SO 16 + spinor_SO16 = 248 := by native_decide +theorem split_preserves_dim : dim_SO 16 + spinor_SO16 = 248 := by decide /-! ## Summary diff --git a/GIFT/Certificate/Core.lean b/GIFT/Certificate/Core.lean index e55118aa..712a47b2 100644 --- a/GIFT/Certificate/Core.lean +++ b/GIFT/Certificate/Core.lean @@ -2,32 +2,10 @@ import GIFT.Certificate.Foundations import GIFT.Certificate.Predictions import GIFT.Certificate.Spectral -/-! -# GIFT Master Certificate - -The single theorem proving GIFT is certified: - Foundations ∧ Predictions ∧ Spectral - -Structure: -- **Foundations**: E₈ root system, G₂ cross product, octonion bridge, - K₇ topology, Hodge theory, Joyce existence, conformal rigidity -- **Predictions**: 33+ published dimensionless derivations, V5.0 observables, - Fano selection, sector classification, hierarchy -- **Spectral**: Mass gap 14/99, TCS bounds, selection principle, - Cheeger inequality, Yang-Mills, spectral scaling - -Replaces the legacy monolithic Certificate.lean. --/ - namespace GIFT.Certificate -/-- GIFT Master Certificate: the entire framework is formally verified. - -Three independent pillars: -1. **Foundations** — Mathematical infrastructure (E₈, G₂, octonions, K₇, Joyce) -2. **Predictions** — Published dimensionless relations and observables -3. **Spectral** — Spectral gap programme (mass gap, TCS, selection) --/ +/-- Conjunction of the three exported statements, under their respective dependencies. +This theorem does not establish the physical interpretation of the numerical relations. -/ theorem gift_master_certificate : Foundations.statement ∧ Predictions.statement ∧ diff --git a/GIFT/Foundations/Analysis.lean b/GIFT/Foundations/Analysis.lean index 8432a9d4..e49d21a9 100644 --- a/GIFT/Foundations/Analysis.lean +++ b/GIFT/Foundations/Analysis.lean @@ -1,13 +1,3 @@ --- GIFT Foundations Analysis Aggregator --- Bundles all Analysis submodules for convenient import --- --- Usage: --- import GIFT.Foundations.Analysis --- instead of: --- import GIFT.Foundations.Analysis.InnerProductSpace --- import GIFT.Foundations.Analysis.ExteriorAlgebra --- ...etc (8 imports) - import GIFT.Foundations.Analysis.InnerProductSpace import GIFT.Foundations.Analysis.ExteriorAlgebra import GIFT.Foundations.Analysis.E8Lattice @@ -18,56 +8,5 @@ import GIFT.Foundations.Analysis.G2TensorForm import GIFT.Foundations.Analysis.JoyceAnalytic import GIFT.Foundations.Analysis.AnalyticalFoundations import GIFT.Foundations.Analysis.K7Orthonormality - -namespace GIFT.Foundations.Analysis - -/-! -# Analysis Module Overview - -This module collects advanced analytical foundations for GIFT: - -## Inner Product Spaces (InnerProductSpace.lean) -- ℝ⁷ and ℝ⁸ inner product formalization -- Norm and orthogonality - -## Exterior Algebra (ExteriorAlgebra.lean) -- Λᵏ(V) construction -- Wedge product properties - -## E₈ Lattice (E8Lattice.lean) -- Lattice vectors and closure -- Weyl reflections - -## Wedge Product (WedgeProduct.lean) -- Concrete wedge computations -- Basis elements - -## Hodge Theory (HodgeTheory.lean) -- Hodge star operator * -- Harmonic forms ker(Δ) - -## Harmonic Forms (HarmonicForms.lean) -- H^k(M) spaces -- Hodge decomposition - -## G₂ Tensor Form (G2TensorForm.lean) -- Associative 3-form φ₀ -- G₂ structure on ℝ⁷ - -## Joyce Analytic (JoyceAnalytic.lean) -- Analytic framework for Joyce theorem -- Perturbation estimates - -## Analytical Foundations (AnalyticalFoundations.lean) -- Master certificate for Sobolev, Elliptic, IFT -- PINN bounds verification - -## K7 Orthonormality (K7Orthonormality.lean) -- L2 Gram matrices for harmonic 2-forms and 3-forms -- Positive definiteness, condition bounds, Gram-Schmidt --/ - --- Note: This module bundles imports only. Access definitions via their --- original namespaces, e.g., GIFT.Foundations.Analysis.HodgeTheory.* - -end GIFT.Foundations.Analysis +import GIFT.Foundations.Analysis.Sobolev.Box +import GIFT.Foundations.Analysis.SmoothFamily diff --git a/GIFT/Foundations/Analysis/Elliptic/Basic.lean b/GIFT/Foundations/Analysis/Elliptic/Basic.lean index 5eb5d242..790e31e3 100644 --- a/GIFT/Foundations/Analysis/Elliptic/Basic.lean +++ b/GIFT/Foundations/Analysis/Elliptic/Basic.lean @@ -1,50 +1,18 @@ -/- -GIFT Foundations: Elliptic Operators -==================================== - -Computational formalization of elliptic operator constants. -Key property: regularity gain (solutions are 2 derivatives smoother than RHS). - -## Background - -For a second-order elliptic operator L (like the Hodge Laplacian): -- If Lu = f and f in H^k, then u in H^{k+2} -- This "regularity gain" of 2 enables bootstrap arguments - -## Design - -We focus on the computable aspects: -1. Regularity gain constants -2. Bootstrap iteration counts -3. Dimensional conditions for embeddings - -Version: 3.3.2 --/ - import GIFT.Core -namespace GIFT.Foundations.Analysis.Elliptic - /-! -## Elliptic Regularity Constants - -An elliptic operator of order 2m gains 2m derivatives. -For the Hodge Laplacian (m = 1), we gain 2 derivatives. +Finite index data and arithmetic for regularity orders. No elliptic operator, +regularity estimate, or identification of these data with a geometric operator is proved here. -/ +namespace GIFT.Foundations.Analysis.Elliptic + /-- Regularity gain for second-order elliptic operators (e.g., Laplacian) -/ def regularity_gain : ℕ := 2 /-- Regularity gain certified -/ theorem regularity_gain_value : regularity_gain = 2 := rfl -/-! -## Fredholm Index - -Elliptic operators on compact manifolds are Fredholm. -For Joyce's linearization, the index is 0. --/ - /-- Fredholm data: kernel and cokernel dimensions -/ structure FredholmIndex where /-- Kernel dimension (finite) -/ @@ -59,15 +27,9 @@ def joyce_fredholm : FredholmIndex where ker_dim := 0 coker_dim := 0 -/-- Joyce Fredholm index is 0 -/ +/-- The index of the declared data is zero. -/ theorem joyce_index_zero : joyce_fredholm.index = 0 := rfl -/-! -## Regularity Bootstrap - -Starting from weak solution, iterate to gain regularity. --/ - /-- Bootstrap iteration data. Given Lu = f with f in H^k, we can bootstrap: @@ -83,42 +45,24 @@ structure BootstrapData (start_reg target_reg : ℕ) where /-- Bootstrap from H^0 to H^4 in 2 steps -/ def bootstrap_H0_H4 : BootstrapData 0 4 where iterations := 2 - reaches_target := by native_decide + reaches_target := by decide /-- Bootstrap from H^0 to H^6 in 3 steps -/ def bootstrap_H0_H6 : BootstrapData 0 6 where iterations := 3 - reaches_target := by native_decide - -/-! -## K7 Application - -For Joyce's 7-manifold K7, we need H^4 embeds in C^0. -Bootstrap: H^0 -> H^2 -> H^4 -> C^0 --/ + reaches_target := by decide /-- Bootstrap for K7: reach C^0 embedding threshold -/ theorem K7_bootstrap_to_continuous : - -- Start at H^0 (L^2) - -- After 2 iterations (gaining 2 each time) - -- Reach H^4 which embeds in C^0 for dim 7 0 + 2 * 2 = 4 ∧ 2 * 4 > 7 := by - constructor <;> native_decide - -/-! -## Certification --/ + constructor <;> decide /-- Elliptic theory constants certified -/ theorem elliptic_certified : - -- Regularity gain for Laplacian (regularity_gain = 2) ∧ - -- Bootstrap steps to H^4 (bootstrap_H0_H4.iterations = 2) ∧ - -- H^4 embeds in C^0 for dim 7 (2 * 4 > 7) ∧ - -- Joyce index is 0 (joyce_fredholm.index = 0) := by - repeat (first | constructor | native_decide | rfl) + repeat (first | constructor | decide | rfl) end GIFT.Foundations.Analysis.Elliptic diff --git a/GIFT/Foundations/Analysis/HodgeTheory.lean b/GIFT/Foundations/Analysis/HodgeTheory.lean index 4d88f032..7072b792 100644 --- a/GIFT/Foundations/Analysis/HodgeTheory.lean +++ b/GIFT/Foundations/Analysis/HodgeTheory.lean @@ -88,7 +88,7 @@ def IsHarmonic {M : Type*} {hd : HodgeData M} (lap : HodgeLaplacian M hd) opaque K7 : Type /-- Betti numbers of K7 -/ -def b (k : ℕ) : ℕ := +abbrev b (k : ℕ) : ℕ := match k with | 0 => 1 | 1 => 0 diff --git a/GIFT/Foundations/Analysis/IFT/Basic.lean b/GIFT/Foundations/Analysis/IFT/Basic.lean index 479988b7..559dd867 100644 --- a/GIFT/Foundations/Analysis/IFT/Basic.lean +++ b/GIFT/Foundations/Analysis/IFT/Basic.lean @@ -1,40 +1,12 @@ -/- -GIFT Foundations: Implicit Function Theorem (Joyce Application) -================================================================ - -Computational aspects of the IFT for Joyce's G2 perturbation theorem. - -## Mathlib's IFT - -Mathlib provides `HasStrictFDerivAt.to_localInverse` which gives: -- For f : E -> F with strict derivative f' : E <-> F at a -- There exists a local inverse g with strict derivative f'^{-1} at f(a) - -Key imports (when available): -- `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv` -- `Mathlib.Analysis.Calculus.Implicit` - -## Application to Joyce - -Joyce's operator F : G2 -> Omega^4 x Omega^5 maps G2 structures to torsion. -- F(phi) = 0 means phi is torsion-free -- DF|_{phi_0} is Fredholm index 0 -- For "generic" phi_0, DF|_{phi_0} is an isomorphism -- IFT then gives: small torsion -> nearby torsion-free - -Version: 3.3.2 --/ - import GIFT.Core -namespace GIFT.Foundations.Analysis.IFT - /-! -## Joyce Hypothesis (Computational) - -The computational conditions for Joyce's theorem. +Rational threshold data retained from the historical numerical model. +The inequalities do not certify a geometric torsion norm or prove an implicit function theorem. -/ +namespace GIFT.Foundations.Analysis.IFT + /-- Joyce hypothesis data (computational bounds). Captures the numerical verification of Joyce's theorem: @@ -55,12 +27,6 @@ structure JoyceHypothesis where /-- PINN verification: torsion < threshold -/ pinn_bound : torsion_bound_num * threshold_den < threshold_num * torsion_bound_den -/-! -## K7 Application - -Concrete numbers for Joyce's K7 manifold. --/ - /-- K7 torsion bound (PINN-computed): 0.00141 -/ def K7_torsion_bound_num : ℕ := 141 def K7_torsion_bound_den : ℕ := 100000 @@ -73,35 +39,28 @@ def K7_threshold_den : ℕ := 10000 theorem K7_pinn_verified : K7_torsion_bound_num * K7_threshold_den < K7_threshold_num * K7_torsion_bound_den := by - native_decide -- 141 * 10000 = 1410000 < 28800000 = 288 * 100000 + decide -- 141 * 10000 = 1410000 < 28800000 = 288 * 100000 /-- Safety margin: threshold/bound > 20 -/ theorem K7_safety_margin : K7_threshold_num * K7_torsion_bound_den > 20 * K7_threshold_den * K7_torsion_bound_num := by - native_decide -- 28800000 > 28200000 = 20 * 10000 * 141 + decide -- 28800000 > 28200000 = 20 * 10000 * 141 -/-- K7 satisfies Joyce hypothesis -/ +/-- The stored data satisfy the rational inequality. -/ def K7_joyce_hypothesis : JoyceHypothesis where torsion_bound_num := K7_torsion_bound_num torsion_bound_den := K7_torsion_bound_den threshold_num := K7_threshold_num threshold_den := K7_threshold_den - hden_pos := by constructor <;> native_decide + hden_pos := by constructor <;> decide pinn_bound := K7_pinn_verified -/-! -## Certification --/ - /-- IFT framework certification -/ theorem ift_certified : - -- PINN bounds verified (K7_torsion_bound_num * K7_threshold_den < K7_threshold_num * K7_torsion_bound_den) ∧ - -- Safety margin (K7_threshold_num * K7_torsion_bound_den > 20 * K7_threshold_den * K7_torsion_bound_num) ∧ - -- Numerical values K7_torsion_bound_num = 141 ∧ K7_threshold_num = 288 := ⟨K7_pinn_verified, K7_safety_margin, rfl, rfl⟩ diff --git a/GIFT/Foundations/Analysis/JoyceAnalytic.lean b/GIFT/Foundations/Analysis/JoyceAnalytic.lean index f088a5f0..2a9c28db 100644 --- a/GIFT/Foundations/Analysis/JoyceAnalytic.lean +++ b/GIFT/Foundations/Analysis/JoyceAnalytic.lean @@ -1,22 +1,14 @@ -/- -GIFT Foundations: Joyce Analytic Theorem -======================================== - -Structure-based formulation of Joyce's perturbation theorem. -Given a G2 structure with small torsion, perturb to torsion-free. - -**V3.3.2 REFACTOR**: Replaced 14 axioms with structure-based approach. -All computational bounds verified via native_decide. - -Version: 3.3.2 --/ - import GIFT.Foundations.Analysis.HodgeTheory import GIFT.Foundations.Analysis.G2Forms.All import GIFT.Foundations.Analysis.Sobolev.Basic import GIFT.Foundations.Analysis.Elliptic.Basic import GIFT.Foundations.Analysis.IFT.Basic +/-! +Arithmetic threshold conditions and the constant form model on real seven-space. +This module does not prove Joyce's perturbation theorem or existence on a compact K7. +-/ + namespace GIFT.Foundations.Analysis.JoyceAnalytic open HodgeTheory @@ -26,35 +18,14 @@ open Sobolev open Elliptic open IFT -/-! -## Sobolev Spaces (Structure-Based) - -Previously axiomatized, now using Sobolev.EmbeddingCondition. -The key computational fact: H^4 embeds in C^0 for 7-manifolds. --/ - -/-- Sobolev embedding for K7: H^4 embeds in C^0 (2 * 4 > 7) -/ -theorem K7_sobolev_embedding : Sobolev.EmbeddingCondition 7 4 := +/-- Numerical Sobolev index condition in dimension seven. -/ +theorem K7_sobolev_index_condition : Sobolev.EmbeddingCondition 7 4 := Sobolev.K7_embedding_condition -/-! -## G2 Structures (Structure-Based) - -Previously axiomatized as `G2Structures M`, now using G2Structure from G2Forms. -The TorsionFree predicate is well-typed: (dφ = 0) ∧ (d⋆φ = 0). --/ - /-- G2 structure from cross product is torsion-free -/ theorem cross_product_torsion_free : CrossProductG2.TorsionFree := crossProductG2_torsionFree -/-! -## Torsion (Structure-Based) - -Previously axiomatized, now expressed via TorsionFree predicate. -A structure has zero torsion iff TorsionFree holds. --/ - /-- Torsion pair: norms of dφ and d⋆φ components -/ structure TorsionPair where dphi_norm : ℝ -- ‖dφ‖ @@ -71,39 +42,19 @@ def zero_torsion : TorsionPair := ⟨0, 0⟩ theorem zero_torsion_norm : torsion_norm zero_torsion = 0 := by simp [torsion_norm, zero_torsion] -/-! -## Joyce Operator (Structure-Based) - -Previously axiomatized as JoyceOp, JoyceLinearization. -Now using Elliptic.FredholmIndex for linearization properties. --/ - -/-- Joyce linearization has Fredholm index 0 -/ +/-- Declared finite-dimensional index data; no operator is constructed here. -/ def joyce_linearization_fredholm : Elliptic.FredholmIndex := Elliptic.joyce_fredholm -/-- Joyce Fredholm index is 0 -/ +/-- The index of the declared data is zero. -/ theorem joyce_index_zero : joyce_linearization_fredholm.index = 0 := Elliptic.joyce_index_zero -/-! -## Joyce's Existence Theorem (Structure-Based) - -Previously axiomatized as joyce_existence, epsilon_joyce, epsilon_pos. -Now using IFT.JoyceHypothesis with PINN-verified bounds. - -The theorem structure: -- Hypothesis: small torsion (PINN-verified) -- Conclusion: exists torsion-free deformation - -We don't axiomatize the implication; we verify the hypothesis computationally. --/ - -/-- K7 satisfies Joyce hypothesis with PINN-verified bounds -/ +/-- Historical rational threshold data. -/ def K7_hypothesis : IFT.JoyceHypothesis := IFT.K7_joyce_hypothesis -/-- PINN verification: K7 torsion < threshold -/ +/-- Comparison of the stored rational numbers. -/ theorem K7_torsion_below_threshold : IFT.K7_torsion_bound_num * IFT.K7_threshold_den < IFT.K7_threshold_num * IFT.K7_torsion_bound_den := @@ -115,24 +66,10 @@ theorem K7_safety_factor : 20 * IFT.K7_threshold_den * IFT.K7_torsion_bound_num := IFT.K7_safety_margin -/-! -## Application to K7 - -Joyce constructed K7 by resolving T^7/Gamma orbifold. -The cross product G2 structure provides a canonical torsion-free structure. --/ - -/-- K7 admits torsion-free G2 structure (from cross product) -/ -theorem K7_admits_torsion_free_G2 : CrossProductG2.TorsionFree := +/-- Torsion vanishes for the constant form model on real seven-space. -/ +theorem constant_model_torsion_free : CrossProductG2.TorsionFree := crossProductG2_torsionFree -/-! -## Quantitative Bounds (PINN Verification) - -Numerical verification shows torsion is well below threshold. -These are the same values as before, now imported from IFT module. --/ - /-- PINN-computed torsion bound: 0.00141 -/ def pinn_torsion_bound_num : ℕ := IFT.K7_torsion_bound_num -- 141 def pinn_torsion_bound_den : ℕ := IFT.K7_torsion_bound_den -- 100000 @@ -151,21 +88,9 @@ theorem safety_margin : joyce_threshold_num * pinn_torsion_bound_den > 20 * joyce_threshold_den * pinn_torsion_bound_num := IFT.K7_safety_margin -/-! -## Moduli Space - -The moduli space of torsion-free G2 structures on K7 has dimension b^3(K7) = 77. --/ - -/-- Moduli dimension equals b^3 -/ +/-- The declared third Betti number equals 77. -/ theorem moduli_dimension : b 3 = 77 := rfl -/-! -## Elliptic Regularity Chain - -Bootstrap from weak to strong solutions via elliptic regularity. --/ - /-- Bootstrap data: H^0 -> H^2 -> H^4 in 2 steps -/ def K7_bootstrap : Elliptic.BootstrapData 0 4 := Elliptic.bootstrap_H0_H4 @@ -174,47 +99,23 @@ def K7_bootstrap : Elliptic.BootstrapData 0 4 := theorem K7_reaches_continuous : 0 + 2 * 2 = 4 ∧ 2 * 4 > 7 := Elliptic.K7_bootstrap_to_continuous -/-! -## Certified Constants --/ - -/-- Joyce analytic certified (all computational, no axioms) -/ +/-- Arithmetic identities and the constant-model torsion predicate. -/ theorem joyce_analytic_certified : - -- PINN bounds pinn_torsion_bound_num = 141 ∧ pinn_torsion_bound_den = 100000 ∧ joyce_threshold_num = 288 ∧ joyce_threshold_den = 10000 ∧ - -- Betti number b 3 = 77 ∧ - -- Fredholm index joyce_linearization_fredholm.index = 0 ∧ - -- Sobolev embedding (2 * 4 > 7) ∧ - -- Cross product is torsion-free CrossProductG2.TorsionFree := by refine ⟨rfl, rfl, rfl, rfl, rfl, rfl, ?_, crossProductG2_torsionFree⟩ - native_decide + decide -/-! -## Summary: Axiom Reduction - -**Before (v3.2.0)**: 14 axioms -- Sobolev, Sobolev_banach, sobolev_norm, sobolev_embedding -- G2Structures, Torsion -- JoyceOp, JoyceLinearization -- epsilon_joyce, epsilon_pos, joyce_existence -- K7_initial_G2, K7_torsion_bound - -**After (v3.3.2)**: 0 axioms -- Sobolev conditions: EmbeddingCondition with native_decide -- G2 structures: G2Structure from G2Forms -- Torsion: TorsionFree predicate -- Joyce operator: FredholmIndex structure -- Existence: JoyceHypothesis with PINN verification -- K7: CrossProductG2.TorsionFree proven - -All proofs are either definitional (rfl) or computational (native_decide). --/ +/-- Historical name; the conclusion concerns only the constant model. -/ +abbrev K7_admits_torsion_free_G2 := constant_model_torsion_free + +/-- Historical name for the numerical index condition. -/ +abbrev K7_sobolev_embedding := K7_sobolev_index_condition end GIFT.Foundations.Analysis.JoyceAnalytic diff --git a/GIFT/Foundations/Analysis/SmoothFamily.lean b/GIFT/Foundations/Analysis/SmoothFamily.lean new file mode 100644 index 00000000..41b0c354 --- /dev/null +++ b/GIFT/Foundations/Analysis/SmoothFamily.lean @@ -0,0 +1,84 @@ +/- +Copyright 2026 Anthropic, PBC. Licensed under the Apache License, Version 2.0. +Adapted from anthropics/fermats-last-theorem at aa2d8b34692b16c70f699536de0d8e75b9a3e9ef. +Source: P2M/Sol/S_ContDiff_exists_forall_norm_iteratedDeriv_slice_le_of_isCompact.lean +Modifications: removed pipeline namespaces and utilities; restored mathematical names. +See LICENSES/Apache-2.0.txt and NOTICE. +-/ + +import Mathlib + +set_option autoImplicit false + +namespace SmoothFamily + +variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] + +noncomputable def dU (G : E × ℝ → F) : ℕ → (E × ℝ → F) + | 0 => G + | n + 1 => fun p => fderiv ℝ (dU G n) p (0, 1) + +theorem contDiff_dU (G : E × ℝ → F) (hG : ContDiff ℝ (⊤ : ℕ∞) G) : ∀ n, ContDiff ℝ (⊤ : ℕ∞) (dU G n) := by + intro n + induction n with + | zero => exact hG + | succ n ih => + show ContDiff ℝ (⊤ : ℕ∞) (fun p => fderiv ℝ (dU G n) p (0, 1)) + have h1 : ContDiff ℝ (⊤ : ℕ∞) (fderiv ℝ (dU G n)) := ih.fderiv_right (by simp) + exact h1.clm_apply contDiff_const + +theorem iteratedDeriv_slice (G : E × ℝ → F) (hG : ContDiff ℝ (⊤ : ℕ∞) G) : + ∀ (n : ℕ) (a : E) (u : ℝ), iteratedDeriv n (fun u => G (a, u)) u = dU G n (a, u) := by + intro n + induction n with + | zero => intro a u; rfl + | succ n ih => + intro a u + rw [iteratedDeriv_succ] + have hfun : iteratedDeriv n (fun u => G (a, u)) = fun u => dU G n (a, u) := funext (ih a) + rw [hfun] + show deriv (fun u => dU G n (a, u)) u = fderiv ℝ (dU G n) (a, u) (0, 1) + have hd : DifferentiableAt ℝ (dU G n) (a, u) := + ((contDiff_dU G hG n).differentiable (by simp)).differentiableAt + have hγ : HasDerivAt (fun u : ℝ => ((a, u) : E × ℝ)) ((0 : E), (1 : ℝ)) u := + (hasDerivAt_const u a).prodMk (hasDerivAt_id u) + exact (hd.hasFDerivAt.comp_hasDerivAt u hγ).deriv + +theorem main {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] + [NormedAddCommGroup F] [NormedSpace ℝ F] + (Ψ : E → ℝ → F) (hΨ : ContDiff ℝ (⊤ : ℕ∞) (fun p : E × ℝ => Ψ p.1 p.2)) + (S : Set E) (hS : IsCompact S) (R : ℝ) (N : ℕ) : + (∀ a : E, ContDiff ℝ N (Ψ a)) ∧ + ∃ C : ℝ, 0 ≤ C ∧ ∀ a ∈ S, ∀ u ∈ Set.Icc (-R) R, ∀ n ≤ N, ‖iteratedDeriv n (Ψ a) u‖ ≤ C := by + set G : E × ℝ → F := fun p => Ψ p.1 p.2 with hGdef + have hslice : ∀ a : E, ContDiff ℝ (⊤ : ℕ∞) (Ψ a) := fun a => by + have : Ψ a = G ∘ fun u : ℝ => ((a, u) : E × ℝ) := rfl + rw [this] + exact hΨ.comp (contDiff_const.prodMk contDiff_id) + refine ⟨fun a => (hslice a).of_le (by exact_mod_cast le_top), ?_⟩ + + have hK : IsCompact (S ×ˢ Set.Icc (-R) R) := hS.prod isCompact_Icc + have hb : ∀ n : ℕ, ∃ Cn : ℝ, ∀ p ∈ S ×ˢ Set.Icc (-R) R, ‖dU G n p‖ ≤ Cn := fun n => + hK.exists_bound_of_continuousOn ((contDiff_dU G hΨ n).continuous.continuousOn) + choose Cn hCn using hb + refine ⟨∑ n ∈ Finset.range (N + 1), |Cn n|, Finset.sum_nonneg fun n _ => abs_nonneg _, ?_⟩ + intro a ha u hu n hn + have hmem : ((a, u) : E × ℝ) ∈ S ×ˢ Set.Icc (-R) R := ⟨ha, hu⟩ + have h1 : ‖iteratedDeriv n (Ψ a) u‖ ≤ |Cn n| := by + rw [show Ψ a = fun u => G (a, u) from rfl, iteratedDeriv_slice G hΨ n a u] + exact (hCn n _ hmem).trans (le_abs_self _) + refine h1.trans ?_ + exact Finset.single_le_sum (f := fun n => |Cn n|) (fun n _ => abs_nonneg _) + (Finset.mem_range.mpr (Nat.lt_succ_of_le hn)) + +end SmoothFamily + +theorem ContDiff.exists_forall_norm_iteratedDeriv_slice_le_of_isCompact + {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] + [NormedAddCommGroup F] [NormedSpace ℝ F] + (Ψ : E → ℝ → F) (hΨ : ContDiff ℝ (⊤ : ℕ∞) (fun p : E × ℝ => Ψ p.1 p.2)) + (S : Set E) (hS : IsCompact S) (R : ℝ) (N : ℕ) : + (∀ a : E, ContDiff ℝ N (Ψ a)) ∧ + ∃ C : ℝ, 0 ≤ C ∧ ∀ a ∈ S, ∀ u ∈ Set.Icc (-R) R, ∀ n ≤ N, ‖iteratedDeriv n (Ψ a) u‖ ≤ C := + SmoothFamily.main Ψ hΨ S hS R N + diff --git a/GIFT/Foundations/Analysis/Sobolev/Basic.lean b/GIFT/Foundations/Analysis/Sobolev/Basic.lean index 0f0289c2..caeada93 100644 --- a/GIFT/Foundations/Analysis/Sobolev/Basic.lean +++ b/GIFT/Foundations/Analysis/Sobolev/Basic.lean @@ -1,63 +1,37 @@ -/- -GIFT Foundations: Sobolev Spaces (Abstract Framework) -===================================================== - -Typeclass-based abstraction for Sobolev spaces. -This provides an interface that can be instantiated when Mathlib -adds proper Sobolev space support. - -## Design Philosophy - -Since Mathlib (as of 2026) lacks Sobolev spaces, we use a typeclass -approach that: -1. Captures essential properties as fields (not axioms) -2. Allows computational proofs of dimensional conditions -3. Enables future instantiation with concrete Sobolev spaces - -## Key Insight - -The embedding H^k ↪ C^0 when k > n/2 has two parts: -- Dimensional condition (k > n/2) — COMPUTABLE -- Actual embedding — ABSTRACT (structure field) +import GIFT.Core -Version: 3.3.2 +/-! +Numerical Sobolev index conditions. These statements concern natural numbers; +they do not construct Sobolev spaces or prove a continuous embedding. -/ -import GIFT.Core - namespace GIFT.Foundations.Analysis.Sobolev /-- Dimensional condition for Sobolev embedding H^k into C^0. For a manifold of dimension n, H^k embeds into C^0 when 2k > n. -This is a computational condition we can verify with native_decide. -/ +This is a computational condition we can verify with decide. -/ structure EmbeddingCondition (n k : ℕ) : Prop where condition : 2 * k > n -/-- H^4 embeds into C^0 for 7-manifolds (2 * 4 = 8 > 7) -/ -theorem embedding_H4_C0_dim7 : EmbeddingCondition 7 4 := - ⟨by native_decide⟩ +/-- Numerical condition `2 * 4 > 7`. -/ +theorem sobolev_index_condition_dim7_order4 : EmbeddingCondition 7 4 := + ⟨by decide⟩ -/-- H^5 embeds into C^1 for 7-manifolds -/ -theorem embedding_H5_C1_dim7 : EmbeddingCondition 9 5 := - ⟨by native_decide⟩ -- 2 * 5 = 10 > 9 (n + 2j = 7 + 2 = 9) +/-- Numerical condition `2 * 5 > 7 + 2`. -/ +theorem sobolev_index_condition_dim7_order5_deriv1 : EmbeddingCondition 9 5 := + ⟨by decide⟩ -- 2 * 5 = 10 > 9 (n + 2j = 7 + 2 = 9) -/-- H^6 embeds into C^2 for 7-manifolds -/ -theorem embedding_H6_C2_dim7 : EmbeddingCondition 11 6 := - ⟨by native_decide⟩ -- 2 * 6 = 12 > 11 +/-- Numerical condition `2 * 6 > 7 + 4`. -/ +theorem sobolev_index_condition_dim7_order6_deriv2 : EmbeddingCondition 11 6 := + ⟨by decide⟩ -- 2 * 6 = 12 > 11 -/-- General embedding chain for 7-manifolds -/ -theorem embedding_chain_dim7 : +/-- Three numerical index conditions in dimension seven. -/ +theorem sobolev_index_conditions_dim7 : EmbeddingCondition 7 4 ∧ EmbeddingCondition 9 5 ∧ EmbeddingCondition 11 6 := - ⟨embedding_H4_C0_dim7, embedding_H5_C1_dim7, embedding_H6_C2_dim7⟩ - -/-! -## K7-Specific Constants - -For Joyce's 7-manifold K7. --/ + ⟨sobolev_index_condition_dim7_order4, sobolev_index_condition_dim7_order5_deriv1, sobolev_index_condition_dim7_order6_deriv2⟩ /-- Manifold dimension for K7 -/ def K7_dim : ℕ := 7 @@ -65,9 +39,9 @@ def K7_dim : ℕ := 7 /-- Critical Sobolev index for C^0 embedding on K7 -/ def K7_critical_index : ℕ := 4 -/-- K7 satisfies H^4 ↪ C^0 embedding condition -/ -theorem K7_embedding_condition : EmbeddingCondition K7_dim K7_critical_index := - ⟨by native_decide⟩ +/-- The declared dimension and order satisfy the numerical index condition. -/ +theorem K7_sobolev_index_condition : EmbeddingCondition K7_dim K7_critical_index := + ⟨by decide⟩ /-- Elliptic regularity gain (derivatives gained from Δu = f) -/ def elliptic_gain : ℕ := 2 @@ -78,22 +52,22 @@ def bootstrap_steps : ℕ := 2 /-- Bootstrap reaches critical index -/ theorem bootstrap_reaches_critical : bootstrap_steps * elliptic_gain = K7_critical_index := by - native_decide - -/-! -## Certification --/ + decide /-- All Sobolev dimensional conditions certified -/ theorem sobolev_conditions_certified : - -- H^4 ↪ C^0 for dim 7 (2 * 4 > 7) ∧ - -- H^5 ↪ C^1 for dim 7 (2 * 5 > 9) ∧ - -- Bootstrap works (2 * 2 = 4) ∧ - -- Critical index correct (K7_critical_index = 4) := by - repeat (first | constructor | native_decide | rfl) + repeat (first | constructor | decide | rfl) + + +/-- Compatibility names for the numerical conditions; these do not assert embeddings. -/ +abbrev embedding_H4_C0_dim7 := sobolev_index_condition_dim7_order4 +abbrev embedding_H5_C1_dim7 := sobolev_index_condition_dim7_order5_deriv1 +abbrev embedding_H6_C2_dim7 := sobolev_index_condition_dim7_order6_deriv2 +abbrev embedding_chain_dim7 := sobolev_index_conditions_dim7 +abbrev K7_embedding_condition := K7_sobolev_index_condition end GIFT.Foundations.Analysis.Sobolev diff --git a/GIFT/Foundations/Analysis/Sobolev/Box.lean b/GIFT/Foundations/Analysis/Sobolev/Box.lean new file mode 100644 index 00000000..0676873b --- /dev/null +++ b/GIFT/Foundations/Analysis/Sobolev/Box.lean @@ -0,0 +1,374 @@ +/- +Copyright 2026 Anthropic, PBC. Licensed under the Apache License, Version 2.0. +Adapted from anthropics/fermats-last-theorem at aa2d8b34692b16c70f699536de0d8e75b9a3e9ef. +Source: P2M/Sol/S_Sobolev_exists_forall_norm_le_mul_sum_sqrt_integral_norm_iteratedFDeriv_sq_of_contDiff_box.lean +Modifications: removed pipeline namespaces and utilities; restored mathematical names. +See LICENSES/Apache-2.0.txt and NOTICE. +-/ + +import Mathlib + +set_option autoImplicit false + +open MeasureTheory Set Function +open scoped ENNReal Interval + +namespace SobolevBox + +variable {n : ℕ} + +theorem norm_le_inv_mul_integral_add_integral + (ℓ : ℝ) (hℓ : 0 < ℓ) (α : ℝ) (g : (Fin n → ℝ) → ℂ) (hg : ContDiff ℝ 1 g) + (x : Fin n → ℝ) (i : Fin n) (hx : x i ∈ Icc α (α + ℓ)) : + ‖g x‖ ≤ ℓ⁻¹ * (∫ t in Icc α (α + ℓ), ‖g (update x i t)‖) + + ∫ t in Icc α (α + ℓ), ‖fderiv ℝ g (update x i t) (Pi.single i 1)‖ := by + set φ : ℝ → ℂ := fun t => g (update x i t) with hφ_def + set φ' : ℝ → ℂ := fun t => fderiv ℝ g (update x i t) (Pi.single i 1) with hφ'_def + change ‖g x‖ ≤ ℓ⁻¹ * (∫ t in Icc α (α + ℓ), ‖φ t‖) + ∫ t in Icc α (α + ℓ), ‖φ' t‖ + have hgd : Differentiable ℝ g := hg.differentiable one_ne_zero + have hupd : Continuous fun t : ℝ => update x i t := continuous_const.update i continuous_id + have hφc : Continuous φ := hg.continuous.comp hupd + have hφ'c : Continuous φ' := + ((hg.continuous_fderiv one_ne_zero).comp hupd).clm_apply continuous_const + have hder : ∀ t, HasDerivAt φ (φ' t) t := fun t => + (hgd _).hasFDerivAt.comp_hasDerivAt t (hasDerivAt_update x i t) + have hftc : ∀ s, φ (x i) - φ s = ∫ t in s..x i, φ' t := fun s => + (intervalIntegral.integral_eq_sub_of_hasDerivAt (fun t _ => hder t) + (hφ'c.intervalIntegrable _ _)).symm + set I₀ : ℝ := ∫ t in Icc α (α + ℓ), ‖φ t‖ with hI₀_def + set I₁ : ℝ := ∫ t in Icc α (α + ℓ), ‖φ' t‖ with hI₁_def + have hI₁int : IntegrableOn (fun t => ‖φ' t‖) (Icc α (α + ℓ)) := + hφ'c.norm.continuousOn.integrableOn_Icc + have hI₀int : IntegrableOn (fun t => ‖φ t‖) (Icc α (α + ℓ)) := + hφc.norm.continuousOn.integrableOn_Icc + have hfin : volume (Icc α (α + ℓ)) ≠ ∞ := by simp [Real.volume_Icc] + have hpt : ∀ s ∈ Icc α (α + ℓ), ‖g x‖ ≤ ‖φ s‖ + I₁ := by + intro s hs + have h1 : ‖φ (x i) - φ s‖ ≤ I₁ := by + rw [hftc s] + calc ‖∫ t in s..x i, φ' t‖ ≤ ∫ t in Ι s (x i), ‖φ' t‖ := + intervalIntegral.norm_integral_le_integral_norm_uIoc + _ ≤ I₁ := setIntegral_mono_set hI₁int (ae_of_all _ fun _ => norm_nonneg _) + ((uIoc_subset_uIcc.trans (uIcc_subset_Icc hs hx)).eventuallyLE) + have h2 : φ (x i) = g x := by simp [hφ_def] + calc ‖g x‖ = ‖(φ (x i) - φ s) + φ s‖ := by rw [sub_add_cancel, h2] + _ ≤ ‖φ (x i) - φ s‖ + ‖φ s‖ := norm_add_le _ _ + _ ≤ I₁ + ‖φ s‖ := by gcongr + _ = ‖φ s‖ + I₁ := add_comm _ _ + have hvol : (volume : Measure ℝ).real (Icc α (α + ℓ)) = ℓ := by + simp [Measure.real, Real.volume_Icc, hℓ.le] + have hint := setIntegral_mono_on (μ := volume) (s := Icc α (α + ℓ)) (f := fun _ => ‖g x‖) + (g := fun s => ‖φ s‖ + I₁) (integrableOn_const hfin) (hI₀int.add (integrableOn_const hfin)) + measurableSet_Icc hpt + rw [setIntegral_const, integral_add hI₀int (integrableOn_const hfin), setIntegral_const, hvol, + smul_eq_mul, smul_eq_mul] at hint + + have hℓ0 : ℓ ≠ 0 := hℓ.ne' + have : ‖g x‖ = ℓ⁻¹ * (ℓ * ‖g x‖) := by field_simp + rw [this] + calc ℓ⁻¹ * (ℓ * ‖g x‖) ≤ ℓ⁻¹ * (I₀ + ℓ * I₁) := + mul_le_mul_of_nonneg_left hint (inv_nonneg.2 hℓ.le) + _ = ℓ⁻¹ * I₀ + I₁ := by field_simp + +theorem ofReal_norm_le_step + (ℓ : ℝ) (hℓ : 0 < ℓ) (α : ℝ) (g : (Fin n → ℝ) → ℂ) (hg : ContDiff ℝ 1 g) + (x : Fin n → ℝ) (i : Fin n) (hx : x i ∈ Icc α (α + ℓ)) : + ENNReal.ofReal ‖g x‖ ≤ ENNReal.ofReal (max 1 ℓ⁻¹) * + ((∫⁻ t in Icc α (α + ℓ), ENNReal.ofReal ‖g (update x i t)‖) + + ∫⁻ t in Icc α (α + ℓ), ENNReal.ofReal ‖fderiv ℝ g (update x i t) (Pi.single i 1)‖) := by + set I₀ : ℝ := ∫ t in Icc α (α + ℓ), ‖g (update x i t)‖ with hI₀_def + set I₁ : ℝ := ∫ t in Icc α (α + ℓ), ‖fderiv ℝ g (update x i t) (Pi.single i 1)‖ with hI₁_def + have h : ‖g x‖ ≤ ℓ⁻¹ * I₀ + I₁ := norm_le_inv_mul_integral_add_integral ℓ hℓ α g hg x i hx + have hI₀ : 0 ≤ I₀ := integral_nonneg fun _ => norm_nonneg _ + have hI₁ : 0 ≤ I₁ := integral_nonneg fun _ => norm_nonneg _ + have hM0 : (0 : ℝ) ≤ max 1 ℓ⁻¹ := zero_le_one.trans (le_max_left _ _) + have hM : ‖g x‖ ≤ max 1 ℓ⁻¹ * (I₀ + I₁) := by + calc ‖g x‖ ≤ ℓ⁻¹ * I₀ + I₁ := h + _ ≤ max 1 ℓ⁻¹ * I₀ + max 1 ℓ⁻¹ * I₁ := + add_le_add (mul_le_mul_of_nonneg_right (le_max_right _ _) hI₀) + (le_mul_of_one_le_left hI₁ (le_max_left _ _)) + _ = max 1 ℓ⁻¹ * (I₀ + I₁) := by ring + have hupd : Continuous fun t : ℝ => update x i t := continuous_const.update i continuous_id + have hc₀ : Continuous fun t : ℝ => ‖g (update x i t)‖ := (hg.continuous.comp hupd).norm + have hc₁ : Continuous fun t : ℝ => ‖fderiv ℝ g (update x i t) (Pi.single i 1)‖ := + (((hg.continuous_fderiv one_ne_zero).comp hupd).clm_apply continuous_const).norm + have e₀ : ENNReal.ofReal I₀ = ∫⁻ t in Icc α (α + ℓ), ENNReal.ofReal ‖g (update x i t)‖ := + ofReal_integral_eq_lintegral_ofReal hc₀.continuousOn.integrableOn_Icc + (ae_of_all _ fun _ => norm_nonneg _) + have e₁ : ENNReal.ofReal I₁ = + ∫⁻ t in Icc α (α + ℓ), ENNReal.ofReal ‖fderiv ℝ g (update x i t) (Pi.single i 1)‖ := + ofReal_integral_eq_lintegral_ofReal hc₁.continuousOn.integrableOn_Icc + (ae_of_all _ fun _ => norm_nonneg _) + rw [← e₀, ← e₁, ← ENNReal.ofReal_add hI₀ hI₁, ← ENNReal.ofReal_mul hM0] + exact ENNReal.ofReal_le_ofReal hM + +noncomputable def F (k : ℕ) (g : (Fin n → ℝ) → ℂ) : (Fin n → ℝ) → ℝ≥0∞ := + fun y => ENNReal.ofReal ‖iteratedFDeriv ℝ k g y‖ + +theorem measurable_F (k : ℕ) (g : (Fin n → ℝ) → ℂ) (hg : ContDiff ℝ k g) : Measurable (F k g) := + (hg.continuous_iteratedFDeriv'.norm).measurable.ennreal_ofReal + +noncomputable def boxMeasure (a : Fin n → ℝ) (ℓ : ℝ) : Fin n → Measure ℝ := + fun i => volume.restrict (Icc (a i) (a i + ℓ)) + +theorem boxMeasure_apply (a : Fin n → ℝ) (ℓ : ℝ) (i : Fin n) : + boxMeasure a ℓ i = volume.restrict (Icc (a i) (a i + ℓ)) := rfl + +scoped instance (a : Fin n → ℝ) (ℓ : ℝ) (i : Fin n) : SigmaFinite (boxMeasure a ℓ i) := by + rw [boxMeasure_apply]; infer_instance + +theorem F_clm_apply_le (m : ℕ) (g : (Fin n → ℝ) → ℂ) (hg : ContDiff ℝ (m + 1) g) + (v : Fin n → ℝ) (hv : ‖v‖ ≤ 1) (k : ℕ) (hk : k ≤ m) : + F k (fun y => fderiv ℝ g y v) ≤ F (k + 1) g := by + intro y + unfold F + apply ENNReal.ofReal_le_ofReal + have hfd : ContDiff ℝ m (fderiv ℝ g) := hg.fderiv_right le_rfl + have hcomp : (fun y => fderiv ℝ g y v) = ⇑(ContinuousLinearMap.apply ℝ ℂ v) ∘ fderiv ℝ g := by + funext y; simp + have hL : ‖ContinuousLinearMap.apply ℝ ℂ v‖ ≤ 1 := by + refine ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun A => ?_ + rw [ContinuousLinearMap.apply_apply, one_mul] + exact (A.le_opNorm v).trans (mul_le_of_le_one_right (norm_nonneg _) hv) + calc ‖iteratedFDeriv ℝ k (fun y => fderiv ℝ g y v) y‖ + = ‖iteratedFDeriv ℝ k (⇑(ContinuousLinearMap.apply ℝ ℂ v) ∘ fderiv ℝ g) y‖ := by + rw [hcomp] + _ ≤ ‖ContinuousLinearMap.apply ℝ ℂ v‖ * ‖iteratedFDeriv ℝ k (fderiv ℝ g) y‖ := + ContinuousLinearMap.norm_iteratedFDeriv_comp_left _ hfd.contDiffAt (by exact_mod_cast hk) + _ ≤ 1 * ‖iteratedFDeriv ℝ k (fderiv ℝ g) y‖ := + mul_le_mul_of_nonneg_right hL (norm_nonneg _) + _ = ‖iteratedFDeriv ℝ (k + 1) g y‖ := by rw [one_mul, norm_iteratedFDeriv_fderiv] + +theorem marginal_bound (ℓ : ℝ) (hℓ : 0 < ℓ) (a : Fin n → ℝ) (s : Finset (Fin n)) : + ∀ (g : (Fin n → ℝ) → ℂ), ContDiff ℝ s.card g → + ∀ x : Fin n → ℝ, (∀ j, x j ∈ Icc (a j) (a j + ℓ)) → + ENNReal.ofReal ‖g x‖ ≤ (2 * ENNReal.ofReal (max 1 ℓ⁻¹)) ^ s.card * + ∑ k ∈ Finset.range (s.card + 1), lmarginal (boxMeasure a ℓ) s (F k g) x := by + induction s using Finset.induction_on with + | empty => + intro g hg x hx + simp only [Finset.card_empty, pow_zero, one_mul, zero_add, Finset.range_one, + Finset.sum_singleton, lmarginal_empty] + unfold F + rw [norm_iteratedFDeriv_zero] + | insert i s hi ih => + intro g hg x hx + rw [Finset.card_insert_of_notMem hi] at hg ⊢ + set m : ℕ := s.card with hm_def + set M : ℝ≥0∞ := ENNReal.ofReal (max 1 ℓ⁻¹) with hM_def + set μ := boxMeasure a ℓ with hμ_def + have hMtop : M ≠ ∞ := ENNReal.ofReal_ne_top + have h2Mm : (2 * M) ^ m ≠ ∞ := ENNReal.pow_ne_top (ENNReal.mul_ne_top (by simp) hMtop) + + have hg1 : ContDiff ℝ 1 g := hg.of_le (by exact_mod_cast Nat.succ_le_succ (Nat.zero_le m)) + have hgm : ContDiff ℝ m g := hg.of_le (by exact_mod_cast Nat.le_succ m) + set h : (Fin n → ℝ) → ℂ := fun y => fderiv ℝ g y (Pi.single i 1) with hh_def + have hhm : ContDiff ℝ m h := + (hg.fderiv_right (by push_cast; exact le_rfl)).clm_apply contDiff_const + have hv : ‖(Pi.single i 1 : Fin n → ℝ)‖ ≤ 1 := by rw [Pi.norm_single, norm_one] + have hFh : ∀ k ≤ m, F k h ≤ F (k + 1) g := fun k hk => + F_clm_apply_le m g hg (Pi.single i 1) hv k hk + + have hbox : ∀ t ∈ Icc (a i) (a i + ℓ), ∀ j, update x i t j ∈ Icc (a j) (a j + ℓ) := by + intro t ht j + rcases eq_or_ne j i with rfl | hji + · simpa using ht + · rw [update_of_ne hji]; exact hx j + + have hstep : ENNReal.ofReal ‖g x‖ ≤ M * + ((∫⁻ t, ENNReal.ofReal ‖g (update x i t)‖ ∂(μ i)) + + ∫⁻ t, ENNReal.ofReal ‖h (update x i t)‖ ∂(μ i)) := + ofReal_norm_le_step ℓ hℓ (a i) g hg1 x i (hx i) + + have hmeasg : ∀ k ∈ Finset.range (m + 1), + Measurable fun t : ℝ => lmarginal μ s (F k g) (update x i t) := fun k hk => + ((measurable_F k g (hg.of_le (by + have := Finset.mem_range.1 hk; exact_mod_cast (by omega : k ≤ m + 1)))).lmarginal μ).comp + (measurable_update x) + have hmeasg' : ∀ k ∈ Finset.range (m + 1), + Measurable fun t : ℝ => lmarginal μ s (F (k + 1) g) (update x i t) := fun k hk => + ((measurable_F (k + 1) g (hg.of_le (by + have := Finset.mem_range.1 hk; exact_mod_cast (by omega : k + 1 ≤ m + 1)))).lmarginal μ).comp + (measurable_update x) + + have hA : (∫⁻ t, ENNReal.ofReal ‖g (update x i t)‖ ∂(μ i)) ≤ + (2 * M) ^ m * ∑ k ∈ Finset.range (m + 1), lmarginal μ (insert i s) (F k g) x := by + calc (∫⁻ t, ENNReal.ofReal ‖g (update x i t)‖ ∂(μ i)) + ≤ ∫⁻ t, (2 * M) ^ m * ∑ k ∈ Finset.range (m + 1), + lmarginal μ s (F k g) (update x i t) ∂(μ i) := by + rw [hμ_def, boxMeasure_apply] + exact setLIntegral_mono' measurableSet_Icc fun t ht => ih g hgm _ (hbox t ht) + _ = (2 * M) ^ m * ∑ k ∈ Finset.range (m + 1), + ∫⁻ t, lmarginal μ s (F k g) (update x i t) ∂(μ i) := by + rw [lintegral_const_mul' _ _ h2Mm, lintegral_finsetSum _ hmeasg] + _ = (2 * M) ^ m * ∑ k ∈ Finset.range (m + 1), lmarginal μ (insert i s) (F k g) x := by + congr 1 + refine Finset.sum_congr rfl fun k hk => ?_ + rw [lmarginal_insert _ (measurable_F k g (hg.of_le (by + have := Finset.mem_range.1 hk; exact_mod_cast (by omega : k ≤ m + 1)))) hi] + + have hB : (∫⁻ t, ENNReal.ofReal ‖h (update x i t)‖ ∂(μ i)) ≤ + (2 * M) ^ m * ∑ k ∈ Finset.range (m + 1), lmarginal μ (insert i s) (F (k + 1) g) x := by + calc (∫⁻ t, ENNReal.ofReal ‖h (update x i t)‖ ∂(μ i)) + ≤ ∫⁻ t, (2 * M) ^ m * ∑ k ∈ Finset.range (m + 1), + lmarginal μ s (F k h) (update x i t) ∂(μ i) := by + rw [hμ_def, boxMeasure_apply] + exact setLIntegral_mono' measurableSet_Icc fun t ht => ih h hhm _ (hbox t ht) + _ ≤ ∫⁻ t, (2 * M) ^ m * ∑ k ∈ Finset.range (m + 1), + lmarginal μ s (F (k + 1) g) (update x i t) ∂(μ i) := by + refine lintegral_mono fun t => ?_ + gcongr with k hk + exact lmarginal_mono (hFh k (by have := Finset.mem_range.1 hk; omega)) _ + _ = (2 * M) ^ m * ∑ k ∈ Finset.range (m + 1), + ∫⁻ t, lmarginal μ s (F (k + 1) g) (update x i t) ∂(μ i) := by + rw [lintegral_const_mul' _ _ h2Mm, lintegral_finsetSum _ hmeasg'] + _ = (2 * M) ^ m * ∑ k ∈ Finset.range (m + 1), + lmarginal μ (insert i s) (F (k + 1) g) x := by + congr 1 + refine Finset.sum_congr rfl fun k hk => ?_ + rw [lmarginal_insert _ (measurable_F (k + 1) g (hg.of_le (by + have := Finset.mem_range.1 hk; exact_mod_cast (by omega : k + 1 ≤ m + 1)))) hi] + + set T : ℝ≥0∞ := ∑ k ∈ Finset.range (m + 1 + 1), lmarginal μ (insert i s) (F k g) x with hT_def + have hsub₁ : ∑ k ∈ Finset.range (m + 1), lmarginal μ (insert i s) (F k g) x ≤ T := + Finset.sum_le_sum_of_subset (Finset.range_subset_range.2 (Nat.le_succ _)) + have hsub₂ : ∑ k ∈ Finset.range (m + 1), lmarginal μ (insert i s) (F (k + 1) g) x ≤ T := by + have hT : T = ∑ k ∈ Finset.range (m + 1), lmarginal μ (insert i s) (F (k + 1) g) x + + lmarginal μ (insert i s) (F 0 g) x := Finset.sum_range_succ' _ _ + rw [hT] + exact le_self_add + calc ENNReal.ofReal ‖g x‖ + ≤ M * ((2 * M) ^ m * T + (2 * M) ^ m * T) := by + refine hstep.trans ?_ + gcongr + · exact hA.trans (by gcongr) + · exact hB.trans (by gcongr) + _ = (2 * M) ^ (m + 1) * T := by ring + +def box (a : Fin n → ℝ) (ℓ : ℝ) : Set (Fin n → ℝ) := Set.pi univ fun i => Icc (a i) (a i + ℓ) + +theorem isCompact_box (a : Fin n → ℝ) (ℓ : ℝ) : IsCompact (box a ℓ) := + isCompact_univ_pi fun _ => isCompact_Icc + +theorem volume_box (a : Fin n → ℝ) (ℓ : ℝ) : + volume (box a ℓ) = ENNReal.ofReal ℓ ^ n := by + rw [box, volume_pi_pi] + simp [Real.volume_Icc, Finset.prod_const] + +theorem volume_real_box (a : Fin n → ℝ) (ℓ : ℝ) (hℓ : 0 < ℓ) : + (volume : Measure (Fin n → ℝ)).real (box a ℓ) = ℓ ^ n := by + simp [Measure.real, volume_box a ℓ, ENNReal.toReal_pow, hℓ.le] + +theorem pi_boxMeasure (a : Fin n → ℝ) (ℓ : ℝ) : + Measure.pi (boxMeasure a ℓ) = (volume : Measure (Fin n → ℝ)).restrict (box a ℓ) := by + rw [box, volume_pi, Measure.restrict_pi_pi] + rfl + +theorem setIntegral_le_sqrt_mul_sqrt (a : Fin n → ℝ) (ℓ : ℝ) (hℓ : 0 < ℓ) + (G : (Fin n → ℝ) → ℝ) (hG : Continuous G) (hG0 : ∀ y, 0 ≤ G y) : + ∫ y in box a ℓ, G y ≤ Real.sqrt (ℓ ^ n) * Real.sqrt (∫ y in box a ℓ, G y ^ 2) := by + set Q := box a ℓ with hQ_def + have hQc : IsCompact Q := isCompact_box a ℓ + have hQfin : volume Q ≠ ∞ := hQc.measure_ne_top + set mQ : ℝ := ℓ ^ n with hmQ_def + have hmQ : 0 < mQ := pow_pos hℓ n + have hreal : (volume : Measure (Fin n → ℝ)).real Q = mQ := volume_real_box a ℓ hℓ + set I : ℝ := ∫ y in Q, G y with hI_def + set J : ℝ := ∫ y in Q, G y ^ 2 with hJ_def + have hI0 : 0 ≤ I := integral_nonneg hG0 + have hGint : IntegrableOn G Q := hG.continuousOn.integrableOn_compact hQc + have hG2int : IntegrableOn (fun y => G y ^ 2) Q := (hG.pow 2).continuousOn.integrableOn_compact hQc + + set lam : ℝ := I / mQ with hlam_def + have hpt : ∀ y ∈ Q, 2 * lam * G y ≤ G y ^ 2 + lam ^ 2 := fun y _ => by + have := two_mul_le_add_sq (G y) lam + linarith + have hmono : ∫ y in Q, 2 * lam * G y ≤ ∫ y in Q, (G y ^ 2 + lam ^ 2) := + setIntegral_mono_on (μ := volume) (s := Q) (hGint.const_mul (2 * lam)) + (hG2int.add (integrableOn_const hQfin)) hQc.measurableSet hpt + have hL : ∫ y in Q, 2 * lam * G y = 2 * lam * I := integral_const_mul _ _ + have hR : ∫ y in Q, (G y ^ 2 + lam ^ 2) = J + mQ * lam ^ 2 := by + rw [integral_add hG2int (integrableOn_const hQfin), setIntegral_const, hreal, smul_eq_mul] + rw [hL, hR] at hmono + + have hsq : I ^ 2 ≤ mQ * J := by + have hmQ0 : mQ ≠ 0 := hmQ.ne' + have h1 : 2 * lam * I = 2 * I ^ 2 / mQ := by rw [hlam_def]; field_simp + have h2 : mQ * lam ^ 2 = I ^ 2 / mQ := by rw [hlam_def]; field_simp + rw [h1, h2] at hmono + have h3 : I ^ 2 / mQ ≤ J := by + have e : 2 * I ^ 2 / mQ = 2 * (I ^ 2 / mQ) := by ring + rw [e] at hmono + linarith + rwa [div_le_iff₀' hmQ] at h3 + calc I = |I| := (abs_of_nonneg hI0).symm + _ ≤ Real.sqrt (mQ * J) := Real.abs_le_sqrt hsq + _ = Real.sqrt mQ * Real.sqrt J := Real.sqrt_mul hmQ.le J + +theorem norm_le_mul_sum_setIntegral (ℓ : ℝ) (hℓ : 0 < ℓ) (a : Fin n → ℝ) + (f : (Fin n → ℝ) → ℂ) (hf : ContDiff ℝ n f) + (x : Fin n → ℝ) (hx : ∀ j, x j ∈ Icc (a j) (a j + ℓ)) : + ‖f x‖ ≤ (2 * max 1 ℓ⁻¹) ^ n * + ∑ k ∈ Finset.range (n + 1), ∫ y in box a ℓ, ‖iteratedFDeriv ℝ k f y‖ := by + have hQc : IsCompact (box a ℓ) := isCompact_box a ℓ + have hcard : (Finset.univ : Finset (Fin n)).card = n := Finset.card_fin n + have hmb := marginal_bound ℓ hℓ a Finset.univ f (by rw [hcard]; exact hf) x hx + rw [hcard] at hmb + set I : ℕ → ℝ := fun k => ∫ y in box a ℓ, ‖iteratedFDeriv ℝ k f y‖ with hI_def + have hI0 : ∀ k, 0 ≤ I k := fun k => integral_nonneg fun _ => norm_nonneg _ + have hM0 : (0 : ℝ) ≤ max 1 ℓ⁻¹ := zero_le_one.trans (le_max_left _ _) + + have hterm : ∀ k ∈ Finset.range (n + 1), + lmarginal (boxMeasure a ℓ) Finset.univ (F k f) x = ENNReal.ofReal (I k) := by + intro k hk + have hk' : k ≤ n := by have := Finset.mem_range.1 hk; omega + have hcont : Continuous fun y => ‖iteratedFDeriv ℝ k f y‖ := + (hf.continuous_iteratedFDeriv (by exact_mod_cast hk')).norm + rw [lmarginal_univ, pi_boxMeasure] + change (∫⁻ y in box a ℓ, ENNReal.ofReal ‖iteratedFDeriv ℝ k f y‖) = ENNReal.ofReal (I k) + rw [hI_def] + exact (ofReal_integral_eq_lintegral_ofReal (hcont.continuousOn.integrableOn_compact hQc) + (ae_of_all _ fun _ => norm_nonneg _)).symm + have hkey : ENNReal.ofReal ‖f x‖ ≤ + ENNReal.ofReal ((2 * max 1 ℓ⁻¹) ^ n * ∑ k ∈ Finset.range (n + 1), I k) := by + refine hmb.trans (le_of_eq ?_) + rw [Finset.sum_congr rfl hterm, ← ENNReal.ofReal_sum_of_nonneg fun k _ => hI0 k, + ENNReal.ofReal_mul (pow_nonneg (mul_nonneg zero_le_two hM0) n), + ENNReal.ofReal_pow (mul_nonneg zero_le_two hM0), ENNReal.ofReal_mul zero_le_two, + ENNReal.ofReal_ofNat] + exact (ENNReal.ofReal_le_ofReal_iff (mul_nonneg (pow_nonneg (mul_nonneg zero_le_two hM0) n) + (Finset.sum_nonneg fun k _ => hI0 k))).1 hkey + +end SobolevBox + +open MeasureTheory SobolevBox in +theorem Sobolev.exists_forall_norm_le_mul_sum_sqrt_integral_norm_iteratedFDeriv_sq_of_contDiff_box + (n : ℕ) (ℓ : ℝ) (hℓ : 0 < ℓ) : + ∃ c : ℝ, 0 ≤ c ∧ ∀ (a : Fin n → ℝ) (f : (Fin n → ℝ) → ℂ), ContDiff ℝ n f → + ∀ x : Fin n → ℝ, (∀ i, x i ∈ Set.Icc (a i) (a i + ℓ)) → + ‖f x‖ ≤ c * ∑ k ∈ Finset.range (n + 1), + Real.sqrt (∫ y in Set.pi Set.univ (fun i => Set.Icc (a i) (a i + ℓ)), ‖iteratedFDeriv ℝ k f y‖ ^ 2) := by + have hM0 : (0 : ℝ) ≤ max 1 ℓ⁻¹ := zero_le_one.trans (le_max_left _ _) + set C₁ : ℝ := (2 * max 1 ℓ⁻¹) ^ n with hC₁_def + have hC₁ : 0 ≤ C₁ := pow_nonneg (mul_nonneg zero_le_two hM0) n + refine ⟨C₁ * Real.sqrt (ℓ ^ n), mul_nonneg hC₁ (Real.sqrt_nonneg _), ?_⟩ + intro a f hf x hx + have h1 := norm_le_mul_sum_setIntegral ℓ hℓ a f hf x hx + have h2 : ∀ k ∈ Finset.range (n + 1), + ∫ y in box a ℓ, ‖iteratedFDeriv ℝ k f y‖ ≤ + Real.sqrt (ℓ ^ n) * Real.sqrt (∫ y in box a ℓ, ‖iteratedFDeriv ℝ k f y‖ ^ 2) := by + intro k hk + have hk' : k ≤ n := by have := Finset.mem_range.1 hk; omega + exact setIntegral_le_sqrt_mul_sqrt a ℓ hℓ (fun y => ‖iteratedFDeriv ℝ k f y‖) + (hf.continuous_iteratedFDeriv (by exact_mod_cast hk')).norm fun _ => norm_nonneg _ + calc ‖f x‖ ≤ C₁ * ∑ k ∈ Finset.range (n + 1), ∫ y in box a ℓ, ‖iteratedFDeriv ℝ k f y‖ := h1 + _ ≤ C₁ * ∑ k ∈ Finset.range (n + 1), + Real.sqrt (ℓ ^ n) * Real.sqrt (∫ y in box a ℓ, ‖iteratedFDeriv ℝ k f y‖ ^ 2) := by + gcongr with k hk + exact h2 k hk + _ = C₁ * Real.sqrt (ℓ ^ n) * ∑ k ∈ Finset.range (n + 1), + Real.sqrt (∫ y in Set.pi Set.univ (fun i => Set.Icc (a i) (a i + ℓ)), + ‖iteratedFDeriv ℝ k f y‖ ^ 2) := by + rw [← Finset.mul_sum, mul_assoc] + rfl + diff --git a/GIFT/Foundations/G2CrossProduct.lean b/GIFT/Foundations/G2CrossProduct.lean index 2a9e39d7..7b3e8562 100644 --- a/GIFT/Foundations/G2CrossProduct.lean +++ b/GIFT/Foundations/G2CrossProduct.lean @@ -365,7 +365,7 @@ theorem R7_inner_eq_sum (u v : R7) : @inner ℝ R7 _ u v = ∑ i : Fin 7, u i * rw [PiLp.inner_apply] congr 1 funext i - simp only [inner, conj_trivial, RCLike.re_to_real, mul_comm] + simp only [inner, star_trivial, RCLike.re_to_real, mul_comm] /-- Lagrange identity for 7D cross product (FULLY PROVEN) |u × v|² = |u|²|v|² - ⟨u,v⟩² diff --git a/GIFT/Geometry/HodgeStarR7.lean b/GIFT/Geometry/HodgeStarR7.lean index da80ccd3..e68455dc 100644 --- a/GIFT/Geometry/HodgeStarR7.lean +++ b/GIFT/Geometry/HodgeStarR7.lean @@ -67,17 +67,19 @@ def star4 (η : DiffForm 4) : DiffForm 3 := /-- star3 is linear -/ theorem star3_linear (a : ℝ) (ω η : DiffForm 3) : star3 (a • ω + η) = a • star3 ω + star3 η := by - unfold star3 constDiffForm ext p i - simp only [smul_coeffs, add_coeffs, hodgeStar3to4] + show sign3 (complement4to3 i) * (a * ω.coeffs 0 (complement4to3 i) + η.coeffs 0 (complement4to3 i)) + = a * (sign3 (complement4to3 i) * ω.coeffs 0 (complement4to3 i)) + + sign3 (complement4to3 i) * η.coeffs 0 (complement4to3 i) ring /-- star4 is linear -/ theorem star4_linear (a : ℝ) (ω η : DiffForm 4) : star4 (a • ω + η) = a • star4 ω + star4 η := by - unfold star4 constDiffForm ext p i - simp only [smul_coeffs, add_coeffs, hodgeStar4to3] + show sign4 (complement3to4 i) * (a * ω.coeffs 0 (complement3to4 i) + η.coeffs 0 (complement3to4 i)) + = a * (sign4 (complement3to4 i) * ω.coeffs 0 (complement3to4 i)) + + sign4 (complement3to4 i) * η.coeffs 0 (complement3to4 i) ring /-- ⋆⋆ = id on constant 3-forms (coefficient level) -/ diff --git a/LICENSES/Apache-2.0.txt b/LICENSES/Apache-2.0.txt new file mode 100644 index 00000000..6f101c9f --- /dev/null +++ b/LICENSES/Apache-2.0.txt @@ -0,0 +1,202 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright 2026 Anthropic, PBC + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/NOTICE b/NOTICE new file mode 100644 index 00000000..dddf5d13 --- /dev/null +++ b/NOTICE @@ -0,0 +1,14 @@ +The following files are adapted from anthropics/fermats-last-theorem: + + GIFT/Foundations/Analysis/Sobolev/Box.lean + GIFT/Foundations/Analysis/SmoothFamily.lean + +Copyright 2026 Anthropic, PBC. Licensed under Apache License 2.0. +Upstream commit: aa2d8b34692b16c70f699536de0d8e75b9a3e9ef +Upstream paths: + P2M/Sol/S_Sobolev_exists_forall_norm_le_mul_sum_sqrt_integral_norm_iteratedFDeriv_sq_of_contDiff_box.lean + P2M/Sol/S_ContDiff_exists_forall_norm_iteratedDeriv_slice_le_of_isCompact.lean + +Changes: removed pipeline utility imports and namespaces, restored mathematical +names, and adapted to the pinned Mathlib version. See LICENSES/Apache-2.0.txt. +Mathlib and Lean are obtained as build dependencies under their own licenses. diff --git a/README.md b/README.md index 66f9c578..cdbbed77 100644 --- a/README.md +++ b/README.md @@ -1,102 +1,79 @@ # K₇-Lean -> ### This repository has moved -> -> **`gift-framework/core` → [`Arithmon/K7-Lean`](https://github.com/Arithmon/K7-Lean)** -> -> The K₇ framework's certified Lean 4 core has joined the [Arithmon](https://github.com/Arithmon) -> organisation alongside [K7](https://github.com/Arithmon/K7) (the framework, formerly -> `gift-framework/GIFT`), Atlas, Program, Lean and Sieve. Not to be confused with -> [Arithmon/Lean](https://github.com/Arithmon/Lean), the Sieve/Q5 methodology layer: -> this repository is the framework's formal core, formerly known as "GIFT Core". -> -> **Nothing you cite will break.** The published papers (immutable PDFs on Zenodo) cite -> `github.com/gift-framework/core` dozens of times. GitHub redirects the old URLs (web -> *and* `git clone` / `fetch` / `push`), and those redirects are load-bearing -> infrastructure, so the old path will never be reused. Release tags and the -> pre-registration pointer (`v3.4.29`, `667c8b9`) are unaffected. - ---- - [![Formal Verification](https://github.com/Arithmon/K7-Lean/actions/workflows/verify.yml/badge.svg)](https://github.com/Arithmon/K7-Lean/actions/workflows/verify.yml) -[![PyPI](https://img.shields.io/pypi/v/giftpy)](https://pypi.org/project/giftpy/) - -Part of the **[Arithmon program](https://github.com/arithmon)** -- the hypothesis that the constants of nature are counts. - -Formally verified mathematical relations from the K₇ framework. 460+ certified relations, **15 axioms** (4 logical on the main prediction chain + 11 interval-arithmetic certificates for the K3 block of g*), all theorems proven in **Lean 4** (8394 build jobs). - -## Structure -``` -GIFT/ # Lean 4 formalization (root library) -├── Core.lean # Constants (dim_E8, b2, b3, H*, ...) -├── Certificate/ # Modular certificate system -│ ├── Core.lean # Master: Foundations ∧ Predictions ∧ Spectral -│ ├── Foundations.lean # E₈, G₂, octonions, K₇, Joyce, NK cert (39 conjuncts) -│ ├── Predictions.lean # 33+ relations, ~50 observables (56 conjuncts) -│ └── Spectral.lean # Mass gap, TCS, computed spectrum, Weyl law (45 conjuncts) -├── Foundations/ # Mathematical foundations (23 files) -│ ├── RootSystems.lean # E₈ roots in ℝ⁸ (240 vectors) -│ ├── E8Lattice.lean # E₈ lattice, Weyl reflection -│ ├── G2CrossProduct.lean # 7D cross product, Fano plane -│ ├── ExplicitG2Metric.lean # 169-param Chebyshev-Cholesky -│ ├── NewtonKantorovich.lean # NK cert: h < 0.5, decomposed -│ ├── NumericalBounds.lean # Taylor series bounds (axiom-free) -│ └── Analysis/ # G₂ forms, Hodge theory, Sobolev -├── Geometry/ # Axiom-free DG infrastructure -│ ├── HodgeStarR7.lean # ⋆, ψ=⋆φ PROVEN, TorsionFree -│ └── HodgeStarCompute.lean # Explicit Hodge star (Levi-Civita) -├── Spectral/ # Spectral gap theory (17 files) -│ ├── PhysicalSpectralGap.lean # dim(G₂)−h = 13 algebraic (zero axioms) -│ ├── ComputedSpectrum.lean # Q22 sig, SD/ASD gap, B-test -│ └── CheegerInequality.lean # Cheeger-Buser bounds -├── Algebraic/ # Octonion/G₂ algebraic foundations -│ └── G2ThreeForm.lean # φ₀ 3-form, G₂=Stab(φ₀), g₂=ker(L_φ₀), dim=14 -├── Relations/ # Physical predictions (22 files) -├── Observables/ # PMNS, CKM, quark masses, cosmology -├── Hierarchy/ # Dimensional gap, absolute masses - -GIFTTest/ # Lean test files - -blueprint/ # Leanblueprint dependency graph - -contrib/ # Non-Lean assets -├── python/ # Python package (giftpy on PyPI) -│ └── gift_core/ # Certified constants export -├── homepage/ # GitHub Pages / Jekyll site -└── docs/ # Extended documentation -``` +Lean 4 formalizations of algebraic identities, finite-dimensional models, numerical +inequalities and conditional geometric statements associated with the +[Arithmon K₇ framework](https://github.com/Arithmon/K7). -## Quick Start +The Lean statements specify the scope of each result. In particular, arithmetic +conditions on Sobolev indices are not embedding theorems, and the constant +three-form model on ℝ⁷ is not a construction of a compact manifold with G₂ holonomy. +Physical interpretations of the numerical relations are outside the formal proofs. -```bash -pip install giftpy -``` +## Build and verify -```python -from gift_core import * +Install [elan](https://github.com/leanprover/elan), then run: -print(SIN2_THETA_W) # Fraction(3, 13) -print(GAMMA_GIFT) # Fraction(511, 884) -print(TAU) # Fraction(3472, 891) -``` - -## Building Proofs - -```bash +```sh +git clone https://github.com/Arithmon/K7-Lean.git +cd K7-Lean +lake exe cache get lake build +python3 scripts/proof_inventory.py --check +lake build Verification ``` -## Documentation - -For extended observables, publications, and detailed analysis: - -**[Arithmon/K7](https://github.com/Arithmon/K7)** - ---- - -> **K₇ (formerly GIFT) is the founding framework of the [Arithmon program](https://github.com/arithmon).** - -[Changelog](contrib/CHANGELOG.md) | [MIT License](LICENSE) +Lean, Mathlib and doc-gen4 target **4.33.1**. Exact dependency revisions are recorded +in `lake-manifest.json`. Routine builds use that lockfile; `lake update` is reserved +for deliberate dependency updates. Migration validation is recorded in +[docs/modernization.md](docs/modernization.md). + +## Reading the library + +| Directory | Contents | +| --- | --- | +| `GIFT/Algebraic/` | Octonions, explicit G₂ tensors and finite matrix identities | +| `GIFT/Foundations/` | Root systems, numerical inequalities and geometric models | +| `GIFT/Foundations/Analysis/` | Analysis lemmas and arithmetic interfaces | +| `GIFT/Geometry/` | Coordinate calculations with differential forms | +| `GIFT/Spectral/` | Spectral models and statements with explicit project assumptions | +| `GIFT/Relations/`, `GIFT/Observables/` | Relations among the framework's declared constants | +| `GIFT/Certificate/` | Conjunctions of exported statements | +| `Verification/` | Transitive axiom audit and checks for the analysis lemmas | +| `blueprint/` | Mathematical exposition and declaration references | +| `contrib/` | Python package, website and historical documentation | + +Start with [the proof guide](docs/proof-guide.md) and consult the exact theorem types +before interpreting a module title. The `GIFT` namespace and historical aliases are +retained so existing imports and published references continue to resolve. + +## Proof dependencies + +The current library declares **15 axioms**: five unspecified real quantities, six +assumptions in the numerical-certificate module, and four assumptions in the spectral +modules. This count is a source inventory, not a measure of mathematical completeness. +Bundling assumptions into a structure does not discharge them. + +The library also uses `native_decide` for finite computations. These proofs have a +different trust boundary from proofs reduced entirely by the kernel. The generated +[source inventory](docs/proof-inventory.json) lists occurrences. The Lean audit +reports transitive dependencies of exported certificates and fails on `sorryAx` or +unlisted axioms; stricter checks require only Lean's standard axioms for the new +analysis lemmas and elementary index conditions. + +See [the dependency policy](docs/proof-guide.md#dependency-policy) for the distinction +between kernel axioms, project assumptions, and native computation. + +## Related artifacts and attribution + +- [K₇ framework](https://github.com/Arithmon/K7): accompanying mathematical exposition. +- [Python package](contrib/python/README.md): optional export of numerical constants. +- [Contribution guide](CONTRIBUTING.md) and [changelog](contrib/CHANGELOG.md). +- [MIT license](LICENSE); adapted analysis proofs retain their + [Apache-2.0 license](LICENSES/Apache-2.0.txt) and [attribution](NOTICE). + +Former repository: `gift-framework/core`. Existing release tags and the +pre-registration reference `v3.4.29` / `667c8b9` are retained. *K₇-Lean v3.4.29* diff --git a/Verification/AllImports.lean b/Verification/AllImports.lean new file mode 100644 index 00000000..3e7c300a --- /dev/null +++ b/Verification/AllImports.lean @@ -0,0 +1,150 @@ +-- Generated by scripts/update_verification_imports.py. +import GIFT.Algebraic.BettiNumbers +import GIFT.Algebraic.CayleyDickson +import GIFT.Algebraic.G2 +import GIFT.Algebraic.G2Bform +import GIFT.Algebraic.G2Rank +import GIFT.Algebraic.G2ThreeForm +import GIFT.Algebraic.GIFTConstants +import GIFT.Algebraic.GeometricSaturation +import GIFT.Algebraic.Octonions +import GIFT.Algebraic.Quaternions +import GIFT.Algebraic.SO16Decomposition +import GIFT.Algebraic +import GIFT.Certificate.Core +import GIFT.Certificate.Foundations +import GIFT.Certificate.Predictions +import GIFT.Certificate.Spectral +import GIFT.Certificate +import GIFT.Core +import GIFT.DifferentialForms +import GIFT.Foundations.AmbroseSinger +import GIFT.Foundations.Analysis.AnalyticalFoundations +import GIFT.Foundations.Analysis.E8Lattice +import GIFT.Foundations.Analysis.Elliptic.Basic +import GIFT.Foundations.Analysis.ExteriorAlgebra +import GIFT.Foundations.Analysis.G2Forms.All +import GIFT.Foundations.Analysis.G2Forms.DifferentialForms +import GIFT.Foundations.Analysis.G2Forms.G2FormsBridge +import GIFT.Foundations.Analysis.G2Forms.G2Structure +import GIFT.Foundations.Analysis.G2Forms.HodgeStar +import GIFT.Foundations.Analysis.G2TensorForm +import GIFT.Foundations.Analysis.HarmonicForms +import GIFT.Foundations.Analysis.HodgeTheory +import GIFT.Foundations.Analysis.IFT.Basic +import GIFT.Foundations.Analysis.InnerProductSpace +import GIFT.Foundations.Analysis.JoyceAnalytic +import GIFT.Foundations.Analysis.K7Orthonormality +import GIFT.Foundations.Analysis.SmoothFamily +import GIFT.Foundations.Analysis.Sobolev.Basic +import GIFT.Foundations.Analysis.Sobolev.Box +import GIFT.Foundations.Analysis.WedgeProduct +import GIFT.Foundations.Analysis +import GIFT.Foundations.AnalyticalMetric +import GIFT.Foundations.CollarResummationCertificate +import GIFT.Foundations.ConformalRigidity +import GIFT.Foundations.ContractionMajorant +import GIFT.Foundations.DonaldsonCoassociativeFibration +import GIFT.Foundations.DonaldsonGlobalBaseAudit +import GIFT.Foundations.E8Lattice +import GIFT.Foundations.E8Mathlib +import GIFT.Foundations.ExplicitG2Metric +import GIFT.Foundations.G2CrossProduct +import GIFT.Foundations.G2DonaldsonLinkCohomology +import GIFT.Foundations.G2Holonomy +import GIFT.Foundations.G2IrrepLatticeCertificate +import GIFT.Foundations.G2TCSLatticeCertificate +import GIFT.Foundations.GoldenRatio +import GIFT.Foundations.GoldenRatioPowers +import GIFT.Foundations.GraphTheory +import GIFT.Foundations.IntervalCertificates +import GIFT.Foundations.K3AutomorphismPackage +import GIFT.Foundations.K3ClosedFormBoxEnclosures +import GIFT.Foundations.K3ClosedFormWitness +import GIFT.Foundations.K3HarmonicCorrection +import GIFT.Foundations.K3IsotypeLefschetzCertificate +import GIFT.Foundations.K3KrawczykContainment +import GIFT.Foundations.K3NewtonKantorovich +import GIFT.Foundations.K3VandermondeSmoothness +import GIFT.Foundations.K7NuBar +import GIFT.Foundations.MetricEigenvalues +import GIFT.Foundations.MetricGapClosure +import GIFT.Foundations.NewtonKantorovich +import GIFT.Foundations.NumericalBounds +import GIFT.Foundations.OctonionBridge +import GIFT.Foundations.PiBounds +import GIFT.Foundations.PoincareDuality +import GIFT.Foundations.RationalConstants +import GIFT.Foundations.RootSystems +import GIFT.Foundations.SpectralScaling +import GIFT.Foundations.TCSConstruction +import GIFT.Foundations.TCSPiecewiseMetric +import GIFT.Foundations +import GIFT.Geometry.DifferentialFormsR7 +import GIFT.Geometry.Exterior +import GIFT.Geometry.HodgeStarCompute +import GIFT.Geometry.HodgeStarR7 +import GIFT.Geometry +import GIFT.Hierarchy.AbsoluteMasses +import GIFT.Hierarchy.AssociativeVolumes +import GIFT.Hierarchy.DimensionalGap +import GIFT.Hierarchy.E6Cascade +import GIFT.Hierarchy.GaugeBundleData +import GIFT.Hierarchy.TCSGaugeBreaking +import GIFT.Hierarchy.VacuumStructure +import GIFT.Hierarchy +import GIFT.ImplicitFunction +import GIFT.IntervalArithmetic +import GIFT.Joyce +import GIFT.Observables.BosonMasses +import GIFT.Observables.CKM +import GIFT.Observables.Cosmology +import GIFT.Observables.PMNS +import GIFT.Observables.QuarkMasses +import GIFT.Observables.WeakMixingAngle +import GIFT.Observables +import GIFT.Predictions.CP.DeltaCPNuBarConjecture +import GIFT.Relations.BosonTriangle +import GIFT.Relations.CompactificationCorrection +import GIFT.Relations.Cosmology +import GIFT.Relations.ExceptionalChain +import GIFT.Relations.ExceptionalGroups +import GIFT.Relations.FanoSelectionPrinciple +import GIFT.Relations.G2MetricProperties +import GIFT.Relations.GaugeSector +import GIFT.Relations.GoldenRatio +import GIFT.Relations.IrrationalSector +import GIFT.Relations.KoideAssembly +import GIFT.Relations.LandauerDarkEnergy +import GIFT.Relations.LeptonSector +import GIFT.Relations.NeutrinoSector +import GIFT.Relations.OverDetermination +import GIFT.Relations.QuarkSector +import GIFT.Relations.SO16Relations +import GIFT.Relations.SectorClassification +import GIFT.Relations.Structural +import GIFT.Relations.TauBounds +import GIFT.Relations.V33Additions +import GIFT.Relations +import GIFT.Sobolev +import GIFT.Spectral.AnalyticalMassGap +import GIFT.Spectral.CheegerInequality +import GIFT.Spectral.ComputedSpectrum +import GIFT.Spectral.ComputedWeylLaw +import GIFT.Spectral.ComputedYukawa +import GIFT.Spectral.G2Manifold +import GIFT.Spectral.KKSpectralBridge +import GIFT.Spectral.LiteratureAxioms +import GIFT.Spectral.MassGapRatio +import GIFT.Spectral.NeckGeometry +import GIFT.Spectral.OctonionMassGap +import GIFT.Spectral.PhysicalSpectralGap +import GIFT.Spectral.RefinedSpectralBounds +import GIFT.Spectral.SelectionPrinciple +import GIFT.Spectral.SpectralDemocracy +import GIFT.Spectral.SpectralInvariants +import GIFT.Spectral.SpectralTheory +import GIFT.Spectral.TCSBounds +import GIFT.Spectral.UniversalLaw +import GIFT.Spectral.YangMills +import GIFT.Spectral diff --git a/Verification/AnalysisChecks.lean b/Verification/AnalysisChecks.lean new file mode 100644 index 00000000..be92e0e5 --- /dev/null +++ b/Verification/AnalysisChecks.lean @@ -0,0 +1,20 @@ +import GIFT.Foundations.Analysis.Sobolev.Box +import GIFT.Foundations.Analysis.SmoothFamily +import GIFT.Foundations.Analysis.Sobolev.Basic +import GIFT.Foundations.Analysis.Elliptic.Basic +import GIFT.Foundations.Analysis.IFT.Basic +import GIFT.Algebraic.GIFTConstants +import Verification.Policy + +open Verification in +run_cmd do + for decl in #[ + `Sobolev.exists_forall_norm_le_mul_sum_sqrt_integral_norm_iteratedFDeriv_sq_of_contDiff_box, + `ContDiff.exists_forall_norm_iteratedDeriv_slice_le_of_isCompact, + `GIFT.Foundations.Analysis.Sobolev.sobolev_conditions_certified, + `GIFT.Foundations.Analysis.Elliptic.elliptic_certified, + `GIFT.Foundations.Analysis.IFT.ift_certified, + `GIFT.Algebraic.BettiNumbers.b2_eq, + `GIFT.Algebraic.G2.omega3_total, + `GIFT.Algebraic.GIFTConstants.kappa_T_inv_prime] do + checkAxioms decl standardAxioms diff --git a/Verification/AxiomAudit.lean b/Verification/AxiomAudit.lean new file mode 100644 index 00000000..6ea0a09d --- /dev/null +++ b/Verification/AxiomAudit.lean @@ -0,0 +1,65 @@ +import Verification.AllImports +import Verification.AnalysisChecks +import Verification.Policy + +open Lean Elab Command Verification + +/-- Existing assumptions, individually named rather than counted as bundles. -/ +def projectAxioms : Array Name := #[ + `GIFT.Spectral.CheegerInequality.cheeger_inequality, + `GIFT.Spectral.LiteratureAxioms.literature_package, + `GIFT.Spectral.TCSBounds.spectral_upper_bound, + `GIFT.Spectral.TCSBounds.neck_dominates, + `GIFT.Foundations.IntervalCertificates.det_g_at_half, + `GIFT.Foundations.IntervalCertificates.K3_eigenvalue_0, + `GIFT.Foundations.IntervalCertificates.K3_eigenvalue_1, + `GIFT.Foundations.IntervalCertificates.K3_eigenvalue_2, + `GIFT.Foundations.IntervalCertificates.K3_eigenvalue_3, + `GIFT.Foundations.IntervalCertificates.det_g_at_half_bracketed, + `GIFT.Foundations.IntervalCertificates.K3_eigenvalue_0_bracketed, + `GIFT.Foundations.IntervalCertificates.K3_eigenvalue_1_bracketed, + `GIFT.Foundations.IntervalCertificates.K3_eigenvalue_2_bracketed, + `GIFT.Foundations.IntervalCertificates.K3_eigenvalue_3_bracketed, + `GIFT.Foundations.IntervalCertificates.PSLQ_null_in_TCS_basis] + +-- Legacy native computations are permitted here, but not in AnalysisChecks. +def nativeAxioms : Array Name := #[`Lean.ofReduceBool, `Lean.ofReduceNat, `Lean.trustCompiler] + +/-- Lean 4.33 names native-evaluation axioms at the declaration that generated them. -/ +def isNativeEvaluationAxiom (name : Name) : Bool := + nativeAxioms.contains name || + (name.toString.splitOn "._native.native_decide.ax").length > 1 || + (name.toString.splitOn "._native.bv_decide.ax").length > 1 + +run_cmd do + let allowed := standardAxioms ++ projectAxioms + let env ← getEnv + let native := env.constants.toList.filterMap fun (name, info) => + match info with + | .axiomInfo _ => if isNativeEvaluationAxiom name then some name else none + | _ => none + let allowed := allowed ++ native.toArray + for decl in #[ + `GIFT.Certificate.Foundations.certified, + `GIFT.Certificate.Predictions.certified, + `GIFT.Certificate.Spectral.certified, + `GIFT.Certificate.gift_master_certificate, + `GIFT.Relations.KoideAssembly.koideQ_gift_lt_two_thirds] do + checkAxioms decl allowed + let mut count : Nat := 0 + let mut nativeCount : Nat := 0 + for (name, info) in env.constants.toList do + let inLibrary := name.toString.startsWith "GIFT." || name.toString.startsWith "_private.GIFT." + if inLibrary then + match info with + | .axiomInfo _ => + unless allowed.contains name do throwError "Unapproved library axiom: {name}" + | _ => pure () + if inLibrary && info.isTheorem then + count := count + 1 + let axioms ← collectAxioms name + if axioms.any isNativeEvaluationAxiom then nativeCount := nativeCount + 1 + for axiomName in axioms do + unless allowed.contains axiomName do + throwError "{name} depends on unapproved axiom {axiomName}" + logInfo m!"Audited {count} library theorems; {nativeCount} depend on native evaluation." diff --git a/Verification/Policy.lean b/Verification/Policy.lean new file mode 100644 index 00000000..c82a0740 --- /dev/null +++ b/Verification/Policy.lean @@ -0,0 +1,20 @@ +import Lean.Util.CollectAxioms +import Lean.Elab.Command + +open Lean Elab Command + +namespace Verification + +def standardAxioms : Array Name := #[``propext, ``Classical.choice, ``Quot.sound] + +/-- Require an audited declaration to use only the explicitly permitted axioms. -/ +def checkAxioms (decl : Name) (allowed : Array Name) : CommandElabM Unit := do + unless (← getEnv).contains decl do + throwError "Missing audited declaration: {decl}" + let axioms ← collectAxioms decl + for axiomName in axioms do + unless allowed.contains axiomName do + throwError "{decl} depends on unapproved axiom {axiomName}" + logInfo m!"{decl}: {axioms}" + +end Verification diff --git a/docs/modernization.md b/docs/modernization.md new file mode 100644 index 00000000..ca86cc0a --- /dev/null +++ b/docs/modernization.md @@ -0,0 +1,58 @@ +# Modernization validation + +Branch: `codex/lean-modernization`. +Baseline: `7a017bc3c56d3864efa9235fe7344769f9c262a2` (Lean/Mathlib 4.29.1). +Target: Lean, Mathlib and doc-gen4 4.33.1; checkdecls pinned to its previous revision. + +## Changes + +- Shortened the README and analysis module commentary; documented the exact scope + of numerical index conditions and the constant form model. +- Introduced precise Sobolev and constant-model names, retaining existing aliases. +- Replaced 45 elementary native-decide occurrences with kernel-reduced `decide`. +- Adapted the cube Sobolev inequality and smooth-family derivative bounds from + the FLT artifact, with source revision and Apache-2.0 attribution. +- Added a comment-aware source inventory, complete audit imports and a Lean + transitive-axiom policy, including strict checks for the analysis results. +- Removed routine dependency updates from verification; cache keys include the + toolchain, Lake configuration and dependency lockfile. + +## Source validation + +| Check | Baseline | Branch | +| --- | ---: | ---: | +| Explicit project axiom declarations | 15 | 15 | +| Explicit `sorry`, `admit`, `sorryAx` outside comments/strings | 0 | 0 | +| `native_decide` occurrences outside comments/strings | 1526 | 1481 | + +The source scanner's nested-comment and inline-hole regression tests pass. +The blueprint declaration synchronization and version checks pass on this branch. +The old local version check expected “GIFT Core” while the README used “K₇-Lean”; +the old verification workflow also matched comments containing “no sorry”, while +a missing `GIFTTest/` directory could mask the check with a grep error exit code. + +## Compilation status + +Local compilation is blocked by executable initialization in the Work runtime: +Lean 4.29.1 and 4.33.1 report `error: failed to locate application` even for +`lean --version`. This is not a proof failure and is not recorded as a successful +baseline build. The baseline has a successful GitHub Actions Build step in +[run 33856820678](https://github.com/Arithmon/K7-Lean/actions/runs/33856820678). +The branch's GitHub Actions workflow runs the actual build and +axiom audit. Consult that run before merging; source checks alone are insufficient. + +## Remaining obligations + +No project axiom has been discharged in this change. Numerical enclosures need a +formal connection to the defined geometric quantities; spectral assumptions need +a precise mathematical review. The new cube estimate is not the dimension-seven +H⁴ embedding theorem. Historical constants, release tags and Koide comparison +inputs are unchanged. This branch does not claim a completed compact G₂ construction. + +## First migration build + +Run 34105836451 compiled both new analysis modules successfully. It exposed four +module docstrings placed before imports (corrected), plus Mathlib migration +changes in real inner-product simplification, coefficient rewriting for the +Hodge star, and type inference for finite harmonic-basis indices. The next +commit corrects these without changing theorem statements. diff --git a/docs/proof-guide.md b/docs/proof-guide.md new file mode 100644 index 00000000..41715e75 --- /dev/null +++ b/docs/proof-guide.md @@ -0,0 +1,70 @@ +# Proof guide + +## Reusable analysis + +`GIFT/Foundations/Analysis/Sobolev/Box.lean` bounds the value of a globally Cⁿ, +complex-valued function on an n-dimensional cube by a sum of L² norms of its +iterated Fréchet derivatives through order n. The proof gives the constant +`(2 * max 1 ℓ⁻¹)^n * sqrt(ℓ^n)`, uniformly in the position of the cube, for ℓ > 0. +It does not establish the optimal H⁴ → C⁰ embedding in dimension seven, nor an +embedding on a compact manifold. The latter requires charts, norm comparisons, +localization and the appropriate regularity theorem. + +`GIFT/Foundations/Analysis/SmoothFamily.lean` gives a uniform bound on finitely many +iterated derivatives of smooth one-variable slices, with parameters in a compact +set and the variable in a closed bounded interval. The bound is existential, not +a numerical enclosure suitable for an interval certificate. + +Both proofs are adapted from Anthropic's FLT artifact; see `NOTICE`. They depend +on Mathlib, not on the framework's constants or spectral assumptions. + +## Arithmetic interfaces and geometric models + +`Sobolev/Basic.lean`, `Elliptic/Basic.lean`, and `IFT/Basic.lean` contain arithmetic +conditions and finite records. Their data alone do not prove Sobolev embedding, +elliptic regularity, or Joyce's theorem. `JoyceAnalytic.constant_model_torsion_free` +concerns the constant form model on ℝ⁷. Historical theorem names remain aliases. + +The three `Certificate.*.certified` theorems package their respective `statement` +definitions. `Certificate.gift_master_certificate` conjoins these statements; a +reader must inspect their types and dependencies, not infer a broader theorem +from the word “certificate”. + +The Koide comparison in `Relations/KoideAssembly.lean` retains its published +statement and fixed input 3477. Neither its constants nor its interpretation are +changed by this modernization. + +## Dependency policy + +- `propext`, `Classical.choice`, and `Quot.sound` are the standard logical axioms. +- Project axioms are unproved assumptions even when attributed to literature or + supported by an external computation. Moving them into fields or combining + them into one declaration does not prove their contents. +- Native reduction is tracked separately; eliminating a source occurrence of + `native_decide` does not remove a transitive dependency from other lemmas. +- A `sorryAx` dependency is forbidden, including when inherited indirectly. + +The source scanner ignores comments and strings and checks explicit holes. It +cannot replace the Lean audit. `Verification/AxiomAudit.lean` imports all library +modules and traverses their declarations, rejects unlisted axioms and prints the +axioms of the main certificates. `Verification/AnalysisChecks.lean` applies a +strict standard-axiom-only policy to the new analysis results and numerical index +conditions. No claim of independent-kernel replay is made. + +## Remaining mathematical work + +The interval module leaves five real quantities unspecified and assumes six +properties. A genuine elimination needs definitions of the corresponding metric +quantities and proofs relating exact enclosures to those definitions. Checking +an integer aggregate of externally supplied endpoints does not prove that the +endpoints enclose the intended geometric quantity. + +The spectral literature package needs a statement-by-statement review. Its +`torsion_free_correction` field only asserts the existence of two positive real +numbers. Its historical citation contains a placeholder DOI. The source's +`K3_S1` Betti table is also not a proof of the cohomology of a product. These +items must not be advertised as a formalization of the cited geometric results. + +The Chebyshev U completeness lemma from FLT has not been imported: no current +result here requires it. A Chebyshev–Cholesky error estimate needs approximation +and truncation bounds, which that completeness statement alone does not supply. diff --git a/docs/proof-inventory.json b/docs/proof-inventory.json new file mode 100644 index 00000000..6390e43d --- /dev/null +++ b/docs/proof-inventory.json @@ -0,0 +1,6007 @@ +{ + "lean_files": 150, + "axiom_declarations": [ + { + "file": "GIFT/Foundations/IntervalCertificates.lean", + "line": 43, + "name": "det_g_at_half" + }, + { + "file": "GIFT/Foundations/IntervalCertificates.lean", + "line": 46, + "name": "K3_eigenvalue_0" + }, + { + "file": "GIFT/Foundations/IntervalCertificates.lean", + "line": 47, + "name": "K3_eigenvalue_1" + }, + { + "file": "GIFT/Foundations/IntervalCertificates.lean", + "line": 48, + "name": "K3_eigenvalue_2" + }, + { + "file": "GIFT/Foundations/IntervalCertificates.lean", + "line": 49, + "name": "K3_eigenvalue_3" + }, + { + "file": "GIFT/Foundations/IntervalCertificates.lean", + "line": 86, + "name": "det_g_at_half_bracketed" + }, + { + "file": "GIFT/Foundations/IntervalCertificates.lean", + "line": 111, + "name": "K3_eigenvalue_0_bracketed" + }, + { + "file": "GIFT/Foundations/IntervalCertificates.lean", + "line": 116, + "name": "K3_eigenvalue_1_bracketed" + }, + { + "file": "GIFT/Foundations/IntervalCertificates.lean", + "line": 121, + "name": "K3_eigenvalue_2_bracketed" + }, + { + "file": "GIFT/Foundations/IntervalCertificates.lean", + "line": 126, + "name": "K3_eigenvalue_3_bracketed" + }, + { + "file": "GIFT/Foundations/IntervalCertificates.lean", + "line": 451, + "name": "PSLQ_null_in_TCS_basis" + }, + { + "file": "GIFT/Spectral/CheegerInequality.lean", + "line": 119, + "name": "cheeger_inequality" + }, + { + "file": "GIFT/Spectral/LiteratureAxioms.lean", + "line": 171, + "name": "literature_package" + }, + { + "file": "GIFT/Spectral/TCSBounds.lean", + "line": 160, + "name": "spectral_upper_bound" + }, + { + "file": "GIFT/Spectral/TCSBounds.lean", + "line": 211, + "name": "neck_dominates" + } + ], + "native_decide": [ + { + "file": "GIFT/Algebraic/G2Bform.lean", + "line": 34 + }, + { + "file": "GIFT/Algebraic/G2Rank.lean", + "line": 78 + }, + { + "file": "GIFT/Algebraic/G2Rank.lean", + "line": 80 + }, + { + "file": "GIFT/Algebraic/G2Rank.lean", + "line": 93 + }, + { + "file": "GIFT/Algebraic/G2Rank.lean", + "line": 99 + }, + { + "file": "GIFT/Algebraic/G2Rank.lean", + "line": 105 + }, + { + "file": "GIFT/Algebraic/G2Rank.lean", + "line": 118 + }, + { + "file": "GIFT/Algebraic/G2Rank.lean", + "line": 288 + }, + { + "file": "GIFT/Algebraic/G2ThreeForm.lean", + "line": 119 + }, + { + "file": "GIFT/Algebraic/G2ThreeForm.lean", + "line": 125 + }, + { + "file": "GIFT/Algebraic/G2ThreeForm.lean", + "line": 128 + }, + { + "file": "GIFT/Algebraic/G2ThreeForm.lean", + "line": 134 + }, + { + "file": "GIFT/Algebraic/G2ThreeForm.lean", + "line": 377 + }, + { + "file": "GIFT/Algebraic/G2ThreeForm.lean", + "line": 412 + }, + { + "file": "GIFT/Algebraic/G2ThreeForm.lean", + "line": 531 + }, + { + "file": "GIFT/Algebraic/G2ThreeForm.lean", + "line": 696 + }, + { + "file": "GIFT/Algebraic/G2ThreeForm.lean", + "line": 717 + }, + { + "file": "GIFT/Algebraic/GeometricSaturation.lean", + "line": 40 + }, + { + "file": "GIFT/Algebraic/GeometricSaturation.lean", + "line": 45 + }, + { + "file": "GIFT/Algebraic/GeometricSaturation.lean", + "line": 50 + }, + { + "file": "GIFT/Algebraic/GeometricSaturation.lean", + "line": 65 + }, + { + "file": "GIFT/Algebraic/GeometricSaturation.lean", + "line": 72 + }, + { + "file": "GIFT/Algebraic/GeometricSaturation.lean", + "line": 86 + }, + { + "file": "GIFT/Algebraic/GeometricSaturation.lean", + "line": 107 + }, + { + "file": "GIFT/Algebraic/Octonions.lean", + "line": 120 + }, + { + "file": "GIFT/Algebraic/Octonions.lean", + "line": 127 + }, + { + "file": "GIFT/Algebraic/Octonions.lean", + "line": 167 + }, + { + "file": "GIFT/Algebraic/Octonions.lean", + "line": 240 + }, + { + "file": "GIFT/Certificate/Foundations.lean", + "line": 644 + }, + { + "file": "GIFT/Certificate/Predictions.lean", + "line": 368 + }, + { + "file": "GIFT/Certificate/Predictions.lean", + "line": 453 + }, + { + "file": "GIFT/Certificate/Predictions.lean", + "line": 469 + }, + { + "file": "GIFT/Certificate/Predictions.lean", + "line": 488 + }, + { + "file": "GIFT/Certificate/Predictions.lean", + "line": 504 + }, + { + "file": "GIFT/Certificate/Predictions.lean", + "line": 515 + }, + { + "file": "GIFT/Certificate/Spectral.lean", + "line": 554 + }, + { + "file": "GIFT/DifferentialForms.lean", + "line": 58 + }, + { + "file": "GIFT/DifferentialForms.lean", + "line": 62 + }, + { + "file": "GIFT/DifferentialForms.lean", + "line": 81 + }, + { + "file": "GIFT/DifferentialForms.lean", + "line": 97 + }, + { + "file": "GIFT/DifferentialForms.lean", + "line": 132 + }, + { + "file": "GIFT/DifferentialForms.lean", + "line": 136 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 52 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 55 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 61 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 64 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 67 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 100 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 103 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 106 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 109 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 144 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 148 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 152 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 190 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 225 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 231 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 259 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 262 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 265 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 268 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 271 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 301 + }, + { + "file": "GIFT/Foundations/AmbroseSinger.lean", + "line": 335 + }, + { + "file": "GIFT/Foundations/Analysis/AnalyticalFoundations.lean", + "line": 64 + }, + { + "file": "GIFT/Foundations/Analysis/AnalyticalFoundations.lean", + "line": 66 + }, + { + "file": "GIFT/Foundations/Analysis/E8Lattice.lean", + "line": 725 + }, + { + "file": "GIFT/Foundations/Analysis/E8Lattice.lean", + "line": 735 + }, + { + "file": "GIFT/Foundations/Analysis/E8Lattice.lean", + "line": 744 + }, + { + "file": "GIFT/Foundations/Analysis/E8Lattice.lean", + "line": 757 + }, + { + "file": "GIFT/Foundations/Analysis/ExteriorAlgebra.lean", + "line": 100 + }, + { + "file": "GIFT/Foundations/Analysis/ExteriorAlgebra.lean", + "line": 103 + }, + { + "file": "GIFT/Foundations/Analysis/ExteriorAlgebra.lean", + "line": 106 + }, + { + "file": "GIFT/Foundations/Analysis/ExteriorAlgebra.lean", + "line": 109 + }, + { + "file": "GIFT/Foundations/Analysis/ExteriorAlgebra.lean", + "line": 119 + }, + { + "file": "GIFT/Foundations/Analysis/ExteriorAlgebra.lean", + "line": 122 + }, + { + "file": "GIFT/Foundations/Analysis/ExteriorAlgebra.lean", + "line": 131 + }, + { + "file": "GIFT/Foundations/Analysis/ExteriorAlgebra.lean", + "line": 134 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/DifferentialForms.lean", + "line": 150 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/DifferentialForms.lean", + "line": 153 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/DifferentialForms.lean", + "line": 156 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/DifferentialForms.lean", + "line": 159 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/DifferentialForms.lean", + "line": 168 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/DifferentialForms.lean", + "line": 171 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/G2FormsBridge.lean", + "line": 117 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/G2FormsBridge.lean", + "line": 214 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/G2FormsBridge.lean", + "line": 217 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/G2FormsBridge.lean", + "line": 245 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/G2Structure.lean", + "line": 133 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/G2Structure.lean", + "line": 136 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/HodgeStar.lean", + "line": 40 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/HodgeStar.lean", + "line": 43 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/HodgeStar.lean", + "line": 57 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/HodgeStar.lean", + "line": 62 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/HodgeStar.lean", + "line": 67 + }, + { + "file": "GIFT/Foundations/Analysis/G2Forms/HodgeStar.lean", + "line": 74 + }, + { + "file": "GIFT/Foundations/Analysis/G2TensorForm.lean", + "line": 167 + }, + { + "file": "GIFT/Foundations/Analysis/HarmonicForms.lean", + "line": 290 + }, + { + "file": "GIFT/Foundations/Analysis/HodgeTheory.lean", + "line": 122 + }, + { + "file": "GIFT/Foundations/Analysis/K7Orthonormality.lean", + "line": 77 + }, + { + "file": "GIFT/Foundations/Analysis/K7Orthonormality.lean", + "line": 80 + }, + { + "file": "GIFT/Foundations/Analysis/K7Orthonormality.lean", + "line": 91 + }, + { + "file": "GIFT/Foundations/Analysis/K7Orthonormality.lean", + "line": 102 + }, + { + "file": "GIFT/Foundations/Analysis/K7Orthonormality.lean", + "line": 131 + }, + { + "file": "GIFT/Foundations/Analysis/K7Orthonormality.lean", + "line": 139 + }, + { + "file": "GIFT/Foundations/Analysis/K7Orthonormality.lean", + "line": 160 + }, + { + "file": "GIFT/Foundations/Analysis/K7Orthonormality.lean", + "line": 168 + }, + { + "file": "GIFT/Foundations/Analysis/K7Orthonormality.lean", + "line": 197 + }, + { + "file": "GIFT/Foundations/Analysis/K7Orthonormality.lean", + "line": 200 + }, + { + "file": "GIFT/Foundations/Analysis/K7Orthonormality.lean", + "line": 217 + }, + { + "file": "GIFT/Foundations/Analysis/K7Orthonormality.lean", + "line": 250 + }, + { + "file": "GIFT/Foundations/Analysis/WedgeProduct.lean", + "line": 77 + }, + { + "file": "GIFT/Foundations/Analysis/WedgeProduct.lean", + "line": 80 + }, + { + "file": "GIFT/Foundations/Analysis/WedgeProduct.lean", + "line": 83 + }, + { + "file": "GIFT/Foundations/Analysis/WedgeProduct.lean", + "line": 86 + }, + { + "file": "GIFT/Foundations/Analysis/WedgeProduct.lean", + "line": 95 + }, + { + "file": "GIFT/Foundations/Analysis/WedgeProduct.lean", + "line": 99 + }, + { + "file": "GIFT/Foundations/Analysis/WedgeProduct.lean", + "line": 102 + }, + { + "file": "GIFT/Foundations/Analysis/WedgeProduct.lean", + "line": 111 + }, + { + "file": "GIFT/Foundations/Analysis/WedgeProduct.lean", + "line": 114 + }, + { + "file": "GIFT/Foundations/AnalyticalMetric.lean", + "line": 131 + }, + { + "file": "GIFT/Foundations/AnalyticalMetric.lean", + "line": 134 + }, + { + "file": "GIFT/Foundations/AnalyticalMetric.lean", + "line": 238 + }, + { + "file": "GIFT/Foundations/AnalyticalMetric.lean", + "line": 244 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 75 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 102 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 112 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 115 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 139 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 142 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 164 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 169 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 174 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 203 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 210 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 244 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 248 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 252 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 256 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 276 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 279 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 282 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 285 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 288 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 291 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 313 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 316 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 319 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 322 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 353 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 356 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 359 + }, + { + "file": "GIFT/Foundations/ConformalRigidity.lean", + "line": 387 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 39 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 82 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 88 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 137 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 184 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 220 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 245 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 325 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 359 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 413 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 426 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 516 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 528 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 577 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 619 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 677 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 762 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 800 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 854 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 877 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 878 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 879 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 880 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 881 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 882 + }, + { + "file": "GIFT/Foundations/DonaldsonCoassociativeFibration.lean", + "line": 926 + }, + { + "file": "GIFT/Foundations/E8Lattice.lean", + "line": 592 + }, + { + "file": "GIFT/Foundations/E8Lattice.lean", + "line": 596 + }, + { + "file": "GIFT/Foundations/E8Mathlib.lean", + "line": 44 + }, + { + "file": "GIFT/Foundations/E8Mathlib.lean", + "line": 65 + }, + { + "file": "GIFT/Foundations/E8Mathlib.lean", + "line": 82 + }, + { + "file": "GIFT/Foundations/E8Mathlib.lean", + "line": 105 + }, + { + "file": "GIFT/Foundations/E8Mathlib.lean", + "line": 146 + }, + { + "file": "GIFT/Foundations/E8Mathlib.lean", + "line": 151 + }, + { + "file": "GIFT/Foundations/E8Mathlib.lean", + "line": 189 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 64 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 76 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 81 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 85 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 105 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 114 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 117 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 121 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 179 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 182 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 206 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 209 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 215 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 218 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 241 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 244 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 276 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 305 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 321 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 324 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 328 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 332 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 335 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 364 + }, + { + "file": "GIFT/Foundations/ExplicitG2Metric.lean", + "line": 398 + }, + { + "file": "GIFT/Foundations/G2CrossProduct.lean", + "line": 111 + }, + { + "file": "GIFT/Foundations/G2CrossProduct.lean", + "line": 115 + }, + { + "file": "GIFT/Foundations/G2CrossProduct.lean", + "line": 220 + }, + { + "file": "GIFT/Foundations/G2CrossProduct.lean", + "line": 225 + }, + { + "file": "GIFT/Foundations/G2CrossProduct.lean", + "line": 230 + }, + { + "file": "GIFT/Foundations/G2CrossProduct.lean", + "line": 235 + }, + { + "file": "GIFT/Foundations/G2CrossProduct.lean", + "line": 259 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 125 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 132 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 139 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 143 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 144 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 145 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 146 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 147 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 149 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 156 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 159 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 162 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 165 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 196 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 202 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 207 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 212 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 217 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 228 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 262 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 315 + }, + { + "file": "GIFT/Foundations/G2DonaldsonLinkCohomology.lean", + "line": 322 + }, + { + "file": "GIFT/Foundations/G2Holonomy.lean", + "line": 70 + }, + { + "file": "GIFT/Foundations/G2Holonomy.lean", + "line": 76 + }, + { + "file": "GIFT/Foundations/G2Holonomy.lean", + "line": 124 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 53 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 56 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 86 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 88 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 108 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 110 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 124 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 127 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 130 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 137 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 148 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 150 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 157 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 159 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 164 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 166 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 185 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 192 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 211 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 218 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 223 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 227 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 288 + }, + { + "file": "GIFT/Foundations/G2IrrepLatticeCertificate.lean", + "line": 296 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 71 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 75 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 79 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 83 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 87 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 91 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 107 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 108 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 109 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 110 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 117 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 165 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 168 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 171 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 174 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 177 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 220 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 284 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 287 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 290 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 293 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 296 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 299 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 302 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 309 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 317 + }, + { + "file": "GIFT/Foundations/G2TCSLatticeCertificate.lean", + "line": 343 + }, + { + "file": "GIFT/Foundations/GoldenRatioPowers.lean", + "line": 185 + }, + { + "file": "GIFT/Foundations/GoldenRatioPowers.lean", + "line": 302 + }, + { + "file": "GIFT/Foundations/GoldenRatioPowers.lean", + "line": 305 + }, + { + "file": "GIFT/Foundations/GraphTheory.lean", + "line": 56 + }, + { + "file": "GIFT/Foundations/GraphTheory.lean", + "line": 61 + }, + { + "file": "GIFT/Foundations/GraphTheory.lean", + "line": 83 + }, + { + "file": "GIFT/Foundations/GraphTheory.lean", + "line": 91 + }, + { + "file": "GIFT/Foundations/GraphTheory.lean", + "line": 115 + }, + { + "file": "GIFT/Foundations/GraphTheory.lean", + "line": 118 + }, + { + "file": "GIFT/Foundations/K3AutomorphismPackage.lean", + "line": 96 + }, + { + "file": "GIFT/Foundations/K3AutomorphismPackage.lean", + "line": 152 + }, + { + "file": "GIFT/Foundations/K3AutomorphismPackage.lean", + "line": 221 + }, + { + "file": "GIFT/Foundations/K3AutomorphismPackage.lean", + "line": 270 + }, + { + "file": "GIFT/Foundations/K3AutomorphismPackage.lean", + "line": 275 + }, + { + "file": "GIFT/Foundations/K3AutomorphismPackage.lean", + "line": 328 + }, + { + "file": "GIFT/Foundations/K3ClosedFormBoxEnclosures.lean", + "line": 4148 + }, + { + "file": "GIFT/Foundations/K3ClosedFormBoxEnclosures.lean", + "line": 4152 + }, + { + "file": "GIFT/Foundations/K3ClosedFormBoxEnclosures.lean", + "line": 4160 + }, + { + "file": "GIFT/Foundations/K3ClosedFormWitness.lean", + "line": 149 + }, + { + "file": "GIFT/Foundations/K3ClosedFormWitness.lean", + "line": 208 + }, + { + "file": "GIFT/Foundations/K3ClosedFormWitness.lean", + "line": 211 + }, + { + "file": "GIFT/Foundations/K3ClosedFormWitness.lean", + "line": 216 + }, + { + "file": "GIFT/Foundations/K3ClosedFormWitness.lean", + "line": 223 + }, + { + "file": "GIFT/Foundations/K3ClosedFormWitness.lean", + "line": 228 + }, + { + "file": "GIFT/Foundations/K3ClosedFormWitness.lean", + "line": 241 + }, + { + "file": "GIFT/Foundations/K3ClosedFormWitness.lean", + "line": 246 + }, + { + "file": "GIFT/Foundations/K3ClosedFormWitness.lean", + "line": 278 + }, + { + "file": "GIFT/Foundations/K3ClosedFormWitness.lean", + "line": 279 + }, + { + "file": "GIFT/Foundations/K3ClosedFormWitness.lean", + "line": 297 + }, + { + "file": "GIFT/Foundations/K3ClosedFormWitness.lean", + "line": 311 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 75 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 79 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 115 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 122 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 181 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 184 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 190 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 202 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 237 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 249 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 252 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 304 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 307 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 310 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 313 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 316 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 326 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 329 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 333 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 337 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 341 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 370 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 373 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 395 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 398 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 404 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 407 + }, + { + "file": "GIFT/Foundations/K3HarmonicCorrection.lean", + "line": 445 + }, + { + "file": "GIFT/Foundations/K3IsotypeLefschetzCertificate.lean", + "line": 92 + }, + { + "file": "GIFT/Foundations/K3IsotypeLefschetzCertificate.lean", + "line": 111 + }, + { + "file": "GIFT/Foundations/K3IsotypeLefschetzCertificate.lean", + "line": 114 + }, + { + "file": "GIFT/Foundations/K3IsotypeLefschetzCertificate.lean", + "line": 122 + }, + { + "file": "GIFT/Foundations/K3IsotypeLefschetzCertificate.lean", + "line": 125 + }, + { + "file": "GIFT/Foundations/K3IsotypeLefschetzCertificate.lean", + "line": 143 + }, + { + "file": "GIFT/Foundations/K3IsotypeLefschetzCertificate.lean", + "line": 147 + }, + { + "file": "GIFT/Foundations/K3IsotypeLefschetzCertificate.lean", + "line": 151 + }, + { + "file": "GIFT/Foundations/K3IsotypeLefschetzCertificate.lean", + "line": 164 + }, + { + "file": "GIFT/Foundations/K3IsotypeLefschetzCertificate.lean", + "line": 167 + }, + { + "file": "GIFT/Foundations/K3IsotypeLefschetzCertificate.lean", + "line": 173 + }, + { + "file": "GIFT/Foundations/K3IsotypeLefschetzCertificate.lean", + "line": 179 + }, + { + "file": "GIFT/Foundations/K3IsotypeLefschetzCertificate.lean", + "line": 198 + }, + { + "file": "GIFT/Foundations/K3IsotypeLefschetzCertificate.lean", + "line": 205 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4675 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4676 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4677 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4678 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4679 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4680 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4681 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4682 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4683 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4684 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4685 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4686 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4687 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4688 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4689 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4690 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4691 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4692 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4693 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4694 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4695 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4696 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4697 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4698 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4699 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4700 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4701 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4702 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4703 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4704 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4705 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4706 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4707 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4708 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4709 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4710 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4711 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4712 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4713 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4714 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4715 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4716 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4717 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4718 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4719 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4720 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4721 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4722 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4723 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4724 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4725 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4726 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4727 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4728 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4729 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4730 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4731 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4732 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4733 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4734 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4735 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4736 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4737 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4738 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4739 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4740 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4741 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4742 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4743 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4744 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4745 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4746 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4747 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4748 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4749 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4750 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4751 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4752 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4753 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4754 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4755 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4756 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4757 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4758 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4759 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4760 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4761 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4762 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4763 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4764 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4765 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4766 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4767 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4768 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4769 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4770 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4771 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4772 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4773 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4774 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4775 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4776 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4777 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4778 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4779 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4780 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4781 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4782 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4783 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4784 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4785 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4786 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4787 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4788 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4789 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4790 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4791 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4792 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4793 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4794 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4795 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4796 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4797 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4798 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4799 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4800 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4801 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4802 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4803 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4804 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4805 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4806 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4807 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4808 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4809 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4810 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4811 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4812 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4813 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4814 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4815 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4816 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4817 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4818 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4819 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4820 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4821 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4822 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4823 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4824 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4825 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4826 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4827 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4828 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4829 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4830 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4831 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4832 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4833 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4834 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4835 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4836 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4837 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4838 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4839 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4840 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4841 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4842 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4843 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4844 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4845 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4846 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4847 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4848 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4849 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4850 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4851 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4852 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4853 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4854 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4855 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4856 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4857 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4858 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4859 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4860 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4861 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4862 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4863 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4864 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4865 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4866 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4867 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4868 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4869 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4870 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4871 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4872 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4873 + }, + { + "file": "GIFT/Foundations/K3KrawczykContainment.lean", + "line": 4874 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 95 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 96 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 133 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 137 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 142 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 181 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 185 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 207 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 272 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 278 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 284 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 288 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 312 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 320 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 325 + }, + { + "file": "GIFT/Foundations/K3NewtonKantorovich.lean", + "line": 350 + }, + { + "file": "GIFT/Foundations/K3VandermondeSmoothness.lean", + "line": 55 + }, + { + "file": "GIFT/Foundations/K3VandermondeSmoothness.lean", + "line": 66 + }, + { + "file": "GIFT/Foundations/K3VandermondeSmoothness.lean", + "line": 89 + }, + { + "file": "GIFT/Foundations/K3VandermondeSmoothness.lean", + "line": 94 + }, + { + "file": "GIFT/Foundations/K3VandermondeSmoothness.lean", + "line": 101 + }, + { + "file": "GIFT/Foundations/K3VandermondeSmoothness.lean", + "line": 111 + }, + { + "file": "GIFT/Foundations/K3VandermondeSmoothness.lean", + "line": 133 + }, + { + "file": "GIFT/Foundations/K3VandermondeSmoothness.lean", + "line": 139 + }, + { + "file": "GIFT/Foundations/K3VandermondeSmoothness.lean", + "line": 157 + }, + { + "file": "GIFT/Foundations/K3VandermondeSmoothness.lean", + "line": 164 + }, + { + "file": "GIFT/Foundations/K7NuBar.lean", + "line": 54 + }, + { + "file": "GIFT/Foundations/K7NuBar.lean", + "line": 96 + }, + { + "file": "GIFT/Foundations/K7NuBar.lean", + "line": 129 + }, + { + "file": "GIFT/Foundations/K7NuBar.lean", + "line": 185 + }, + { + "file": "GIFT/Foundations/K7NuBar.lean", + "line": 198 + }, + { + "file": "GIFT/Foundations/K7NuBar.lean", + "line": 234 + }, + { + "file": "GIFT/Foundations/K7NuBar.lean", + "line": 280 + }, + { + "file": "GIFT/Foundations/K7NuBar.lean", + "line": 320 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 68 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 72 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 75 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 78 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 100 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 103 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 106 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 144 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 147 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 150 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 153 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 188 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 191 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 219 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 227 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 238 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 244 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 286 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 291 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 306 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 310 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 315 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 320 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 325 + }, + { + "file": "GIFT/Foundations/MetricEigenvalues.lean", + "line": 391 + }, + { + "file": "GIFT/Foundations/MetricGapClosure.lean", + "line": 64 + }, + { + "file": "GIFT/Foundations/MetricGapClosure.lean", + "line": 103 + }, + { + "file": "GIFT/Foundations/MetricGapClosure.lean", + "line": 111 + }, + { + "file": "GIFT/Foundations/MetricGapClosure.lean", + "line": 178 + }, + { + "file": "GIFT/Foundations/MetricGapClosure.lean", + "line": 182 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 99 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 102 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 105 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 165 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 168 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 171 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 174 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 205 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 218 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 245 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 248 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 280 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 285 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 349 + }, + { + "file": "GIFT/Foundations/NewtonKantorovich.lean", + "line": 399 + }, + { + "file": "GIFT/Foundations/OctonionBridge.lean", + "line": 202 + }, + { + "file": "GIFT/Foundations/OctonionBridge.lean", + "line": 228 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 47 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 51 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 54 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 57 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 61 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 65 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 68 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 71 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 91 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 95 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 98 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 101 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 104 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 132 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 135 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 139 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 144 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 147 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 151 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 154 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 158 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 162 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 186 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 191 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 195 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 200 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 227 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 231 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 234 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 237 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 240 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 243 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 261 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 265 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 269 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 273 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 276 + }, + { + "file": "GIFT/Foundations/PoincareDuality.lean", + "line": 300 + }, + { + "file": "GIFT/Foundations/RootSystems.lean", + "line": 42 + }, + { + "file": "GIFT/Foundations/RootSystems.lean", + "line": 48 + }, + { + "file": "GIFT/Foundations/RootSystems.lean", + "line": 209 + }, + { + "file": "GIFT/Foundations/RootSystems.lean", + "line": 225 + }, + { + "file": "GIFT/Foundations/RootSystems.lean", + "line": 389 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 71 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 74 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 91 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 97 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 108 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 133 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 136 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 139 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 144 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 149 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 175 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 178 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 182 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 186 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 190 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 214 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 217 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 220 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 230 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 261 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 264 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 267 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 270 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 273 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 276 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 288 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 292 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 315 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 318 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 321 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 324 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 327 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 341 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 344 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 347 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 350 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 359 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 381 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 384 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 392 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 397 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 402 + }, + { + "file": "GIFT/Foundations/SpectralScaling.lean", + "line": 434 + }, + { + "file": "GIFT/Foundations/TCSConstruction.lean", + "line": 231 + }, + { + "file": "GIFT/Foundations/TCSConstruction.lean", + "line": 232 + }, + { + "file": "GIFT/Foundations/TCSConstruction.lean", + "line": 235 + }, + { + "file": "GIFT/Foundations/TCSConstruction.lean", + "line": 238 + }, + { + "file": "GIFT/Foundations/TCSConstruction.lean", + "line": 253 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 52 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 55 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 59 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 62 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 90 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 93 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 99 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 102 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 106 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 109 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 134 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 137 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 143 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 149 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 153 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 156 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 159 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 163 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 182 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 188 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 192 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 195 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 198 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 224 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 227 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 230 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 233 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 262 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 278 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 283 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 287 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 307 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 310 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 314 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 319 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 342 + }, + { + "file": "GIFT/Foundations/TCSPiecewiseMetric.lean", + "line": 372 + }, + { + "file": "GIFT/Geometry/DifferentialFormsR7.lean", + "line": 226 + }, + { + "file": "GIFT/Geometry/DifferentialFormsR7.lean", + "line": 229 + }, + { + "file": "GIFT/Geometry/DifferentialFormsR7.lean", + "line": 243 + }, + { + "file": "GIFT/Geometry/DifferentialFormsR7.lean", + "line": 243 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 219 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 222 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 225 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 228 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 231 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 234 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 237 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 240 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 249 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 252 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 255 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 278 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 278 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 278 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 279 + }, + { + "file": "GIFT/Geometry/Exterior.lean", + "line": 279 + }, + { + "file": "GIFT/Geometry/HodgeStarR7.lean", + "line": 39 + }, + { + "file": "GIFT/Geometry/HodgeStarR7.lean", + "line": 46 + }, + { + "file": "GIFT/Geometry/HodgeStarR7.lean", + "line": 49 + }, + { + "file": "GIFT/Geometry.lean", + "line": 81 + }, + { + "file": "GIFT/Geometry.lean", + "line": 81 + }, + { + "file": "GIFT/Geometry.lean", + "line": 81 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 31 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 36 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 44 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 47 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 54 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 58 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 66 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 70 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 73 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 117 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 129 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 134 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 137 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 140 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 150 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 153 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 160 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 178 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 181 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 184 + }, + { + "file": "GIFT/Hierarchy/AbsoluteMasses.lean", + "line": 207 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 68 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 71 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 74 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 122 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 127 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 132 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 137 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 142 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 150 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 213 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 218 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 223 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 228 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 233 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 238 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 243 + }, + { + "file": "GIFT/Hierarchy/AssociativeVolumes.lean", + "line": 289 + }, + { + "file": "GIFT/Hierarchy/DimensionalGap.lean", + "line": 40 + }, + { + "file": "GIFT/Hierarchy/DimensionalGap.lean", + "line": 89 + }, + { + "file": "GIFT/Hierarchy/DimensionalGap.lean", + "line": 90 + }, + { + "file": "GIFT/Hierarchy/DimensionalGap.lean", + "line": 208 + }, + { + "file": "GIFT/Hierarchy/DimensionalGap.lean", + "line": 209 + }, + { + "file": "GIFT/Hierarchy/DimensionalGap.lean", + "line": 245 + }, + { + "file": "GIFT/Hierarchy/DimensionalGap.lean", + "line": 248 + }, + { + "file": "GIFT/Hierarchy/DimensionalGap.lean", + "line": 252 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 63 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 86 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 89 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 99 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 102 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 105 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 108 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 111 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 116 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 116 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 116 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 116 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 131 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 134 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 137 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 140 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 143 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 160 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 163 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 181 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 184 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 201 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 204 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 207 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 210 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 213 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 216 + }, + { + "file": "GIFT/Hierarchy/E6Cascade.lean", + "line": 221 + }, + { + "file": "GIFT/Hierarchy/GaugeBundleData.lean", + "line": 53 + }, + { + "file": "GIFT/Hierarchy/GaugeBundleData.lean", + "line": 57 + }, + { + "file": "GIFT/Hierarchy/GaugeBundleData.lean", + "line": 92 + }, + { + "file": "GIFT/Hierarchy/GaugeBundleData.lean", + "line": 95 + }, + { + "file": "GIFT/Hierarchy/GaugeBundleData.lean", + "line": 127 + }, + { + "file": "GIFT/Hierarchy/GaugeBundleData.lean", + "line": 130 + }, + { + "file": "GIFT/Hierarchy/GaugeBundleData.lean", + "line": 133 + }, + { + "file": "GIFT/Hierarchy/GaugeBundleData.lean", + "line": 177 + }, + { + "file": "GIFT/Hierarchy/GaugeBundleData.lean", + "line": 180 + }, + { + "file": "GIFT/Hierarchy/GaugeBundleData.lean", + "line": 183 + }, + { + "file": "GIFT/Hierarchy/GaugeBundleData.lean", + "line": 187 + }, + { + "file": "GIFT/Hierarchy/GaugeBundleData.lean", + "line": 231 + }, + { + "file": "GIFT/Hierarchy/TCSGaugeBreaking.lean", + "line": 67 + }, + { + "file": "GIFT/Hierarchy/TCSGaugeBreaking.lean", + "line": 71 + }, + { + "file": "GIFT/Hierarchy/TCSGaugeBreaking.lean", + "line": 81 + }, + { + "file": "GIFT/Hierarchy/TCSGaugeBreaking.lean", + "line": 104 + }, + { + "file": "GIFT/Hierarchy/TCSGaugeBreaking.lean", + "line": 111 + }, + { + "file": "GIFT/Hierarchy/TCSGaugeBreaking.lean", + "line": 114 + }, + { + "file": "GIFT/Hierarchy/TCSGaugeBreaking.lean", + "line": 133 + }, + { + "file": "GIFT/Hierarchy/TCSGaugeBreaking.lean", + "line": 137 + }, + { + "file": "GIFT/Hierarchy/TCSGaugeBreaking.lean", + "line": 141 + }, + { + "file": "GIFT/Hierarchy/TCSGaugeBreaking.lean", + "line": 150 + }, + { + "file": "GIFT/Hierarchy/TCSGaugeBreaking.lean", + "line": 158 + }, + { + "file": "GIFT/Hierarchy/TCSGaugeBreaking.lean", + "line": 224 + }, + { + "file": "GIFT/Hierarchy/VacuumStructure.lean", + "line": 36 + }, + { + "file": "GIFT/Hierarchy/VacuumStructure.lean", + "line": 39 + }, + { + "file": "GIFT/Hierarchy/VacuumStructure.lean", + "line": 88 + }, + { + "file": "GIFT/Hierarchy/VacuumStructure.lean", + "line": 91 + }, + { + "file": "GIFT/Hierarchy/VacuumStructure.lean", + "line": 109 + }, + { + "file": "GIFT/Hierarchy/VacuumStructure.lean", + "line": 116 + }, + { + "file": "GIFT/Hierarchy/VacuumStructure.lean", + "line": 119 + }, + { + "file": "GIFT/Hierarchy/VacuumStructure.lean", + "line": 150 + }, + { + "file": "GIFT/Hierarchy/VacuumStructure.lean", + "line": 168 + }, + { + "file": "GIFT/Hierarchy/VacuumStructure.lean", + "line": 171 + }, + { + "file": "GIFT/ImplicitFunction.lean", + "line": 52 + }, + { + "file": "GIFT/ImplicitFunction.lean", + "line": 60 + }, + { + "file": "GIFT/ImplicitFunction.lean", + "line": 92 + }, + { + "file": "GIFT/ImplicitFunction.lean", + "line": 103 + }, + { + "file": "GIFT/ImplicitFunction.lean", + "line": 108 + }, + { + "file": "GIFT/ImplicitFunction.lean", + "line": 118 + }, + { + "file": "GIFT/ImplicitFunction.lean", + "line": 135 + }, + { + "file": "GIFT/ImplicitFunction.lean", + "line": 151 + }, + { + "file": "GIFT/IntervalArithmetic.lean", + "line": 60 + }, + { + "file": "GIFT/IntervalArithmetic.lean", + "line": 64 + }, + { + "file": "GIFT/IntervalArithmetic.lean", + "line": 68 + }, + { + "file": "GIFT/IntervalArithmetic.lean", + "line": 74 + }, + { + "file": "GIFT/IntervalArithmetic.lean", + "line": 86 + }, + { + "file": "GIFT/IntervalArithmetic.lean", + "line": 87 + }, + { + "file": "GIFT/IntervalArithmetic.lean", + "line": 88 + }, + { + "file": "GIFT/IntervalArithmetic.lean", + "line": 92 + }, + { + "file": "GIFT/IntervalArithmetic.lean", + "line": 96 + }, + { + "file": "GIFT/Joyce.lean", + "line": 74 + }, + { + "file": "GIFT/Joyce.lean", + "line": 78 + }, + { + "file": "GIFT/Joyce.lean", + "line": 99 + }, + { + "file": "GIFT/Joyce.lean", + "line": 101 + }, + { + "file": "GIFT/Joyce.lean", + "line": 102 + }, + { + "file": "GIFT/Joyce.lean", + "line": 123 + }, + { + "file": "GIFT/Joyce.lean", + "line": 142 + }, + { + "file": "GIFT/Joyce.lean", + "line": 156 + }, + { + "file": "GIFT/Observables/BosonMasses.lean", + "line": 99 + }, + { + "file": "GIFT/Observables/BosonMasses.lean", + "line": 102 + }, + { + "file": "GIFT/Predictions/CP/DeltaCPNuBarConjecture.lean", + "line": 52 + }, + { + "file": "GIFT/Predictions/CP/DeltaCPNuBarConjecture.lean", + "line": 63 + }, + { + "file": "GIFT/Relations/CompactificationCorrection.lean", + "line": 63 + }, + { + "file": "GIFT/Relations/CompactificationCorrection.lean", + "line": 66 + }, + { + "file": "GIFT/Relations/CompactificationCorrection.lean", + "line": 69 + }, + { + "file": "GIFT/Relations/CompactificationCorrection.lean", + "line": 72 + }, + { + "file": "GIFT/Relations/CompactificationCorrection.lean", + "line": 75 + }, + { + "file": "GIFT/Relations/CompactificationCorrection.lean", + "line": 78 + }, + { + "file": "GIFT/Relations/CompactificationCorrection.lean", + "line": 81 + }, + { + "file": "GIFT/Relations/CompactificationCorrection.lean", + "line": 86 + }, + { + "file": "GIFT/Relations/CompactificationCorrection.lean", + "line": 95 + }, + { + "file": "GIFT/Relations/CompactificationCorrection.lean", + "line": 99 + }, + { + "file": "GIFT/Relations/CompactificationCorrection.lean", + "line": 102 + }, + { + "file": "GIFT/Relations/CompactificationCorrection.lean", + "line": 124 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 47 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 59 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 62 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 72 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 85 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 88 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 91 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 94 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 98 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 113 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 120 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 127 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 148 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 150 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 173 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 173 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 173 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 176 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 176 + }, + { + "file": "GIFT/Relations/Cosmology.lean", + "line": 176 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 42 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 44 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 51 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 53 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 62 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 64 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 71 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 73 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 75 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 82 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 84 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 99 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 101 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 112 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 114 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 128 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 137 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 140 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 143 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 150 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 153 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 156 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 163 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 164 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 165 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 179 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 182 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 185 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 193 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 196 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 199 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 202 + }, + { + "file": "GIFT/Relations/ExceptionalChain.lean", + "line": 233 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 30 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 33 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 36 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 41 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 53 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 56 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 61 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 65 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 68 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 73 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 76 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 79 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 87 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 93 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 96 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 99 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 102 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 110 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 113 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 117 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 121 + }, + { + "file": "GIFT/Relations/ExceptionalGroups.lean", + "line": 137 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 61 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 64 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 67 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 70 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 73 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 76 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 79 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 82 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 85 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 88 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 91 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 94 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 97 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 100 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 122 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 129 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 136 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 139 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 158 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 161 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 182 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 186 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 189 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 192 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 225 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 235 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 250 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 262 + }, + { + "file": "GIFT/Relations/FanoSelectionPrinciple.lean", + "line": 277 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 43 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 47 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 50 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 84 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 102 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 108 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 112 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 115 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 137 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 140 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 143 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 149 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 152 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 176 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 179 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 182 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 185 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 188 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 195 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 201 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 204 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 227 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 230 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 233 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 236 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 240 + }, + { + "file": "GIFT/Relations/G2MetricProperties.lean", + "line": 295 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 24 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 27 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 30 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 33 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 36 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 48 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 59 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 62 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 76 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 83 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 86 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 93 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 106 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 111 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 118 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 126 + }, + { + "file": "GIFT/Relations/GaugeSector.lean", + "line": 130 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 24 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 39 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 46 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 53 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 60 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 63 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 78 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 91 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 100 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 111 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 119 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 127 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 142 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 149 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 159 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 167 + }, + { + "file": "GIFT/Relations/GoldenRatio.lean", + "line": 189 + }, + { + "file": "GIFT/Relations/IrrationalSector.lean", + "line": 26 + }, + { + "file": "GIFT/Relations/IrrationalSector.lean", + "line": 30 + }, + { + "file": "GIFT/Relations/IrrationalSector.lean", + "line": 46 + }, + { + "file": "GIFT/Relations/IrrationalSector.lean", + "line": 60 + }, + { + "file": "GIFT/Relations/IrrationalSector.lean", + "line": 64 + }, + { + "file": "GIFT/Relations/IrrationalSector.lean", + "line": 78 + }, + { + "file": "GIFT/Relations/LandauerDarkEnergy.lean", + "line": 38 + }, + { + "file": "GIFT/Relations/LandauerDarkEnergy.lean", + "line": 43 + }, + { + "file": "GIFT/Relations/LandauerDarkEnergy.lean", + "line": 50 + }, + { + "file": "GIFT/Relations/LandauerDarkEnergy.lean", + "line": 71 + }, + { + "file": "GIFT/Relations/LandauerDarkEnergy.lean", + "line": 77 + }, + { + "file": "GIFT/Relations/LandauerDarkEnergy.lean", + "line": 93 + }, + { + "file": "GIFT/Relations/LandauerDarkEnergy.lean", + "line": 99 + }, + { + "file": "GIFT/Relations/LandauerDarkEnergy.lean", + "line": 108 + }, + { + "file": "GIFT/Relations/LandauerDarkEnergy.lean", + "line": 114 + }, + { + "file": "GIFT/Relations/LandauerDarkEnergy.lean", + "line": 140 + }, + { + "file": "GIFT/Relations/LandauerDarkEnergy.lean", + "line": 162 + }, + { + "file": "GIFT/Relations/LeptonSector.lean", + "line": 27 + }, + { + "file": "GIFT/Relations/LeptonSector.lean", + "line": 30 + }, + { + "file": "GIFT/Relations/LeptonSector.lean", + "line": 33 + }, + { + "file": "GIFT/Relations/LeptonSector.lean", + "line": 42 + }, + { + "file": "GIFT/Relations/LeptonSector.lean", + "line": 50 + }, + { + "file": "GIFT/Relations/LeptonSector.lean", + "line": 53 + }, + { + "file": "GIFT/Relations/LeptonSector.lean", + "line": 62 + }, + { + "file": "GIFT/Relations/LeptonSector.lean", + "line": 78 + }, + { + "file": "GIFT/Relations/LeptonSector.lean", + "line": 101 + }, + { + "file": "GIFT/Relations/LeptonSector.lean", + "line": 105 + }, + { + "file": "GIFT/Relations/LeptonSector.lean", + "line": 108 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 23 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 30 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 43 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 55 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 88 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 105 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 116 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 125 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 129 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 139 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 147 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 158 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 183 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 183 + }, + { + "file": "GIFT/Relations/NeutrinoSector.lean", + "line": 184 + }, + { + "file": "GIFT/Relations/OverDetermination.lean", + "line": 300 + }, + { + "file": "GIFT/Relations/QuarkSector.lean", + "line": 17 + }, + { + "file": "GIFT/Relations/QuarkSector.lean", + "line": 20 + }, + { + "file": "GIFT/Relations/QuarkSector.lean", + "line": 23 + }, + { + "file": "GIFT/Relations/QuarkSector.lean", + "line": 32 + }, + { + "file": "GIFT/Relations/QuarkSector.lean", + "line": 43 + }, + { + "file": "GIFT/Relations/QuarkSector.lean", + "line": 53 + }, + { + "file": "GIFT/Relations/QuarkSector.lean", + "line": 62 + }, + { + "file": "GIFT/Relations/QuarkSector.lean", + "line": 65 + }, + { + "file": "GIFT/Relations/QuarkSector.lean", + "line": 82 + }, + { + "file": "GIFT/Relations/SO16Relations.lean", + "line": 34 + }, + { + "file": "GIFT/Relations/SO16Relations.lean", + "line": 41 + }, + { + "file": "GIFT/Relations/SO16Relations.lean", + "line": 46 + }, + { + "file": "GIFT/Relations/SO16Relations.lean", + "line": 51 + }, + { + "file": "GIFT/Relations/SO16Relations.lean", + "line": 56 + }, + { + "file": "GIFT/Relations/SO16Relations.lean", + "line": 81 + }, + { + "file": "GIFT/Relations/SO16Relations.lean", + "line": 87 + }, + { + "file": "GIFT/Relations/SO16Relations.lean", + "line": 104 + }, + { + "file": "GIFT/Relations/SO16Relations.lean", + "line": 110 + }, + { + "file": "GIFT/Relations/SO16Relations.lean", + "line": 122 + }, + { + "file": "GIFT/Relations/SO16Relations.lean", + "line": 127 + }, + { + "file": "GIFT/Relations/SO16Relations.lean", + "line": 136 + }, + { + "file": "GIFT/Relations/SO16Relations.lean", + "line": 141 + }, + { + "file": "GIFT/Relations/SO16Relations.lean", + "line": 164 + }, + { + "file": "GIFT/Relations/SectorClassification.lean", + "line": 66 + }, + { + "file": "GIFT/Relations/SectorClassification.lean", + "line": 71 + }, + { + "file": "GIFT/Relations/SectorClassification.lean", + "line": 101 + }, + { + "file": "GIFT/Relations/SectorClassification.lean", + "line": 106 + }, + { + "file": "GIFT/Relations/SectorClassification.lean", + "line": 111 + }, + { + "file": "GIFT/Relations/SectorClassification.lean", + "line": 141 + }, + { + "file": "GIFT/Relations/SectorClassification.lean", + "line": 146 + }, + { + "file": "GIFT/Relations/SectorClassification.lean", + "line": 151 + }, + { + "file": "GIFT/Relations/SectorClassification.lean", + "line": 193 + }, + { + "file": "GIFT/Relations/SectorClassification.lean", + "line": 242 + }, + { + "file": "GIFT/Relations/SectorClassification.lean", + "line": 248 + }, + { + "file": "GIFT/Relations/SectorClassification.lean", + "line": 253 + }, + { + "file": "GIFT/Relations/SectorClassification.lean", + "line": 258 + }, + { + "file": "GIFT/Relations/SectorClassification.lean", + "line": 284 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 17 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 22 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 32 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 46 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 49 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 52 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 59 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 62 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 70 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 83 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 86 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 95 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 100 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 106 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 113 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 118 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 127 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 130 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 133 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 140 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 143 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 146 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 149 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 156 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 159 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 162 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 165 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 168 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 171 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 195 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 198 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 201 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 204 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 211 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 238 + }, + { + "file": "GIFT/Relations/Structural.lean", + "line": 260 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 45 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 55 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 59 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 69 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 73 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 83 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 88 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 94 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 104 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 109 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 112 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 116 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 134 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 144 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 147 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 150 + }, + { + "file": "GIFT/Relations/TauBounds.lean", + "line": 153 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 58 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 61 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 64 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 67 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 70 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 73 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 76 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 79 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 95 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 136 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 142 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 145 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 148 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 151 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 154 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 157 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 169 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 179 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 182 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 185 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 188 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 191 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 205 + }, + { + "file": "GIFT/Relations/V33Additions.lean", + "line": 227 + }, + { + "file": "GIFT/Relations.lean", + "line": 11 + }, + { + "file": "GIFT/Relations.lean", + "line": 14 + }, + { + "file": "GIFT/Relations.lean", + "line": 33 + }, + { + "file": "GIFT/Relations.lean", + "line": 41 + }, + { + "file": "GIFT/Relations.lean", + "line": 44 + }, + { + "file": "GIFT/Sobolev.lean", + "line": 39 + }, + { + "file": "GIFT/Sobolev.lean", + "line": 47 + }, + { + "file": "GIFT/Sobolev.lean", + "line": 51 + }, + { + "file": "GIFT/Sobolev.lean", + "line": 56 + }, + { + "file": "GIFT/Sobolev.lean", + "line": 73 + }, + { + "file": "GIFT/Sobolev.lean", + "line": 84 + }, + { + "file": "GIFT/Sobolev.lean", + "line": 89 + }, + { + "file": "GIFT/Sobolev.lean", + "line": 103 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 84 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 87 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 90 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 95 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 98 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 101 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 107 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 110 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 123 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 129 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 138 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 143 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 150 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 162 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 167 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 174 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 179 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 182 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 193 + }, + { + "file": "GIFT/Spectral/AnalyticalMassGap.lean", + "line": 198 + }, + { + "file": "GIFT/Spectral/CheegerInequality.lean", + "line": 158 + }, + { + "file": "GIFT/Spectral/CheegerInequality.lean", + "line": 167 + }, + { + "file": "GIFT/Spectral/CheegerInequality.lean", + "line": 172 + }, + { + "file": "GIFT/Spectral/CheegerInequality.lean", + "line": 187 + }, + { + "file": "GIFT/Spectral/CheegerInequality.lean", + "line": 192 + }, + { + "file": "GIFT/Spectral/CheegerInequality.lean", + "line": 201 + }, + { + "file": "GIFT/Spectral/CheegerInequality.lean", + "line": 206 + }, + { + "file": "GIFT/Spectral/CheegerInequality.lean", + "line": 223 + }, + { + "file": "GIFT/Spectral/CheegerInequality.lean", + "line": 228 + }, + { + "file": "GIFT/Spectral/CheegerInequality.lean", + "line": 247 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 51 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 54 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 57 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 60 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 102 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 105 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 108 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 136 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 141 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 144 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 176 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 183 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 200 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 208 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 243 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 248 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 254 + }, + { + "file": "GIFT/Spectral/ComputedSpectrum.lean", + "line": 297 + }, + { + "file": "GIFT/Spectral/ComputedWeylLaw.lean", + "line": 69 + }, + { + "file": "GIFT/Spectral/ComputedWeylLaw.lean", + "line": 73 + }, + { + "file": "GIFT/Spectral/ComputedWeylLaw.lean", + "line": 77 + }, + { + "file": "GIFT/Spectral/ComputedWeylLaw.lean", + "line": 107 + }, + { + "file": "GIFT/Spectral/ComputedWeylLaw.lean", + "line": 110 + }, + { + "file": "GIFT/Spectral/ComputedWeylLaw.lean", + "line": 113 + }, + { + "file": "GIFT/Spectral/ComputedWeylLaw.lean", + "line": 141 + }, + { + "file": "GIFT/Spectral/ComputedWeylLaw.lean", + "line": 144 + }, + { + "file": "GIFT/Spectral/ComputedWeylLaw.lean", + "line": 174 + }, + { + "file": "GIFT/Spectral/ComputedYukawa.lean", + "line": 107 + }, + { + "file": "GIFT/Spectral/ComputedYukawa.lean", + "line": 113 + }, + { + "file": "GIFT/Spectral/ComputedYukawa.lean", + "line": 120 + }, + { + "file": "GIFT/Spectral/ComputedYukawa.lean", + "line": 127 + }, + { + "file": "GIFT/Spectral/ComputedYukawa.lean", + "line": 156 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 56 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 61 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 66 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 114 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 140 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 143 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 146 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 149 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 153 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 162 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 169 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 201 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 224 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 228 + }, + { + "file": "GIFT/Spectral/KKSpectralBridge.lean", + "line": 253 + }, + { + "file": "GIFT/Spectral/LiteratureAxioms.lean", + "line": 236 + }, + { + "file": "GIFT/Spectral/LiteratureAxioms.lean", + "line": 241 + }, + { + "file": "GIFT/Spectral/LiteratureAxioms.lean", + "line": 260 + }, + { + "file": "GIFT/Spectral/LiteratureAxioms.lean", + "line": 261 + }, + { + "file": "GIFT/Spectral/LiteratureAxioms.lean", + "line": 262 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 85 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 90 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 98 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 102 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 105 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 108 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 113 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 122 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 127 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 133 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 145 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 150 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 155 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 163 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 178 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 182 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 187 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 205 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 211 + }, + { + "file": "GIFT/Spectral/MassGapRatio.lean", + "line": 236 + }, + { + "file": "GIFT/Spectral/NeckGeometry.lean", + "line": 263 + }, + { + "file": "GIFT/Spectral/NeckGeometry.lean", + "line": 268 + }, + { + "file": "GIFT/Spectral/NeckGeometry.lean", + "line": 291 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 47 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 50 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 55 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 62 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 65 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 68 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 72 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 75 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 79 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 82 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 85 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 92 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 95 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 98 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 101 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 104 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 114 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 120 + }, + { + "file": "GIFT/Spectral/OctonionMassGap.lean", + "line": 145 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 84 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 95 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 100 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 103 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 106 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 111 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 118 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 121 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 126 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 137 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 141 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 150 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 154 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 158 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 181 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 185 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 193 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 197 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 231 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 232 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 233 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 234 + }, + { + "file": "GIFT/Spectral/PhysicalSpectralGap.lean", + "line": 235 + }, + { + "file": "GIFT/Spectral/RefinedSpectralBounds.lean", + "line": 363 + }, + { + "file": "GIFT/Spectral/RefinedSpectralBounds.lean", + "line": 372 + }, + { + "file": "GIFT/Spectral/RefinedSpectralBounds.lean", + "line": 388 + }, + { + "file": "GIFT/Spectral/SelectionPrinciple.lean", + "line": 329 + }, + { + "file": "GIFT/Spectral/SelectionPrinciple.lean", + "line": 394 + }, + { + "file": "GIFT/Spectral/SpectralDemocracy.lean", + "line": 72 + }, + { + "file": "GIFT/Spectral/SpectralDemocracy.lean", + "line": 78 + }, + { + "file": "GIFT/Spectral/SpectralDemocracy.lean", + "line": 81 + }, + { + "file": "GIFT/Spectral/SpectralDemocracy.lean", + "line": 86 + }, + { + "file": "GIFT/Spectral/SpectralDemocracy.lean", + "line": 95 + }, + { + "file": "GIFT/Spectral/SpectralDemocracy.lean", + "line": 99 + }, + { + "file": "GIFT/Spectral/SpectralDemocracy.lean", + "line": 116 + }, + { + "file": "GIFT/Spectral/SpectralDemocracy.lean", + "line": 119 + }, + { + "file": "GIFT/Spectral/SpectralDemocracy.lean", + "line": 149 + }, + { + "file": "GIFT/Spectral/SpectralInvariants.lean", + "line": 63 + }, + { + "file": "GIFT/Spectral/SpectralInvariants.lean", + "line": 67 + }, + { + "file": "GIFT/Spectral/SpectralInvariants.lean", + "line": 104 + }, + { + "file": "GIFT/Spectral/SpectralInvariants.lean", + "line": 107 + }, + { + "file": "GIFT/Spectral/SpectralInvariants.lean", + "line": 158 + }, + { + "file": "GIFT/Spectral/SpectralInvariants.lean", + "line": 161 + }, + { + "file": "GIFT/Spectral/SpectralInvariants.lean", + "line": 165 + }, + { + "file": "GIFT/Spectral/SpectralInvariants.lean", + "line": 169 + }, + { + "file": "GIFT/Spectral/SpectralInvariants.lean", + "line": 203 + }, + { + "file": "GIFT/Spectral/SpectralInvariants.lean", + "line": 209 + }, + { + "file": "GIFT/Spectral/SpectralInvariants.lean", + "line": 231 + }, + { + "file": "GIFT/Spectral/SpectralInvariants.lean", + "line": 234 + }, + { + "file": "GIFT/Spectral/SpectralInvariants.lean", + "line": 270 + }, + { + "file": "GIFT/Spectral/TCSBounds.lean", + "line": 309 + }, + { + "file": "GIFT/Spectral/TCSBounds.lean", + "line": 317 + }, + { + "file": "GIFT/Spectral/TCSBounds.lean", + "line": 335 + }, + { + "file": "GIFT/Spectral/TCSBounds.lean", + "line": 357 + }, + { + "file": "GIFT/Spectral/UniversalLaw.lean", + "line": 104 + }, + { + "file": "GIFT/Spectral/UniversalLaw.lean", + "line": 108 + }, + { + "file": "GIFT/Spectral/UniversalLaw.lean", + "line": 113 + }, + { + "file": "GIFT/Spectral/UniversalLaw.lean", + "line": 141 + }, + { + "file": "GIFT/Spectral/UniversalLaw.lean", + "line": 156 + }, + { + "file": "GIFT/Spectral/UniversalLaw.lean", + "line": 160 + }, + { + "file": "GIFT/Spectral/UniversalLaw.lean", + "line": 202 + }, + { + "file": "GIFT/Spectral/UniversalLaw.lean", + "line": 203 + }, + { + "file": "GIFT/Spectral/UniversalLaw.lean", + "line": 204 + }, + { + "file": "GIFT/Spectral/UniversalLaw.lean", + "line": 205 + }, + { + "file": "GIFT/Spectral/UniversalLaw.lean", + "line": 206 + }, + { + "file": "GIFT/Spectral/YangMills.lean", + "line": 280 + }, + { + "file": "GIFT/Spectral/YangMills.lean", + "line": 303 + }, + { + "file": "GIFT/Spectral/YangMills.lean", + "line": 314 + }, + { + "file": "GIFT/Spectral/YangMills.lean", + "line": 337 + } + ], + "holes": [] +} diff --git a/lake-manifest.json b/lake-manifest.json index 505dd352..cdb518d0 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,24 +1,24 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "5e932f97dd25535344f80f9dd8da3aab83df0fe6", + "rev": "0df444a360eaa60ab8c11dca51a86af692955474", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.1", + "inputRev": "v4.33.1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, "scope": "", - "rev": "a0aebd77a6619214a727994fade0e05203fc5252", + "rev": "e2af49a7b7e5e1a9224008c1f15e7aa4f58a4015", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.1", + "inputRev": "v4.33.1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/PatrickMassot/checkdecls.git", @@ -28,14 +28,14 @@ "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4", "name": "checkdecls", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3", + "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "48d5698bc464786347c1b0d859b18f938420f060", + "rev": "16f02aa7642864af59f1ff0e384a015994db9118", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,17 +65,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4dd0959c44d1af0462bd604d0f87c5781307d709", + "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.95+lean-v4.29.1", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7152850e7b216a0d409701617721b6e469d34bf6", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d", + "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -95,37 +95,37 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "756e3321fd3b02a85ffda19fef789916223e578c", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/leanprover/leansqlite", "type": "git", "subDir": null, - "scope": "leanprover", - "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", - "name": "Cli", + "scope": "", + "rev": "6168b7549738a19bc837a1625c60c5d1e5dd8aeb", + "name": "leansqlite", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", + "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/kim-em/leansqlite", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "scope": "", - "rev": "d14544c72b593af6a66131bc34cdab16bf7c0940", - "name": "leansqlite", + "scope": "leanprover", + "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "suppress-reducibility-warning", + "inputRev": "v4.33.0", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, "scope": "", - "rev": "9539e34e5cb2d52a6454d9b6218f6b6835cad071", + "rev": "37e7d8cb7316a88cd3e91208385c9ec6ae780019", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -135,21 +135,22 @@ "type": "git", "subDir": null, "scope": "", - "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "rev": "852edafa268eb038a7158551fd580ee8433847b0", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, "scope": "", - "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", + "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}], "name": "GIFT", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.lean b/lakefile.lean index 59e1e9d8..f40668d5 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,13 +4,13 @@ open Lake DSL package «GIFT» require checkdecls from git - "https://github.com/PatrickMassot/checkdecls.git" @ "master" + "https://github.com/PatrickMassot/checkdecls.git" @ "3d425859e73fcfbef85b9638c2a91708ef4a22d4" require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "v4.29.1" + "https://github.com/leanprover/doc-gen4" @ "v4.33.1" require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ "v4.29.1" + "https://github.com/leanprover-community/mathlib4.git" @ "v4.33.1" @[default_target] lean_lib «GIFT» where @@ -24,3 +24,6 @@ lean_lib «GIFT» where lean_lib «GIFTTest» where globs := #[.submodules `GIFTTest] + +lean_lib «Verification» where + globs := #[.submodules `Verification] diff --git a/lean-toolchain b/lean-toolchain index 33e0c088..a8afa7d1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.1 +leanprover/lean4:v4.33.1 diff --git a/scripts/local_ci.sh b/scripts/local_ci.sh index acf45d0a..bc79c464 100755 --- a/scripts/local_ci.sh +++ b/scripts/local_ci.sh @@ -75,8 +75,8 @@ consistency_check() { local ERRORS=0 - if ! grep -q "GIFT Core v${VERSION}" README.md; then - red " ✗ README.md does NOT contain 'GIFT Core v${VERSION}'" + if ! grep -q "K₇-Lean v${VERSION}" README.md; then + red " ✗ README.md does NOT contain 'K₇-Lean v${VERSION}'" ERRORS=$((ERRORS+1)) else echo " ✓ README.md mentions v${VERSION}" @@ -107,18 +107,7 @@ consistency_check() { # Mirrors verify-consistency.yml step "Check no sorry in Lean files" # ---------------------------------------------------------------------- sorry_check() { - # Match the workflow's filter logic exactly - local hits - hits=$(grep -rn "sorry" GIFT/ GIFTTest/ --include="*.lean" 2>/dev/null \ - | grep -v "^.*:.*--.*sorry" \ - | grep -v "REMOVED\|eliminated\|no.*sorry\|zero.*sorry\|all goals closed" || true) - if [ -n "$hits" ]; then - red " Found 'sorry' in:" - echo "$hits" | sed 's/^/ /' - return 1 - fi - echo " ✓ Zero sorry across $(find GIFT/ -name '*.lean' 2>/dev/null | wc -l) Lean files" - return 0 + python3 scripts/proof_inventory.py --check } # ---------------------------------------------------------------------- @@ -161,8 +150,7 @@ blueprint_check() { lake_build_check() { yellow " ⚠ Running 'lake build'. This can take several minutes and" yellow " may stress your laptop. Press Ctrl+C now to abort." - sleep 3 - lake build + lake build && lake build Verification return $? } diff --git a/scripts/proof_inventory.py b/scripts/proof_inventory.py new file mode 100644 index 00000000..1c019087 --- /dev/null +++ b/scripts/proof_inventory.py @@ -0,0 +1,66 @@ +#!/usr/bin/env python3 +"""Source inventory, not a substitute for Lean's transitive axiom audit.""" +import argparse +import json +import re +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] + +def code_only(text): + """Blank nested Lean comments and strings, retaining positions and newlines.""" + out = list(text) + i, depth, string = 0, 0, False + while i < len(text): + if depth: + if text.startswith('/-', i): + out[i:i+2] = ' '; depth += 1; i += 2; continue + if text.startswith('-/', i): + out[i:i+2] = ' '; depth -= 1; i += 2; continue + if text[i] != '\n': out[i] = ' ' + elif string: + if text[i] == '\\' and i + 1 < len(text): + out[i:i+2] = ' '; i += 2; continue + if text[i] == '"': string = False + if text[i] != '\n': out[i] = ' ' + elif text.startswith('/-', i): + out[i:i+2] = ' '; depth = 1; i += 2; continue + elif text.startswith('--', i): + end = text.find('\n', i) + if end < 0: end = len(text) + out[i:end] = ' ' * (end-i); i = end; continue + elif text[i] == '"': + out[i] = ' '; string = True + i += 1 + if depth or string: + raise ValueError('Unterminated comment or string') + return ''.join(out) + +def inventory(): + files = sorted([ROOT/'GIFT.lean', *ROOT.glob('GIFT/**/*.lean')]) + result = {'lean_files': len(files), 'axiom_declarations': [], 'native_decide': [], 'holes': []} + for f in files: + code = code_only(f.read_text()) + for kind, pattern in [('axiom_declarations', r'\baxiom\s+([^\s:(]+)'), + ('native_decide', r'\bnative_decide\b'), + ('holes', r'\b(?:sorry|admit|sorryAx)\b')]: + for m in re.finditer(pattern, code): + row = {'file': str(f.relative_to(ROOT)), 'line': code[:m.start()].count('\n')+1} + if kind == 'axiom_declarations': row['name'] = m.group(1) + result[kind].append(row) + return result + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', type=Path) + parser.add_argument('--check', action='store_true') + args = parser.parse_args() + result = inventory() + if args.write: + args.write.parent.mkdir(parents=True, exist_ok=True) + args.write.write_text(json.dumps(result, indent=2)+'\n') + print(json.dumps({k: len(v) if isinstance(v, list) else v for k,v in result.items()}, sort_keys=True)) + if args.check and result['holes']: + raise SystemExit('Unfinished proofs in library sources: '+str(result['holes'])) + +if __name__ == '__main__': main() diff --git a/scripts/test_proof_inventory.py b/scripts/test_proof_inventory.py new file mode 100644 index 00000000..0eb82726 --- /dev/null +++ b/scripts/test_proof_inventory.py @@ -0,0 +1,20 @@ +import unittest +from proof_inventory import code_only + +class LeanLexing(unittest.TestCase): + def test_nested_comments_and_strings(self): + source = '/- sorry /- admit -/ sorry -/\ntheorem t : True := by\n trivial -- sorry\n#check "sorry \\" admit"\n' + code = code_only(source) + self.assertEqual(len(source), len(code)) + self.assertEqual(source.count('\n'), code.count('\n')) + self.assertNotIn('sorry', code) + self.assertNotIn('admit', code) + self.assertIn('trivial', code) + + def test_real_hole_survives_inline_comment(self): + self.assertIn('sorry', code_only('theorem t : False := by sorry -- no sorry')) + + def test_unterminated_comment(self): + with self.assertRaises(ValueError): code_only('/- unfinished') + +if __name__ == '__main__': unittest.main() diff --git a/scripts/update_verification_imports.py b/scripts/update_verification_imports.py new file mode 100644 index 00000000..d0ed0655 --- /dev/null +++ b/scripts/update_verification_imports.py @@ -0,0 +1,17 @@ +#!/usr/bin/env python3 +"""Keep the audit's import closure equal to the complete library source tree.""" +from pathlib import Path +import argparse +ROOT = Path(__file__).resolve().parents[1] +p = argparse.ArgumentParser() +p.add_argument('--check', action='store_true') +args = p.parse_args() +text = '-- Generated by scripts/update_verification_imports.py.\n' + ''.join( + 'import ' + str(f.relative_to(ROOT).with_suffix('')).replace('/', '.') + '\n' + for f in sorted((ROOT/'GIFT').rglob('*.lean'))) +out = ROOT/'Verification/AllImports.lean' +if args.check: + if not out.exists() or out.read_text() != text: + raise SystemExit('Run python3 scripts/update_verification_imports.py') +else: + out.write_text(text)