Documentation

LeanPool.BooleanIsoperimetry.ConwayGuyRigidity

Conway--Guy normalized chamber rigidity #

This file packages the concrete Conway--Guy principal relations and triangular corrections as a FirstCoordinateRecurrence. The separate height identity supplies the one remaining arithmetic input.

source
def BooleanIsoperimetry.CoherentGap.ConwayGuyBlockIdentity (offset : ℕ) :
Prop

The triangular-block identity needed to evaluate a Conway--Guy principal relation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def BooleanIsoperimetry.CoherentGap.conwayGuyBaseCertificate :
    Certificate (conwayGuyArithmetic.tower.weights 1) (basis 0)

    The dimension-one Conway--Guy basis certificate.

    Equations
    Instances For
      source
      theorem BooleanIsoperimetry.CoherentGap.principal_valid (hblock : ∀ (offset : ℕ), ConwayGuyBlockIdentity offset) (offset : ℕ) :
      IsLiftableUnit (conwayGuyArithmetic.tower.weights (offset + 2)) (principal offset)
      source
      noncomputable def BooleanIsoperimetry.CoherentGap.conwayGuyFirstCoordinateRecurrence (hblock : ∀ (offset : ℕ), ConwayGuyBlockIdentity offset) :
      FirstCoordinateRecurrence conwayGuyArithmetic.tower

      The concrete first-coordinate recurrence, conditional only on the explicit Conway--Guy block identity.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem BooleanIsoperimetry.CoherentGap.conwayGuyNormalizedChamberRigidity_of_blockIdentity (hblock : ∀ (offset : ℕ), ConwayGuyBlockIdentity offset) {n : ℕ} (candidate : Fin n → ℝ) (hgap : ∀ (relation : Relation n), IsLiftableUnit (conwayGuyArithmetic.tower.weights n) relation → 1 ≤ realDot relation candidate) (coordinate : Fin n) :
        ↑(conwayGuyArithmetic.tower.weights n coordinate) ≤ candidate coordinate

        Conditional concrete normalized chamber rigidity. The height file discharges hblock from the published Conway--Guy recurrence.

        source
        theorem BooleanIsoperimetry.CoherentGap.conwayGuyBlockIdentity_all (offset : ℕ) :
        ConwayGuyBlockIdentity offset
        source
        noncomputable def BooleanIsoperimetry.CoherentGap.conwayGuyRecurrence :
        FirstCoordinateRecurrence conwayGuyArithmetic.tower

        The unconditional first-coordinate certificate recurrence for the Conway--Guy row.

        Equations
        Instances For
          source
          theorem BooleanIsoperimetry.CoherentGap.conwayGuyCertificate_exists (dimension : ℕ) (coordinate : Fin dimension) :
          Nonempty (Certificate (conwayGuyArithmetic.tower.weights dimension) (basis coordinate))

          Every coordinate of every Conway--Guy row has a nonnegative integral certificate supported on liftable unit relations.

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

          Conway--Guy normalized chamber rigidity. Every real row satisfying all unit-relation inequalities of the Conway--Guy row dominates it coordinatewise.

          Bohman's distinct-subset-sum theorem is a separate external input identifying these unit relations with consecutive gaps of the induced Boolean term order.