Documentation

CslibFrontier.Computability.Complexity.Problems.Graph.RotationSystem.Recognition.Bounds

Explicit sparse-query size bounds #

These bounds include the full framed sparse-system encoding, rather than just matrix dimensions. They concern the finite compiler only and do not supply a topological recognition criterion.

source
def Cslib.Complexity.Graph.RotationRecognition.BoundedEndpoints (F : Frame) :
Prop

Every endpoint in an algebraic frame lies below its declared stride.

Instances For
    source
    theorem Cslib.Complexity.Graph.RotationRecognition.boundedEndpoints_frame {I : FixedRotationInput} (hI : Valid I) :
    BoundedEndpoints (frame I)

    A segment emitted by twice subdivision is closed on its dense declared vertex range.

    source
    theorem Cslib.Complexity.Graph.RotationRecognition.label_lt_row {F : Frame} (hF : BoundedEndpoints F) {e f : Segment × ℕ} (he : e ∈ F.segments.zipIdx) (hf : f ∈ F.segments.zipIdx) {label : ℕ} (hl : label ∈ (row F e f).1) :
    label < F.segments.length * F.vertexCount

    Every variable in a literal row lies in the finite rectangular move frame.

    source
    theorem Cslib.Complexity.Graph.RotationRecognition.mem_compileFrame {F : Frame} {r : Logic.PL.AffineEquation ℕ} :
    r ∈ compileFrame F ↔ ∃ e ∈ F.segments.zipIdx, ∃ f ∈ F.segments.zipIdx, f.2 < e.2 ∧ independent e.1.endpoints f.1.endpoints = true ∧ r = row F e f

    Every compiled row comes from an actual independent pair of segment occurrences.

    source
    theorem Cslib.Complexity.Graph.RotationRecognition.width_compileFrame {F : Frame} {r : Logic.PL.AffineEquation ℕ} (hr : r ∈ compileFrame F) :
    r.1.length ≤ 4

    The finite system uses at most four labels per row.

    source
    theorem Cslib.Complexity.Graph.RotationRecognition.bits_compileFrame {F : Frame} (hF : BoundedEndpoints F) {r : Logic.PL.AffineEquation ℕ} (hr : r ∈ compileFrame F) {label : ℕ} (hl : label ∈ r.1) :
    (Turing.MultiTapeTM.encNat label).length ≤ (F.segments.length * F.vertexCount).log2 + 1

    Full binary label width including the zero/empty-frame case.

    source
    theorem Cslib.Complexity.Graph.RotationRecognition.framed_row_length_le {r : Logic.PL.AffineEquation ℕ} {ell : ℕ} (hw : r.1.length ≤ 4) (hb : ∀ label ∈ r.1, (Turing.MultiTapeTM.encNat label).length ≤ ell) :
    2 * (XORSAT.equationEncoding r).length + 1 ≤ 32 * ell + 21

    Each fully framed sparse row costs at most 32 ell + 21 bits in its outer system list.

    source
    theorem Cslib.Complexity.Graph.RotationRecognition.length_encoding_compileFrame_le {F : Frame} (hF : BoundedEndpoints F) :
    (XORSAT.encoding (compileFrame F)).length ≤ F.segments.length ^ 2 * (32 * ((F.segments.length * F.vertexCount).log2 + 1) + 21)

    The entire sparse system encoding, including equation and list framing.