Uhlig's two-copy recovery code

This file formalizes the exact combinatorial core of the section "The two-copy construction as disjoint recovery" in the Boolean mass-production manuscript.

For a nonempty family f_0, ..., f_last, the resource family is

• g_0 = f_0,
• g_j = f_(j - 1) + f_j at an interior boundary, and
• g_(last + 1) = f_last.

Addition is kept abstract. The recovery proof assumes explicitly that every element is self-inverse, rather than introducing a typeclass instance. For Boolean-valued functions, Mathlib's existing Boolean-ring addition is XOR.

Each target has a prefix and a suffix recovery set. The file proves both recovery identities, proves the relevant sets disjoint for ordered requests, and packages the comparator choice for requests arriving in either order.

def Algebraic.MassProduction.uhligResource {A : Type u_1} {last : ℕ} [Add A] (values : Fin (last + 1) → A) : Fin (last + 2) → A

The last + 2 resource values associated with last + 1 source values. The parameter is the final source index, so the family is nonempty without a separate positivity assumption.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.uhligResource_zero {A : Type u_1} {last : ℕ} [Add A] (values : Fin (last + 1) → A) : uhligResource values 0 = values 0

theorem Algebraic.MassProduction.uhligResource_interior {A : Type u_1} {last : ℕ} [Add A] (values : Fin (last + 1) → A) (index : Fin last) : uhligResource values index.succ.castSucc = values index.castSucc + values index.succ

@[simp]

theorem Algebraic.MassProduction.uhligResource_last {A : Type u_1} {last : ℕ} [Add A] (values : Fin (last + 1) → A) : uhligResource values (Fin.last (last + 1)) = values (Fin.last last)

def Algebraic.MassProduction.uhligPrefixSet {last : ℕ} (target : Fin (last + 1)) : Finset (Fin (last + 2))

The prefix representation of one source coordinate.

Equations

• Algebraic.MassProduction.uhligPrefixSet target = Finset.Iic target.castSucc

def Algebraic.MassProduction.uhligSuffixSet {last : ℕ} (target : Fin (last + 1)) : Finset (Fin (last + 2))

The suffix representation of one source coordinate.

Equations

• Algebraic.MassProduction.uhligSuffixSet target = Finset.Ioi target.castSucc

@[simp]

theorem Algebraic.MassProduction.mem_uhligPrefixSet {last : ℕ} (resource : Fin (last + 2)) (target : Fin (last + 1)) : resource ∈ uhligPrefixSet target ↔ ↑resource ≤ ↑target

@[simp]

theorem Algebraic.MassProduction.mem_uhligSuffixSet {last : ℕ} (resource : Fin (last + 2)) (target : Fin (last + 1)) : resource ∈ uhligSuffixSet target ↔ ↑target < ↑resource

theorem Algebraic.MassProduction.uhligPrefixSet_disjoint_uhligSuffixSet {last : ℕ} {left right : Fin (last + 1)} (ordered : left ≤ right) : Disjoint (uhligPrefixSet left) (uhligSuffixSet right)

A prefix through left is disjoint from a suffix strictly after right whenever left <= right. This is the scheduling invariant in Uhlig's two-copy construction.

theorem Algebraic.MassProduction.sum_uhligPrefixSet {A : Type u_1} {last : ℕ} [AddCommMonoid A] (selfAdd : ∀ (value : A), value + value = 0) (values : Fin (last + 1) → A) (target : Fin (last + 1)) : ∑ resource ∈ uhligPrefixSet target, uhligResource values resource = values target

Prefix recovery telescopes to the requested value in any commutative additive monoid in which every element is self-inverse.

theorem Algebraic.MassProduction.sum_uhligResource_eq_zero {A : Type u_1} {last : ℕ} [AddCommMonoid A] (selfAdd : ∀ (value : A), value + value = 0) (values : Fin (last + 1) → A) : ∑ resource : Fin (last + 2), uhligResource values resource = 0

The XOR-like sum of all resources is zero.

theorem Algebraic.MassProduction.sum_uhligSuffixSet {A : Type u_1} {last : ℕ} [AddCommMonoid A] (selfAdd : ∀ (value : A), value + value = 0) (values : Fin (last + 1) → A) (target : Fin (last + 1)) : ∑ resource ∈ uhligSuffixSet target, uhligResource values resource = values target

Suffix recovery also telescopes to the requested value.

def Algebraic.MassProduction.uhligRecoveryPair {last : ℕ} (first second : Fin (last + 1)) : Finset (Fin (last + 2)) × Finset (Fin (last + 2))

Recovery sets chosen for two requests in their arrival order. The lower request uses a prefix and the higher request uses a suffix; in the opposite arrival order the two branches are swapped.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.MassProduction.uhligRecoveryPair_disjoint {last : ℕ} (first second : Fin (last + 1)) : Disjoint (uhligRecoveryPair first second).1 (uhligRecoveryPair first second).2

The recovery sets selected for any two requests are disjoint.

theorem Algebraic.MassProduction.uhligRecoveryPair_recovers {A : Type u_1} {last : ℕ} [AddCommMonoid A] (selfAdd : ∀ (value : A), value + value = 0) (values : Fin (last + 1) → A) (first second : Fin (last + 1)) : ∑ resource ∈ (uhligRecoveryPair first second).1, uhligResource values resource = values first ∧ ∑ resource ∈ (uhligRecoveryPair first second).2, uhligResource values resource = values second

Both sets selected by uhligRecoveryPair recover their corresponding requests, in the original arrival order.

theorem Algebraic.MassProduction.uhlig_two_copy_disjoint_recovery {A : Type u_1} {last : ℕ} [AddCommMonoid A] (selfAdd : ∀ (value : A), value + value = 0) (values : Fin (last + 1) → A) (first second : Fin (last + 1)) : Disjoint (uhligRecoveryPair first second).1 (uhligRecoveryPair first second).2 ∧ ∑ resource ∈ (uhligRecoveryPair first second).1, uhligResource values resource = values first ∧ ∑ resource ∈ (uhligRecoveryPair first second).2, uhligResource values resource = values second

Uhlig's complete two-request invariant: the selected representations are resource-disjoint and recover both requested values.

theorem Algebraic.MassProduction.uhligBoolean_two_copy_disjoint_recovery {last : ℕ} {Z : Type u_1} (values : Fin (last + 1) → Z → Bool) (first second : Fin (last + 1)) : Disjoint (uhligRecoveryPair first second).1 (uhligRecoveryPair first second).2 ∧ ∑ resource ∈ (uhligRecoveryPair first second).1, uhligResource values resource = values first ∧ ∑ resource ∈ (uhligRecoveryPair first second).2, uhligResource values resource = values second

Function-valued Boolean specialization. Here resource addition is pointwise XOR, exactly as in the manuscript.