Native initialization from actual stored rows

The initial buffer is the flattening of one actual first stored row per constraint. Its native certificate applies to all raw inputs; its agreement with occurrence labelings uses the full model guard. In particular, false nullaries and malformed arities cannot enter the optimizer through a fabricated initial row. This representation bookkeeping is original.

theorem Cslib.Complexity.CSP.EdgeSolver.initial_buffer (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (h : checkModel F = true) : List.map (initial F) F.incidenceList = (initialRows F).flatten

Materialize the actual first-row initializer in ordinary incidence order.

theorem Cslib.Complexity.CSP.EdgeSolver.computableInPolyTime_initialBuffer : Turing.MultiTapeTM.ComputableInPolyTime (fun (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) => (initialRows F).flatten) (encCSP encTable Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)

Actual stored-row initialization is native polynomial-time on every raw framed CSP. No satisfying assignment, valid row or width certificate is supplied as input.