Lax Lean Archive

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

The benchmark ladder

Lax771644.Foundations · concepts/Lax771644/Foundations.lean · lax-771644

definition

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

    Definition

    Every claim in this submission is a rung of one ladder: for natural numbers aa and bb, the assertion that divisibility by 2a2^a implies divisibility by 2b2^b. The mathematics is deliberately trivial. It exists only so that this submission's dependency graph can be wired into any shape at all while every proof still genuinely applies the statements it declares as assumptions.

    Concept map
    1 concept; 27 descendants hidden
    100%
    Proven claimOpen claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Data.Nat.Notation
    2
    3/-!
    4---
    5title: The benchmark ladder
    6type: definition
    7---
    8Every claim in this submission is a rung of one ladder: for natural numbers
    9aa and bb, the assertion that divisibility by 2a2^a implies divisibility by
    102b2^b. The mathematics is deliberately trivial. It exists only so that this
    11submission's *dependency graph* can be wired into any shape at all while every
    12proof still genuinely applies the statements it declares as assumptions.
    13
    14# Formalization notes
    15
    16`Stage k n` is plain divisibility, `2 ^ k ∣ n`, and `Descent a b` is the
    17statement shape every axiom of this submission uses. Because `Descent a b`
    18holds whenever `b ≤ a`, a proof of one rung can be assembled from *any*
    19descending sequence of other rungs. That is what lets the proof network of this
    20submission take on arbitrary shapes — long chains, cycles, wide fans — without
    21any statement being false or any proof pretending to use an assumption it does
    22not.
    23-/
    24
    25namespace Lax771644.Foundations
    26
    27/-- `Stage k n` says that `n` is divisible by `2 ^ k`. -/
    28def Stage (k n : ℕ) : Prop := 2 ^ k ∣ n
    29
    30/-- `Descent a b` is the one statement shape this submission uses: every natural
    31number divisible by `2 ^ a` is divisible by `2 ^ b`. -/
    32def Descent (a b : ℕ) : Prop := ∀ n : ℕ, Stage a n → Stage b n
    33
    34end Lax771644.Foundations
    35
    Formalization notes

    StageknStage k n is plain divisibility, 2k∣n2 ^ k ∣ n, and DescentabDescent a b is the statement shape every axiom of this submission uses. Because DescentabDescent a b holds whenever b≤ab ≤ a, a proof of one rung can be assembled from any descending sequence of other rungs. That is what lets the proof network of this submission take on arbitrary shapes — long chains, cycles, wide fans — without any statement being false or any proof pretending to use an assumption it does not.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…