Documentation

CslibFrontier.Computability.PolyTime.Graph.RotationSystem.Recognition.Query

Native frozen parity-query computation #

Every certificate covers all raw inputs. Unary ranges are funded only by actual vertex/edge list lengths. All supplied endpoint/dart labels use binary comparisons and saturating binary lookup, including malformed huge indices. The concrete query composes the sparse compiler with XORSAT.computableInPolyTime_solve; there is no solver, recognizer, growth or encoding provider hypothesis.

Main results #

source
theorem Cslib.Complexity.Graph.RotationRecognition.fiber_polyTime :
Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Graph × ℕ) => fiber p.1 p.2) (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Binary-indexed endpoint fibers are computed from the actual edge count on all graphs.

source
theorem Cslib.Complexity.Graph.RotationRecognition.validate_polyTime :
Turing.MultiTapeTM.ComputableInPolyTime validate encFixedRotationInput Turing.MultiTapeTM.encBool

The dense/full-order validator has no raw well-formedness premise.

source
theorem Cslib.Complexity.Graph.RotationRecognition.subdivide_polyTime :
Turing.MultiTapeTM.ComputableInPolyTime subdivide encFixedRotationInput (Turing.MultiTapeTM.encList encSegment)

Twice subdivision preserves list occurrence identity and is native on every raw input.

source
theorem Cslib.Complexity.Graph.RotationRecognition.referenceOrder_polyTime :
Turing.MultiTapeTM.ComputableInPolyTime referenceOrder encFixedRotationInput (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

The full reference order is built from bounded list scans, including malformed words.

source
theorem Cslib.Complexity.Graph.RotationRecognition.frame_polyTime :
Turing.MultiTapeTM.ComputableInPolyTime frame encFixedRotationInput encFrame

Frame construction is native, with its unary stride funded by actual list lengths.

source
theorem Cslib.Complexity.Graph.RotationRecognition.compileFrame_polyTime :
Turing.MultiTapeTM.ComputableInPolyTime compileFrame encFrame XORSAT.encoding

Sparse row emission scans only segment occurrences, with width at most four.

source
theorem Cslib.Complexity.Graph.RotationRecognition.compile_polyTime :
Turing.MultiTapeTM.ComputableInPolyTime compile encFixedRotationInput XORSAT.encoding

The full graph/order-to-XOR compiler is an ordinary native polynomial-time function.

source
theorem Cslib.Complexity.Graph.RotationRecognition.query_polyTime :
Turing.MultiTapeTM.ComputableInPolyTime query encFixedRotationInput Turing.MultiTapeTM.encBool

Concrete all-raw native query. Invalid models reject, and every valid query actually calls existing certified sparse Gaussian elimination. No topological criterion is used.