This is an optimization equivalence, not a claim that all original feasible points have integer time coordinates.
Write the mixed model as rows in integer variables x and continuous variables y. The admission check requires ordinary integer/continuous types only; each row has zero, one, or two y coefficients, all unit signed, with opposite signs when there are two. All coefficients on x and all finite row bounds are exact integers of magnitude at most 2^40. Every y column has at least one finite integral bound; its other bound can be infinite. All costs are finite. Pure continuous models are excluded.
Fix any feasible integer x. The residual bounds on each row are integers. Each row of the continuous block is a signed unit vector or a difference of two unit vectors. The transpose is a directed node-edge incidence matrix with a row deleted for edges to an auxiliary ground node. It is totally unimodular. Adding unit bound rows and negating or duplicating rows for lower/upper inequalities preserves total unimodularity. Therefore every vertex of the residual continuous polyhedron is integral.
The finite bound on each continuous column makes that polyhedron pointed: a direction of a line would have to be zero on every column. A nonempty pointed polyhedron has a vertex, and whenever its linear objective has a finite optimum it has an optimal vertex. Consequently, whenever the original mixed model has a finite attained optimum, an equally good feasible point exists with all y integral. Restricting all y, or any subset, to integers retains that optimum and cannot introduce a better one. Feasibility is retained for each feasible integer assignment to x. This also follows from the integral-polyhedron characterization.
The guard uses exact comparisons, not tolerance rounding. A future product implementation must run on a private internal model, leave the public model and objective untouched, charge construction time, and skip supplied primal solutions/callbacks until their compatibility is established. It must not confuse optimization equivalence with preservation of an arbitrary original feasible point.
For Csched008 the current certificate admits 252 continuous and 1284 integer columns. The derived MPS files are re-read through the native API and compared field by field: column order/names, sense/offset/costs, all row bounds and terms, all other domains. Feasible scout solutions receive a second GMP check on the original MIPLIB model. These are scouting timings, not accepted native original-model speedups.
The separate objective<=171 and objective=172 models change the feasible set and are proof-structure diagnostics only. They cannot be reported as cold solves of the original model. Their thresholds come from the observed bound/incumbent interval, not a claimed generic product algorithm.