The Conway--Guy triangular-block identity

This file derives the height identity used by every Conway--Guy principal relation directly from the published difference recurrence.

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

theorem BooleanIsoperimetry.CoherentGap.guide_at_triangular_end (width : ℕ) : guide (triangular width + 1) = width

theorem BooleanIsoperimetry.CoherentGap.guide_eq_iff {dimension width : ℕ} (hwidth : 0 < width) : guide dimension = width ↔ triangular (width - 1) + 2 ≤ dimension ∧ dimension ≤ triangular width + 1

noncomputable def BooleanIsoperimetry.CoherentGap.residual (width dimension : ℕ) : ℤ

The left-hand residual of the Conway--Guy block recurrence.

Equations

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

theorem BooleanIsoperimetry.CoherentGap.conwayGuyDifference_succ (index : ℕ) : conwayGuyDifference (index + 1) = ∑ offset ∈ Finset.range (guide (index + 2)), conwayGuyDifference (index - offset)

theorem BooleanIsoperimetry.CoherentGap.residual_succ_eq {width dimension : ℕ} (hdimension : 0 < dimension) (hwidth : width ≤ dimension) (hguide : guide (dimension + 1) = width) : residual width (dimension + 1) = residual width dimension

theorem BooleanIsoperimetry.CoherentGap.reverse_difference_sum (dimension width : ℕ) : width ≤ dimension → ∑ index : Fin width, ↑(conwayGuyDifference (dimension - ↑index - 1)) = conwayGuyHeight dimension - conwayGuyHeight (dimension - width)

theorem BooleanIsoperimetry.CoherentGap.conwayGuyDifference_eq_height_window (dimension : ℕ) (hdimension : 0 < dimension) : ↑(conwayGuyDifference dimension) = conwayGuyHeight dimension - conwayGuyHeight (dimension - guide (dimension + 1))

theorem BooleanIsoperimetry.CoherentGap.residual_succ_width (width dimension : ℕ) : residual (width + 1) (dimension + 1) = residual width dimension + ↑(conwayGuyDifference dimension) - conwayGuyHeight dimension

theorem BooleanIsoperimetry.CoherentGap.residual_eq_block_start {width dimension : ℕ} (hwidth : 0 < width) (hguide : guide dimension = width) : residual width dimension = residual width (triangular (width - 1) + 2)

theorem BooleanIsoperimetry.CoherentGap.residual_next_block_start (previous : ℕ) : residual (previous + 2) (triangular (previous + 1) + 2) = residual (previous + 1) (triangular (previous + 1) + 1) - conwayGuyHeight (triangular previous)

theorem BooleanIsoperimetry.CoherentGap.correction_sum_succ (previous : ℕ) : ∑ index : Fin (previous + 1), conwayGuyHeight (triangular ↑index) = ∑ index : Fin previous, conwayGuyHeight (triangular ↑index) + conwayGuyHeight (triangular previous)

theorem BooleanIsoperimetry.CoherentGap.block_identity_by_width (previous dimension : ℕ) : guide dimension = previous + 1 → residual (previous + 1) dimension + ∑ index : Fin previous, conwayGuyHeight (triangular ↑index) = 1

theorem BooleanIsoperimetry.CoherentGap.conwayGuy_block_identity (dimension : ℕ) (hdimension : 2 ≤ dimension) : conwayGuyHeight dimension - ∑ index : Fin (guide dimension), conwayGuyHeight (dimension - ↑index - 1) + ∑ index : Fin (guide dimension - 1), conwayGuyHeight (triangular ↑index) = 1

The exact triangular-block identity for every Conway--Guy height.