FormalConjectures/Arxiv/1601.03081/UniqueCrystalComponents.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

3 declarations, 1 contain sorry, 0 declared as axioms

Unique Crystal Components

Reference: arxiv/1601.03081 The Biharmonic mean by Marco Abrate, Stefano Barbero, Umberto Cerruti, Nadir Murru

Imports (1)
Imported by 1 file
  1. def Arxiv.«1601.03081».IsCrystalWithComponents An odd number $n$ is called a crystal if $n = ab$, with $a, b > 1$ and $B(a, b) ∈ ℕ$, where $B(a, b) := ((a + b)^2 + (a b + 1)^2) / (2 (a + 1) (b + 1))$ line 36 source

    Source documentation

    An odd number $n$ is called a crystal if $n = ab$, with $a, b > 1$ and $B(a, b) ∈ ℕ$, where $B(a, b) := ((a + b)^2 + (a b + 1)^2) / (2 (a + 1) (b + 1))$.

    standard axioms: propext what this means

    Statement uses: Nat

    Proof uses: And, Odd, LT.lt, OfNat.ofNat, Eq, HMul.hMul, Dvd.dvd, HAdd.hAdd, HPow.hPow

    12 instances, coercions and auxiliary constants left out.

    def IsCrystalWithComponents (n a b : ℕ) : Prop :=
…
  2. theorem Arxiv.«1601.03081».isCrystalWithComponents_35_5_7 line 40 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Arxiv.«1601.03081».IsCrystalWithComponents, OfNat.ofNat, Nat

    Proof uses: of_eq_true, And, Odd, LT.lt, Eq, HMul.hMul, Dvd.dvd, HAdd.hAdd, HPow.hPow, Eq.trans, True, congr, congrArg, eq_true, Iff.mp, HMod.hMod, Bool.rec, Bool, Not, Bool.true and 16 more

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  3. theorem Arxiv.«1601.03081».crystals_components_unique Documented declaration: crystals_components_unique sorry line 51 source

    Source documentation

    If $n = ab$ is a crystal, then there are no other pairs of positive integers $c, d > 1$, different from the couple $a, b$, such that $n = cd$ and $B(c, d) ∈ ℕ$, i.e., the components of the crystals are unique.

    depends on sorry what this means

    Statement uses: Nat, Arxiv.«1601.03081».IsCrystalWithComponents, Eq, Finset, Insert.insert, Singleton.singleton

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem crystals_components_unique (n a b c d : ℕ)
    (hab : IsCrystalWithComponents n a b) (hcd : IsCrystalWithComponents n c d) :
    ({a, b} : Finset ℕ) = {c, d} := by
…

    Mentions: c, Arxiv.«1601.03081».IsCrystalWithComponents