From unit relations to consecutive subset-sum gaps

This file supplies the elementary order-theoretic bridge between the Conway--Guy unit-relation certificates and consecutive gaps in the coherent Boolean term order induced by the Conway--Guy weights.

Tom Bohman's 1996 theorem that the Conway--Guy rows have distinct subset sums is still an external input if one wants the induced comparison to be a total order. The bridge itself only uses integrality: two subset sums differing by one have no integer subset sum strictly between them.

def BooleanIsoperimetry.CoherentGap.integerSubsetWeight {n : ℕ} (weights : Relation n) (vertex : Cube n) : ℤ

The integer weight of a Boolean-cube vertex.

Equations

• BooleanIsoperimetry.CoherentGap.integerSubsetWeight weights vertex = ∑ coordinate ∈ vertex, weights coordinate

def BooleanIsoperimetry.CoherentGap.realSubsetWeight {n : ℕ} (weights : Fin n → ℝ) (vertex : Cube n) : ℝ

The real weight of a Boolean-cube vertex.

Equations

• BooleanIsoperimetry.CoherentGap.realSubsetWeight weights vertex = ∑ coordinate ∈ vertex, weights coordinate

def BooleanIsoperimetry.CoherentGap.positiveSupport {n : ℕ} (relation : Relation n) : Cube n

Coordinates with coefficient one in a signed relation.

Equations

• BooleanIsoperimetry.CoherentGap.positiveSupport relation = {coordinate : Fin n | relation coordinate = 1}

def BooleanIsoperimetry.CoherentGap.negativeSupport {n : ℕ} (relation : Relation n) : Cube n

Coordinates with coefficient minus one in a signed relation.

Equations

• BooleanIsoperimetry.CoherentGap.negativeSupport relation = {coordinate : Fin n | relation coordinate = -1}

def BooleanIsoperimetry.CoherentGap.IsConsecutiveSubsetGap {n : ℕ} (weights : Relation n) (lower upper : Cube n) : Prop

No subset sum lies strictly between the weights of lower and upper.

Equations

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

def BooleanIsoperimetry.CoherentGap.SatisfiesNormalizedConsecutiveGaps {n : ℕ} (reference : Relation n) (candidate : Fin n → ℝ) : Prop

Every consecutive gap of a reference integer row has size at least one when measured by the candidate real row.

Equations

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

theorem BooleanIsoperimetry.CoherentGap.dot_eq_support_difference {n : ℕ} (weights relation : Relation n) (hvalues : ∀ (coordinate : Fin n), relation coordinate = -1 ∨ relation coordinate = 0 ∨ relation coordinate = 1) : dot relation weights = integerSubsetWeight weights (positiveSupport relation) - integerSubsetWeight weights (negativeSupport relation)

theorem BooleanIsoperimetry.CoherentGap.realDot_eq_support_difference {n : ℕ} (candidate : Fin n → ℝ) (relation : Relation n) (hvalues : ∀ (coordinate : Fin n), relation coordinate = -1 ∨ relation coordinate = 0 ∨ relation coordinate = 1) : realDot relation candidate = realSubsetWeight candidate (positiveSupport relation) - realSubsetWeight candidate (negativeSupport relation)

theorem BooleanIsoperimetry.CoherentGap.unitRelation_support_gap {n : ℕ} {weights relation : Relation n} (hrelation : IsLiftableUnit weights relation) : integerSubsetWeight weights (positiveSupport relation) = integerSubsetWeight weights (negativeSupport relation) + 1

A unit relation is realized by two subsets whose integer weights differ by exactly one.

theorem BooleanIsoperimetry.CoherentGap.consecutive_of_integer_gap_one {n : ℕ} {weights : Relation n} {lower upper : Cube n} (hgap : integerSubsetWeight weights upper = integerSubsetWeight weights lower + 1) : IsConsecutiveSubsetGap weights lower upper

Integrality alone makes every realized gap of size one consecutive.

theorem BooleanIsoperimetry.CoherentGap.unitRelation_isConsecutiveSubsetGap {n : ℕ} {weights relation : Relation n} (hrelation : IsLiftableUnit weights relation) : IsConsecutiveSubsetGap weights (negativeSupport relation) (positiveSupport relation)

Every liftable unit relation is a consecutive subset-sum gap.

theorem BooleanIsoperimetry.CoherentGap.normalizedConsecutiveGaps_imply_unitRelations {n : ℕ} {reference : Relation n} {candidate : Fin n → ℝ} (hnormalized : SatisfiesNormalizedConsecutiveGaps reference candidate) (relation : Relation n) : IsLiftableUnit reference relation → 1 ≤ realDot relation candidate

Normalized consecutive-gap inequalities imply all unit-relation inequalities used by the rigidity certificate.

theorem BooleanIsoperimetry.CoherentGap.conwayGuyRigidity_of_normalizedConsecutiveGaps {n : ℕ} (candidate : Fin n → ℝ) (hnormalized : SatisfiesNormalizedConsecutiveGaps (conwayGuyArithmetic.tower.weights n) candidate) (coordinate : Fin n) : ↑(conwayGuyArithmetic.tower.weights n coordinate) ≤ candidate coordinate

The Conway--Guy row is a coordinatewise lower bound for every real row with normalized consecutive gaps relative to its subset sums.

theorem BooleanIsoperimetry.conwayGuyGapRigidity {n : ℕ} (candidate : Fin n → ℝ) (hnormalized : CoherentGap.SatisfiesNormalizedConsecutiveGaps (CoherentGap.conwayGuyArithmetic.tower.weights n) candidate) (coordinate : Fin n) : ↑(CoherentGap.conwayGuyArithmetic.tower.weights n coordinate) ≤ candidate coordinate

Public short name for the all-dimensional Conway--Guy gap-rigidity theorem.