Conway--Guy coherent-gap data

This file instantiates the triangular correction pattern used by the Conway--Guy distinct-subset-sum sequence. The recurrence and notation follow Section 2 of Tom Bohman's 1996 paper on the Conway--Guy sequence.

def BooleanIsoperimetry.CoherentGap.triangular : ℕ → ℕ

The triangular numbers, indexed from zero.

Equations

• BooleanIsoperimetry.CoherentGap.triangular 0 = 0
• BooleanIsoperimetry.CoherentGap.triangular index.succ = BooleanIsoperimetry.CoherentGap.triangular index + index + 1

theorem BooleanIsoperimetry.CoherentGap.self_le_triangular (index : ℕ) : index ≤ triangular index

theorem BooleanIsoperimetry.CoherentGap.triangular_mono : Monotone triangular

theorem BooleanIsoperimetry.CoherentGap.triangular_strictMono : StrictMono triangular

theorem BooleanIsoperimetry.CoherentGap.triangular_add_index (index : ℕ) : triangular index + index + 1 = triangular (index + 1)

theorem BooleanIsoperimetry.CoherentGap.guideWitness (dimension : ℕ) : ∃ (width : ℕ), dimension - 1 ≤ triangular width

noncomputable def BooleanIsoperimetry.CoherentGap.guide (dimension : ℕ) : ℕ

The least triangular block containing dimension - 1.

Equations

• BooleanIsoperimetry.CoherentGap.guide dimension = Nat.find ⋯

theorem BooleanIsoperimetry.CoherentGap.guide_upper (dimension : ℕ) : dimension - 1 ≤ triangular (guide dimension)

theorem BooleanIsoperimetry.CoherentGap.guide_pos {dimension : ℕ} (hdimension : 2 ≤ dimension) : 0 < guide dimension

theorem BooleanIsoperimetry.CoherentGap.guide_lower {dimension : ℕ} (hdimension : 2 ≤ dimension) : triangular (guide dimension - 1) + 2 ≤ dimension

theorem BooleanIsoperimetry.CoherentGap.guide_le_dimension {dimension : ℕ} (hdimension : 2 ≤ dimension) : guide dimension ≤ dimension

theorem BooleanIsoperimetry.CoherentGap.correction_deep_bound {dimension index : ℕ} (hdimension : 2 ≤ dimension) (hindex : index < guide dimension - 1) : triangular index + index + 3 ≤ dimension

theorem BooleanIsoperimetry.CoherentGap.negative_index_ge_guide {dimension index : ℕ} (hdimension : 2 ≤ dimension) (hindex : index < guide dimension - 1) : guide dimension ≤ dimension - triangular index - 1

noncomputable def BooleanIsoperimetry.CoherentGap.positiveIndex (offset : ℕ) (index : Fin (guide (offset + 2))) : Fin (offset + 2)

The positive support of the Conway--Guy principal relation.

Equations

• BooleanIsoperimetry.CoherentGap.positiveIndex offset index = ⟨↑index, ⋯⟩

noncomputable def BooleanIsoperimetry.CoherentGap.negativeIndex (offset : ℕ) (index : Fin (guide (offset + 2) - 1)) : Fin (offset + 2)

The triangular negative support of the Conway--Guy principal relation.

Equations

• BooleanIsoperimetry.CoherentGap.negativeIndex offset index = ⟨offset + 2 - BooleanIsoperimetry.CoherentGap.triangular ↑index - 1, ⋯⟩

noncomputable def BooleanIsoperimetry.CoherentGap.correctionFor (offset : ℕ) (index : Fin (guide (offset + 2) - 1)) : Correction (offset + 2)

The smaller-dimensional certificate lift cancelling one negative support coordinate of the principal relation.

Equations

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

noncomputable def BooleanIsoperimetry.CoherentGap.corrections (offset : ℕ) : List (Correction (offset + 2))

The complete correction list in dimension offset + 2.

Equations

• BooleanIsoperimetry.CoherentGap.corrections offset = List.ofFn (BooleanIsoperimetry.CoherentGap.correctionFor offset)

noncomputable def BooleanIsoperimetry.CoherentGap.principal (offset : ℕ) : Relation (offset + 2)

The Conway--Guy triangular-block principal relation.

Equations

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

theorem BooleanIsoperimetry.CoherentGap.coordinateSum_sub {n : ℕ} (first second : Relation n) : coordinateSum (first - second) = coordinateSum first - coordinateSum second

theorem BooleanIsoperimetry.CoherentGap.coordinateSum_finset_sum {n : ℕ} {α : Type} (set : Finset α) (relations : α → Relation n) : coordinateSum (∑ index ∈ set, relations index) = ∑ index ∈ set, coordinateSum (relations index)

@[simp]

theorem BooleanIsoperimetry.CoherentGap.coordinateSum_basis {n : ℕ} (coordinate : Fin n) : coordinateSum (basis coordinate) = 1

theorem BooleanIsoperimetry.CoherentGap.principal_coordinateSum (offset : ℕ) : coordinateSum (principal offset) = 1

theorem BooleanIsoperimetry.CoherentGap.positiveIndex_injective (offset : ℕ) : Function.Injective (positiveIndex offset)

theorem BooleanIsoperimetry.CoherentGap.negativeIndex_injective (offset : ℕ) : Function.Injective (negativeIndex offset)

theorem BooleanIsoperimetry.CoherentGap.positiveIndex_ne_negativeIndex (offset : ℕ) (positive : Fin (guide (offset + 2))) (negative : Fin (guide (offset + 2) - 1)) : positiveIndex offset positive ≠ negativeIndex offset negative

theorem BooleanIsoperimetry.CoherentGap.relation_finset_sum_apply {n : ℕ} {α : Type} (set : Finset α) (relations : α → Relation n) (coordinate : Fin n) : (∑ index ∈ set, relations index) coordinate = ∑ index ∈ set, relations index coordinate

theorem BooleanIsoperimetry.CoherentGap.sum_basis_apply {sourceDimension targetDimension : ℕ} (embedding : Fin sourceDimension → Fin targetDimension) (hinjective : Function.Injective embedding) (coordinate : Fin targetDimension) : (∑ index : Fin sourceDimension, basis (embedding index)) coordinate = if coordinate ∈ Finset.image embedding Finset.univ then 1 else 0

theorem BooleanIsoperimetry.CoherentGap.principal_entry (offset : ℕ) (coordinate : Fin (offset + 2)) : principal offset coordinate = -1 ∨ principal offset coordinate = 0 ∨ principal offset coordinate = 1

theorem BooleanIsoperimetry.CoherentGap.lift_sub {n : ℕ} (first second : Relation n) : lift (first - second) = lift first - lift second

theorem BooleanIsoperimetry.CoherentGap.iteratedLift_basis_eq {n : ℕ} (coordinate : Fin n) {steps : ℕ} (hsteps : 0 < steps) : iteratedLift (basis coordinate) steps = basis ⟨↑coordinate + steps, ⋯⟩ - basis ⟨steps - 1, ⋯⟩

@[simp]

theorem BooleanIsoperimetry.CoherentGap.castRelation_apply {firstDimension secondDimension : ℕ} (hdimension : firstDimension = secondDimension) (relation : Relation firstDimension) (coordinate : Fin secondDimension) : castRelation hdimension relation coordinate = relation (Fin.cast ⋯ coordinate)

theorem BooleanIsoperimetry.CoherentGap.castRelation_sub {firstDimension secondDimension : ℕ} (hdimension : firstDimension = secondDimension) (first second : Relation firstDimension) : castRelation hdimension (first - second) = castRelation hdimension first - castRelation hdimension second

theorem BooleanIsoperimetry.CoherentGap.castRelation_basis {firstDimension secondDimension : ℕ} (hdimension : firstDimension = secondDimension) (coordinate : Fin firstDimension) : castRelation hdimension (basis coordinate) = basis (Fin.cast hdimension coordinate)

theorem BooleanIsoperimetry.CoherentGap.correctionFor_target (offset : ℕ) (index : Fin (guide (offset + 2) - 1)) : (correctionFor offset index).target = basis (negativeIndex offset index) - basis ⟨↑index + 1, ⋯⟩

theorem BooleanIsoperimetry.CoherentGap.corrections_target_sum (offset : ℕ) : (List.map Correction.target (corrections offset)).sum = ∑ index : Fin (guide (offset + 2) - 1), (basis (negativeIndex offset index) - basis ⟨↑index + 1, ⋯⟩)

theorem BooleanIsoperimetry.CoherentGap.principal_corrections_decomposition (offset : ℕ) : principal offset + (List.map Correction.target (corrections offset)).sum = basis 0

@[irreducible]

def BooleanIsoperimetry.CoherentGap.difference (blockGuide : ℕ → ℕ) : ℕ → ℕ

The one-indexed Conway--Guy recurrence, stored with zero-based indices.

Equations

• BooleanIsoperimetry.CoherentGap.difference blockGuide 0 = 1
• BooleanIsoperimetry.CoherentGap.difference blockGuide index.succ = ∑ offset ∈ Finset.range (blockGuide (index + 2)), BooleanIsoperimetry.CoherentGap.difference blockGuide (index - offset)

noncomputable def BooleanIsoperimetry.CoherentGap.conwayGuyDifference (index : ℕ) : ℕ

The Conway--Guy difference sequence using the triangular block guide.

Equations

• BooleanIsoperimetry.CoherentGap.conwayGuyDifference index = BooleanIsoperimetry.CoherentGap.difference BooleanIsoperimetry.CoherentGap.guide index

noncomputable def BooleanIsoperimetry.CoherentGap.conwayGuyHeight (dimension : ℕ) : ℤ

The cumulative Conway--Guy heights.

Equations

• BooleanIsoperimetry.CoherentGap.conwayGuyHeight dimension = ∑ index ∈ Finset.range dimension, ↑(BooleanIsoperimetry.CoherentGap.conwayGuyDifference index)

@[simp]

theorem BooleanIsoperimetry.CoherentGap.conwayGuyHeight_zero : conwayGuyHeight 0 = 0

@[simp]

theorem BooleanIsoperimetry.CoherentGap.conwayGuyHeight_one : conwayGuyHeight 1 = 1

theorem BooleanIsoperimetry.CoherentGap.conwayGuyHeight_succ (dimension : ℕ) : conwayGuyHeight (dimension + 1) = conwayGuyHeight dimension + ↑(conwayGuyDifference dimension)

structure BooleanIsoperimetry.CoherentGap.ConwayGuyArithmetic : Type

Arithmetic data from which the coherent-gap weight tower is built.

• guide : ℕ → ℕ

  Block guide for the recurrence.

• height : ℕ → ℤ

  Cumulative heights of the recurrence.

• height_zero : self.height 0 = 0

  The zero-dimensional height.

noncomputable def BooleanIsoperimetry.CoherentGap.conwayGuyArithmetic : ConwayGuyArithmetic

The arithmetic data of the actual Conway--Guy sequence.

Equations

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

def BooleanIsoperimetry.CoherentGap.ConwayGuyArithmetic.weights (data : ConwayGuyArithmetic) (dimension : ℕ) : Relation dimension

The increasing Conway--Guy-style row obtained from cumulative heights.

Equations

• data.weights dimension coordinate = data.height dimension - data.height (dimension - (↑coordinate + 1))

def BooleanIsoperimetry.CoherentGap.ConwayGuyArithmetic.head (data : ConwayGuyArithmetic) (dimension : ℕ) : ℤ

The coordinate adjoined at the front when the dimension increases.

Equations

• data.head dimension = data.height (dimension + 1) - data.height dimension

theorem BooleanIsoperimetry.CoherentGap.ConwayGuyArithmetic.weights_step (data : ConwayGuyArithmetic) (dimension : ℕ) : data.weights (dimension + 1) = extendWeights (data.head dimension) (data.weights dimension)

def BooleanIsoperimetry.CoherentGap.ConwayGuyArithmetic.tower (data : ConwayGuyArithmetic) : WeightTower

The exact Conway--Guy-style dimension-lift tower.

Equations

• data.tower = { weights := data.weights, head := data.head, step := ⋯ }

theorem BooleanIsoperimetry.CoherentGap.dot_sub {n : ℕ} (first second weights : Relation n) : dot (first - second) weights = dot first weights - dot second weights

theorem BooleanIsoperimetry.CoherentGap.dot_finset_sum {n : ℕ} {α : Type} (set : Finset α) (relations : α → Relation n) (weights : Relation n) : dot (∑ index ∈ set, relations index) weights = ∑ index ∈ set, dot (relations index) weights

theorem BooleanIsoperimetry.CoherentGap.principal_dot (offset : ℕ) (hblock : conwayGuyHeight (offset + 2) - ∑ index : Fin (guide (offset + 2)), conwayGuyHeight (offset + 2 - ↑index - 1) + ∑ index : Fin (guide (offset + 2) - 1), conwayGuyHeight (triangular ↑index) = 1) : dot (principal offset) (conwayGuyArithmetic.weights (offset + 2)) = 1