GraphCompletionUnique.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness of the actual forest completion

A homogeneous real table supported on an acyclic row/column graph, with zero sums at every nonroot vertex, vanishes. The proof constructs an actual root-away deletion cut for each tree cell and isolates that cell in the signed margin sum. Thus the integral root-path construction is the unique integral completion, without a leaf-order encoding input.

theorem OAI.ContingencyTables.GraphCompletionUnique.zero_of_nonroot_sums line 25

Source documentation

This is the nonsingular forest-incidence assertion needed by the companion's tree-coordinate sum, over the reals as well as the integers.

theorem zero_of_nonroot_sums (T : SimpleGraph (I⊕J))
    (hT : T.IsAcyclic) (z : I → J → ℝ)
    (hsupport : ∀ i j, ¬T.Adj (.inl i) (.inr j) → z i j=0)
    (hr : ∀ i, Sum.inl i≠componentRoot T (.inl i) → (∑ j, z i j)=0)
    (hc : ∀ j, Sum.inr j≠componentRoot T (.inr j) → (∑ i, z i j)=0) :
    ∀ i j, z i j=0 := by
…

theorem OAI.ContingencyTables.GraphCompletionUnique.tableCompletion_unique line 85

Source documentation

The explicit integral root-path solution has no hidden multiplicity: every integral table supported on the tree and satisfying its nonroot margin equations equals that solution.

theorem tableCompletion_unique (small : I → J → Bool) (T : SimpleGraph (I⊕J))
    (hTG : T≤cellGraph small) (hT : T.IsAcyclic)
    (r : I → ℤ) (c : J → ℤ) (z : I → J → ℤ)
    (hsupport : ∀ i j, ¬T.Adj (.inl i) (.inr j) → z i j=0)
    (hr : ∀ i, Sum.inl i≠componentRoot T (.inl i) → (∑ j, z i j)=r i)
    (hc : ∀ j, Sum.inr j≠componentRoot T (.inr j) → (∑ i, z i j)=c j) :
    z=tableCompletion T r c := by
…

theorem OAI.ContingencyTables.GraphCompletionUnique.exists_unique_integral_completion line 110