Lax Lean Archive

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

Consistent symmetric binary prescriptions on two witness lists

Lax342547.SymmetricPrescriptions · concepts/Lax342547/SymmetricPrescriptions.lean · lax-342547

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

    The two lists are nonempty and disjoint, represented by a sum type. Prescribed list sums of every row of a symmetric binary matrix are compatible with its fixed diagonal precisely through the two self-sum conditions and the equality of the cross totals. The sufficiency proof constructs the matrix explicitly.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1 diagonal_rows proven

    2 rectangular_sums proven

    3 two_lists proven

    Lean source view on GitHub

    1import Lax342547.MomentSpace
    2import Mathlib.Data.Matrix.Block
    3
    4/-!
    5---
    6title: Consistent symmetric binary prescriptions on two witness lists
    7type: theorem
    8---
    9The two lists are nonempty and disjoint, represented by a sum type.
    10Prescribed list sums of every row of a symmetric binary matrix are
    11compatible with its fixed diagonal precisely through the two self-sum
    12conditions and the equality of the cross totals. The sufficiency proof
    13constructs the matrix explicitly.
    14-/
    15
    16namespace Lax342547.SymmetricPrescriptions
    17
    18open Lax342547.MomentSpace
    19
    20axiom diagonal_rows {I : Type} [Fintype I] [Nonempty I]
    21 (a c : I → Binary) (h : ∑ i, c i = ∑ i, a i) :
    22 ∃ M : Matrix I I Binary, (∀ i j, M i j = M j i) ∧
    23 (∀ i, M i i = a i) ∧ ∀ i, ∑ j, M i j = c i
    24
    25axiom rectangular_sums {I J : Type} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J]
    26 (r : I → Binary) (c : J → Binary) (h : ∑ i, r i = ∑ j, c j) :
    27 ∃ M : Matrix I J Binary, (∀ i, ∑ j, M i j = r i) ∧ ∀ j, ∑ i, M i j = c j
    28
    29axiom two_lists {I J : Type} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J]
    30 (a c₁ c₂ : I ⊕ J → Binary)
    31 (h₁ : ∑ i : I, c₁ (Sum.inl i) = ∑ i : I, a (Sum.inl i))
    32 (h₂ : ∑ j : J, c₂ (Sum.inr j) = ∑ j : J, a (Sum.inr j))
    33 (hcross : ∑ i : I, c₂ (Sum.inl i) = ∑ j : J, c₁ (Sum.inr j)) :
    34 ∃ M : Matrix (I ⊕ J) (I ⊕ J) Binary, (∀ x y, M x y = M y x) ∧
    35 (∀ x, M x x = a x) ∧ (∀ x, ∑ i : I, M x (Sum.inl i) = c₁ x) ∧
    36 ∀ x, ∑ j : J, M x (Sum.inr j) = c₂ x
    37
    38end Lax342547.SymmetricPrescriptions
    39
    Show ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…