Coherent-gap certificates

This file formalizes the algebraic certificate mechanism behind normalized chamber rigidity for a fixed coherent Boolean term order. The motivating order is the Conway--Guy order from:

• Tom Bohman, "A sum packing problem of Erdős and the Conway--Guy sequence," Proceedings of the AMS 124 (1996), 3627--3636.

The definitions below do not assume Bohman's distinct-subset-sum theorem. That theorem is needed only to identify integral unit relations with consecutive gaps in the Conway--Guy subset-sum order.

The open-problem context and the exact boundary of this formalization are recorded separately in the Construct research notes.

@[reducible, inline]

abbrev BooleanIsoperimetry.CoherentGap.Relation (n : ℕ) : Type

An integer relation in dimension n.

Equations

• BooleanIsoperimetry.CoherentGap.Relation n = (Fin n → ℤ)

def BooleanIsoperimetry.CoherentGap.coordinateSum {n : ℕ} (relation : Relation n) : ℤ

The coordinate sum of an integer relation.

Equations

• BooleanIsoperimetry.CoherentGap.coordinateSum relation = ∑ i : Fin n, relation i

def BooleanIsoperimetry.CoherentGap.dot {n : ℕ} (relation weights : Relation n) : ℤ

The scalar product of an integer relation with an integer weight row.

Equations

• BooleanIsoperimetry.CoherentGap.dot relation weights = ∑ i : Fin n, relation i * weights i

def BooleanIsoperimetry.CoherentGap.basis {n : ℕ} (coordinate : Fin n) : Relation n

The standard coordinate vector.

Equations

• BooleanIsoperimetry.CoherentGap.basis coordinate i = if i = coordinate then 1 else 0

def BooleanIsoperimetry.CoherentGap.IsLiftableUnit {n : ℕ} (weights relation : Relation n) : Prop

A relation whose entries and coordinate sum lie in {-1, 0, 1} and whose value on the weight row is one.

Equations

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

def BooleanIsoperimetry.CoherentGap.aggregate {n : ℕ} (relations : List (Relation n)) : Relation n

Pointwise sum of a list of relations.

Equations

• BooleanIsoperimetry.CoherentGap.aggregate relations = relations.sum

structure BooleanIsoperimetry.CoherentGap.Certificate {n : ℕ} (weights target : Relation n) : Type

A nonnegative integral dual certificate, represented as a list so that multiplicity is the coefficient of a relation.

• relations : List (Relation n)

  Relations listed with their certificate multiplicities.

• valid (relation : Relation n) : relation ∈ self.relations → IsLiftableUnit weights relation

  Every listed relation is a liftable unit relation.

• target_eq : aggregate self.relations = target

  The listed relations sum to the certificate target.

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

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

theorem BooleanIsoperimetry.CoherentGap.dot_aggregate {n : ℕ} (relations : List (Relation n)) (weights : Relation n) : dot (aggregate relations) weights = (List.map (fun (relation : Relation n) => dot relation weights) relations).sum

@[simp]

theorem BooleanIsoperimetry.CoherentGap.dot_basis {n : ℕ} (coordinate : Fin n) (weights : Relation n) : dot (basis coordinate) weights = weights coordinate

theorem BooleanIsoperimetry.CoherentGap.Certificate.length_eq_dot_target {n : ℕ} {weights target : Relation n} (certificate : Certificate weights target) : ↑certificate.relations.length = dot target weights

The mass of a certificate equals the value of its target on the weights.

def BooleanIsoperimetry.CoherentGap.Certificate.singleton {n : ℕ} {weights relation : Relation n} (hrelation : IsLiftableUnit weights relation) : Certificate weights relation

A one-relation certificate.

Equations

• BooleanIsoperimetry.CoherentGap.Certificate.singleton hrelation = { relations := [relation], valid := ⋯, target_eq := ⋯ }

def BooleanIsoperimetry.CoherentGap.Certificate.add {n : ℕ} {weights firstTarget secondTarget : Relation n} (first : Certificate weights firstTarget) (second : Certificate weights secondTarget) : Certificate weights (firstTarget + secondTarget)

Add two certificates.

Equations

• first.add second = { relations := first.relations ++ second.relations, valid := ⋯, target_eq := ⋯ }

def BooleanIsoperimetry.CoherentGap.Certificate.castTarget {n : ℕ} {weights firstTarget secondTarget : Relation n} (certificate : Certificate weights firstTarget) (htarget : firstTarget = secondTarget) : Certificate weights secondTarget

Reinterpret the target of a certificate along an equality.

Equations

• certificate.castTarget htarget = htarget ▸ certificate

def BooleanIsoperimetry.CoherentGap.Certificate.sum {n : ℕ} {weights : Relation n} (certificates : List ((target : Relation n) × Certificate weights target)) : Certificate weights (List.map Sigma.fst certificates).sum

The sum of a list of dependently packaged certificates.

Equations

• BooleanIsoperimetry.CoherentGap.Certificate.sum [] = { relations := [], valid := ⋯, target_eq := ⋯ }
• BooleanIsoperimetry.CoherentGap.Certificate.sum (⟨target, certificate⟩ :: certificates) = ⋯.mpr (certificate.add (BooleanIsoperimetry.CoherentGap.Certificate.sum certificates))

def BooleanIsoperimetry.CoherentGap.extendWeights {n : ℕ} (head : ℤ) (weights : Relation n) : Relation (n + 1)

Add one coordinate at the front of a weight row.

Equations

• BooleanIsoperimetry.CoherentGap.extendWeights head weights i = Fin.cases head (fun (i : Fin n) => head + weights i) i

def BooleanIsoperimetry.CoherentGap.lift {n : ℕ} (relation : Relation n) : Relation (n + 1)

Lift a relation by adding the negative coordinate sum at the front.

Equations

• BooleanIsoperimetry.CoherentGap.lift relation i = Fin.cases (-BooleanIsoperimetry.CoherentGap.coordinateSum relation) relation i

@[simp]

theorem BooleanIsoperimetry.CoherentGap.coordinateSum_lift {n : ℕ} (relation : Relation n) : coordinateSum (lift relation) = 0

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

theorem BooleanIsoperimetry.CoherentGap.lift_aggregate {n : ℕ} (relations : List (Relation n)) : aggregate (List.map lift relations) = lift (aggregate relations)

def BooleanIsoperimetry.CoherentGap.iteratedLift {n : ℕ} (relation : Relation n) (steps : ℕ) : Relation (n + steps)

Iterate the dimension lift.

Equations

• BooleanIsoperimetry.CoherentGap.iteratedLift relation 0 = relation
• BooleanIsoperimetry.CoherentGap.iteratedLift relation steps.succ = BooleanIsoperimetry.CoherentGap.lift (BooleanIsoperimetry.CoherentGap.iteratedLift relation steps)

def BooleanIsoperimetry.CoherentGap.castRelation {firstDimension secondDimension : ℕ} (hdimension : firstDimension = secondDimension) (relation : Relation firstDimension) : Relation secondDimension

Transport a relation through an equality of dimensions.

Equations

• BooleanIsoperimetry.CoherentGap.castRelation hdimension relation = hdimension ▸ relation

theorem BooleanIsoperimetry.CoherentGap.dot_lift_extendWeights {n : ℕ} (head : ℤ) (weights relation : Relation n) : dot (lift relation) (extendWeights head weights) = dot relation weights

theorem BooleanIsoperimetry.CoherentGap.IsLiftableUnit.lift {n : ℕ} {weights relation : Relation n} (hrelation : IsLiftableUnit weights relation) (head : ℤ) : IsLiftableUnit (extendWeights head weights) (CoherentGap.lift relation)

def BooleanIsoperimetry.CoherentGap.Certificate.lift {n : ℕ} {weights target : Relation n} (certificate : Certificate weights target) (head : ℤ) : Certificate (extendWeights head weights) (CoherentGap.lift target)

Lift every relation in a certificate by one dimension.

Equations

• certificate.lift head = { relations := List.map BooleanIsoperimetry.CoherentGap.lift certificate.relations, valid := ⋯, target_eq := ⋯ }

@[simp]

theorem BooleanIsoperimetry.CoherentGap.lift_basis {n : ℕ} (coordinate : Fin n) : lift (basis coordinate) = basis coordinate.succ - basis 0

structure BooleanIsoperimetry.CoherentGap.WeightTower : Type

A tower of rows obtained by adjoining one new positive-linear coordinate at the front at each dimension.

• weights (n : ℕ) : Relation n

  The reference row in each dimension.

• head : ℕ → ℤ

  The coordinate adjoined when passing from dimension n to n + 1.

• step (n : ℕ) : self.weights (n + 1) = extendWeights (self.head n) (self.weights n)

  Every row is obtained from the preceding row by the dimension lift.

def BooleanIsoperimetry.CoherentGap.WeightTower.liftCertificate (tower : WeightTower) {n : ℕ} {target : Relation n} (certificate : Certificate (tower.weights n) target) : Certificate (tower.weights (n + 1)) (lift target)

Transport a certificate through one step of a weight tower.

Equations

• tower.liftCertificate certificate = ⋯.mpr (certificate.lift (tower.head n))

def BooleanIsoperimetry.CoherentGap.WeightTower.iteratedLiftCertificate (tower : WeightTower) {n : ℕ} {target : Relation n} (certificate : Certificate (tower.weights n) target) (steps : ℕ) : Certificate (tower.weights (n + steps)) (iteratedLift target steps)

Repeatedly transport a certificate through a weight tower.

Equations

• tower.iteratedLiftCertificate certificate 0 = certificate
• tower.iteratedLiftCertificate certificate steps.succ = tower.liftCertificate (tower.iteratedLiftCertificate certificate steps)

def BooleanIsoperimetry.CoherentGap.Certificate.castDimension {firstDimension secondDimension : ℕ} (tower : WeightTower) {target : Relation firstDimension} (certificate : Certificate (tower.weights firstDimension) target) (hdimension : firstDimension = secondDimension) : Certificate (tower.weights secondDimension) (castRelation hdimension target)

Reinterpret a certificate along an equality of dimensions.

Equations

• BooleanIsoperimetry.CoherentGap.Certificate.castDimension tower certificate hdimension = hdimension ▸ certificate

structure BooleanIsoperimetry.CoherentGap.Correction (dimension : ℕ) : Type

One correction in the strong-induction construction of a first-coordinate certificate.

• sourceOffset : ℕ

  The source dimension is sourceOffset + 1.

• sourceCoordinate : Fin (self.sourceOffset + 1)

  The smaller-dimensional coordinate whose certificate is lifted.

• steps : ℕ

  Number of dimension lifts.

• steps_pos : 0 < self.steps

  Every correction comes from a strictly smaller dimension.

• dimension_eq : self.sourceOffset + 1 + self.steps = dimension

  Lifting reaches the target dimension exactly.

theorem BooleanIsoperimetry.CoherentGap.Correction.sourceDimension_lt {dimension : ℕ} (correction : Correction dimension) : correction.sourceOffset + 1 < dimension

theorem BooleanIsoperimetry.CoherentGap.Correction.sourceOffset_lt {offset : ℕ} (correction : Correction (offset + 2)) : correction.sourceOffset < offset + 1

def BooleanIsoperimetry.CoherentGap.Correction.target {dimension : ℕ} (correction : Correction dimension) : Relation dimension

The target contributed by a lifted smaller-dimensional basis certificate.

Equations

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

def BooleanIsoperimetry.CoherentGap.Correction.liftCertificate {dimension : ℕ} (correction : Correction dimension) (tower : WeightTower) (certificate : Certificate (tower.weights (correction.sourceOffset + 1)) (basis correction.sourceCoordinate)) : Certificate (tower.weights dimension) correction.target

Realize a correction from a certificate in its source dimension.

Equations

• correction.liftCertificate tower certificate = id (BooleanIsoperimetry.CoherentGap.Certificate.castDimension tower (tower.iteratedLiftCertificate certificate correction.steps) ⋯)

structure BooleanIsoperimetry.CoherentGap.FirstCoordinateRecurrence (tower : WeightTower) : Type

Exact data needed at each dimension for the principal-relation strong-induction step. Every load-bearing input is a field: the principal relation must be a liftable unit relation, and its sum with the explicitly listed lifted corrections must be the first basis vector.

• base : Certificate (tower.weights 1) (basis 0)

  First-coordinate certificate in dimension one.

• principal (offset : ℕ) : Relation (offset + 2)

  The new principal relation in dimension offset + 2.

• principal_valid (offset : ℕ) : IsLiftableUnit (tower.weights (offset + 2)) (self.principal offset)

  Every principal relation belongs to the liftable unit system.

• corrections (offset : ℕ) : List (Correction (offset + 2))

  Smaller-dimensional certificate lifts used to cancel the principal relation.

• decomposition (offset : ℕ) : self.principal offset + (List.map Correction.target (self.corrections offset)).sum = basis 0

  The principal relation plus all correction targets is the first basis vector.

def BooleanIsoperimetry.CoherentGap.allCoordinatesOfFirst (tower : WeightTower) (first : (n : ℕ) → Certificate (tower.weights (n + 1)) (basis 0)) (n : ℕ) (coordinate : Fin n) : Certificate (tower.weights n) (basis coordinate)

If the first coordinate has a certificate in every positive dimension, the dimension lift supplies certificates for every coordinate.

Equations

• One or more equations did not get rendered due to their size.
• BooleanIsoperimetry.CoherentGap.allCoordinatesOfFirst tower first 0 coordinate = coordinate.elim0

theorem BooleanIsoperimetry.CoherentGap.recurrenceCertificate_exists (tower : WeightTower) (recurrence : FirstCoordinateRecurrence tower) (dimension : ℕ) (coordinate : Fin dimension) : Nonempty (Certificate (tower.weights dimension) (basis coordinate))

Strong induction on dimension constructs all coordinate certificates from the explicit principal relations and correction chains.

noncomputable def BooleanIsoperimetry.CoherentGap.recurrenceCertificates (tower : WeightTower) (recurrence : FirstCoordinateRecurrence tower) (n : ℕ) (coordinate : Fin n) : Certificate (tower.weights n) (basis coordinate)

The full certificate family generated by an explicit principal/correction recurrence.

Equations

• BooleanIsoperimetry.CoherentGap.recurrenceCertificates tower recurrence n coordinate = Classical.choice ⋯

def BooleanIsoperimetry.CoherentGap.realDot {n : ℕ} (relation : Relation n) (candidate : Fin n → ℝ) : ℝ

Pair an integer relation with a real candidate row.

Equations

• BooleanIsoperimetry.CoherentGap.realDot relation candidate = ∑ i : Fin n, ↑(relation i) * candidate i

theorem BooleanIsoperimetry.CoherentGap.realDot_add {n : ℕ} (first second : Relation n) (candidate : Fin n → ℝ) : realDot (first + second) candidate = realDot first candidate + realDot second candidate

theorem BooleanIsoperimetry.CoherentGap.realDot_aggregate {n : ℕ} (relations : List (Relation n)) (candidate : Fin n → ℝ) : realDot (aggregate relations) candidate = (List.map (fun (relation : Relation n) => realDot relation candidate) relations).sum

@[simp]

theorem BooleanIsoperimetry.CoherentGap.realDot_basis {n : ℕ} (coordinate : Fin n) (candidate : Fin n → ℝ) : realDot (basis coordinate) candidate = candidate coordinate

theorem BooleanIsoperimetry.CoherentGap.coordinate_lower_bound {n : ℕ} {weights : Relation n} {coordinate : Fin n} (certificate : Certificate weights (basis coordinate)) (candidate : Fin n → ℝ) (hgap : ∀ (relation : Relation n), IsLiftableUnit weights relation → 1 ≤ realDot relation candidate) : ↑(weights coordinate) ≤ candidate coordinate

Abstract normalized-chamber rigidity. A certificate for a coordinate forces every real row satisfying all its unit-relation inequalities to dominate the corresponding reference weight.

theorem BooleanIsoperimetry.CoherentGap.recurrenceCertificate_mass (tower : WeightTower) (recurrence : FirstCoordinateRecurrence tower) {n : ℕ} (coordinate : Fin n) : ↑(recurrenceCertificates tower recurrence n coordinate).relations.length = tower.weights n coordinate

Every recurrence certificate has mass equal to its Conway--Guy-style reference coordinate.

theorem BooleanIsoperimetry.CoherentGap.normalizedChamberRigidity (tower : WeightTower) (recurrence : FirstCoordinateRecurrence tower) {n : ℕ} (candidate : Fin n → ℝ) (hgap : ∀ (relation : Relation n), IsLiftableUnit (tower.weights n) relation → 1 ≤ realDot relation candidate) (coordinate : Fin n) : ↑(tower.weights n coordinate) ≤ candidate coordinate

Normalized chamber rigidity. An explicit principal/correction recurrence makes the reference row a coordinatewise lower bound for every row satisfying its unit-relation inequalities.

For the Conway--Guy order, the remaining concrete instantiation consists of:

1. the recurrence W_(n+1) = (d_(n+1), d_(n+1) + W_n);
2. the block identity proving that each published principal relation has value one;
3. the triangular-index correction list and its basis-vector decomposition.

Bohman's distinct-subset-sum theorem is then used outside this algebraic statement to identify the unit relations with consecutive order gaps.