Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Truly subcubic Exact Triangle

Lax350013.ExactTriangle · concepts/Lax350013/ExactTriangle.lean · lax-350013

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Exact Triangle on a complete tripartite graph with nn vertices in each part and polynomially bounded integer weights is decidable deterministically in O(n2.9983)O(n^{2.9983}) word-RAM steps (Theorem 19). A triangle is accepted exactly when its three edge weights sum to zero.

    Concept map
    3 concepts; 4 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1/-
    2Copyright (c) 2026 Anthropic, PBC. All rights reserved.
    3Released under Apache 2.0 license as described in the file LICENSE.
    4SPDX-License-Identifier: Apache-2.0
    5-/
    6/-
    7Modified for the independent Lax packaging by Édouard Bonnet, 2026.
    8Derived from 3sum-apsp/EndStatement.lean / PaperStatements.lean at upstream commit e1a4e6508154ea59f030480661590a9fe3018011.
    9Changes: Lax module/namespace layout, separated concepts and proofs, archive
    10annotations, and compatibility with the archive Lean/mathlib environment.
    11See NOTICE and README.md in the submission root for provenance and scope.
    12-/
    13
    14import Lax350013.PolynomialTime
    15
    16/-!
    17---
    18title: Truly subcubic Exact Triangle
    19type: theorem
    20---
    21Exact Triangle on a complete tripartite graph with nn vertices in each part and polynomially bounded integer weights is decidable deterministically in O(n2.9983)O(n^{2.9983}) word-RAM steps (Theorem 19). A triangle is accepted exactly when its three edge weights sum to zero.
    22-/
    23
    24namespace Lax350013.ExactTriangle
    25
    26open Lax350013.PolynomialTime
    27
    28/-- Section 3.2: «S(a, b, c) := w(a, b) + w(b, c) + w(a, c). A zero triangle is a triangle … with S(a, b, c) = 0». -/
    29def ExactTriangle : Problem where
    30 Instance n := (Fin n → Fin n → Int) × (Fin n → Fin n → Int) × (Fin n → Fin n → Int)
    31 input := fun (wAB, wBC, wAC) => rowByRow wAB ++ rowByRow wBC ++ rowByRow wAC
    32 yes := fun (wAB, wBC, wAC) => ∃ a b c, wAB a b + wBC b c + wAC a c = 0
    33
    34/-- Theorem 19: «ε_T := 0.0017». -/
    35def ε_T : Rat := 0.0017
    36
    37/-- Theorem 19: «Exact Triangle … can be solved by a deterministic algorithm in … O(n^(3−ε_T)) time». -/
    38def Theorem_19 : Prop :=
    39 ExactTriangle.SolvedInTime (3 - ε_T)
    40
    41/-- Truly subcubic Exact Triangle: Theorem 19. -/
    42axiom algorithm : Theorem_19
    43
    44end Lax350013.ExactTriangle
    45
    Show Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…