Lax Lean Archive

The Deterministic Seed Search Succeeds

Lax920634.SeedCorrectness · concepts/Lax920634/SeedCorrectness.lean · lax-920634

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

    Lemma

    At every finite order the deterministic table scan finds thirty permutations such that, for every set of at most half the vertices, some permutation moves at least a tenth of that set outside itself.

    Concept map
    2 concepts
    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

    1import Lax920634.SeedSearch
    2
    3/-!
    4---
    5title: The Deterministic Seed Search Succeeds
    6type: lemma
    7---
    8At every finite order the deterministic table scan finds thirty permutations
    9such that, for every set of at most half the vertices, some permutation
    10moves at least a tenth of that set outside itself.
    11
    12# Formalization notes
    13
    14The scan checks this exact decidable property. A finite counting argument
    15proves that a successful candidate exists, and numerical enumeration covers
    16every candidate. The total default in the constructor is never needed.
    17-/
    18
    19namespace Lax920634.SeedCorrectness
    20
    21open SeedSearch
    22
    23/-- The specified finite seed search returns a successful permutation table. -/
    24axiom table_good (n : ℕ) : GoodTable (selectedTable n)
    25
    26end Lax920634.SeedCorrectness
    27
    Show Proof
    Formalization notes

    The scan checks this exact decidable property. A finite counting argument proves that a successful candidate exists, and numerical enumeration covers every candidate. The total default in the constructor is never needed.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…