Compositional certificates for graph rotations

Tensor and zig-zag rotations are straight-line programs calling their constituent rotations. Their certificates charge the complete vertex and edge-label encodings, including copying and intermediate pairs. The affine-plane rotation similarly composes multiplication and subtraction.

These rules certify a rotation call. They do not enumerate a graph or certify an unbounded recursive tower. In particular, a certificate for a fixed finite base is not a uniform efficiency theorem for a varying field size or tower depth.

Main results

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.rotationMap_tensor: tensor rotations.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.rotationMap_zigzag: zig-zag rotations.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.rotationMap_affinePlane: arithmetic rotations.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.rotationMap_contract: contraction through efficiently encoded and decoded slots, including the unused-slot branch.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.rotationMap_reindex: change the vertex encoding using efficient forward and inverse maps.

References

• O. Reingold, S. Vadhan, A. Wigderson, Entropy waves, the zig-zag graph product, and new constant-degree expanders

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.rotationMap_tensor {V D W E : Type} {vertex : V ↪ List Bool} {label : D ↪ List Bool} {otherVertex : W ↪ List Bool} {otherLabel : E ↪ List Bool} {G : Cslib.RotationMap V D} {H : Cslib.RotationMap W E} (hG : ComputableTidilyInPolyTime G.rot (encPair vertex label) (encPair vertex label)) (hH : ComputableTidilyInPolyTime H.rot (encPair otherVertex otherLabel) (encPair otherVertex otherLabel)) : ComputableTidilyInPolyTime (G.tensor H).rot (encPair (encPair vertex otherVertex) (encPair label otherLabel)) (encPair (encPair vertex otherVertex) (encPair label otherLabel))

A tensor rotation makes two certified calls and rearranges their complete encoded results.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.rotationMap_zigzag {V D E : Type} {vertex : V ↪ List Bool} {label : D ↪ List Bool} {otherLabel : E ↪ List Bool} {G : Cslib.RotationMap V D} {H : Cslib.RotationMap D E} (hG : ComputableTidilyInPolyTime G.rot (encPair vertex label) (encPair vertex label)) (hH : ComputableTidilyInPolyTime H.rot (encPair label otherLabel) (encPair label otherLabel)) : ComputableTidilyInPolyTime (G.zigzag H).rot (encPair (encPair vertex label) (encPair otherLabel otherLabel)) (encPair (encPair vertex label) (encPair otherLabel otherLabel))

A zig-zag rotation makes two small-graph calls and one large-graph call, retaining labels.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.rotationMap_affinePlane {K : Type} [Field K] {encode : K ↪ List Bool} (hmul : ComputableTidilyInPolyTime (fun (p : K × K) => p.1 * p.2) (encPair encode encode) encode) (hsub : ComputableTidilyInPolyTime (fun (p : K × K) => p.1 - p.2) (encPair encode encode) encode) : ComputableTidilyInPolyTime (Cslib.RotationMap.affinePlane K).rot (encPair (encPair encode encode) encode) (encPair (encPair encode encode) encode)

Field multiplication and subtraction suffice to certify the affine-plane rotation.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.rotationMap_contract {V D W : Type} {vertex : V ↪ List Bool} {label : D ↪ List Bool} {otherVertex : W ↪ List Bool} {I : Type} {slot : I ↪ List Bool} {encode : V → W × I} {decode : W × I → Option V} {rotate : V × D → V × D} (hencode : ComputableTidilyInPolyTime encode vertex (encPair otherVertex slot)) (hdecode : ComputableTidilyInPolyTime decode (encPair otherVertex slot) (encOption vertex)) (hrotate : ComputableTidilyInPolyTime rotate (encPair vertex label) (encPair vertex label)) : ComputableTidilyInPolyTime (Cslib.RotationMap.contractRot encode decode rotate) (encPair otherVertex (encPair slot label)) (encPair otherVertex (encPair slot label))

Contraction charges slot decoding, the occupied-slot rotation and re-encoding, and the unused-slot fallback, with all complete vertex and label encodings.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.rotationMap_reindex {V D W : Type} {vertex : V ↪ List Bool} {label : D ↪ List Bool} {otherVertex : W ↪ List Bool} {forward : V → W} {backward : W → V} {rotate : V × D → V × D} (hrotate : ComputableTidilyInPolyTime rotate (encPair vertex label) (encPair vertex label)) (hforward : ComputableTidilyInPolyTime forward vertex otherVertex) (hbackward : ComputableTidilyInPolyTime backward otherVertex vertex) : ComputableTidilyInPolyTime (Cslib.RotationMap.reindexRot forward backward rotate) (encPair otherVertex label) (encPair otherVertex label)

Vertex renaming charges the forward and backward maps and the complete rotation.