Correctness of a compacted geometric scheduler step

A phase satisfying the geometric output contract, followed by the fixed buffer wiring, produces another encoded scheduler state. All request identities and stored point lists are preserved, and the completed schedule remains pairwise disjoint.

theorem Algebraic.MassProduction.Nonuniform.BufferModel.advance_input_of_correct {width total completed requestDepth dimension requestWidth menuDepth accepted remaining : ℕ} (positive : 0 < width) (state : State total completed (Sorting.networkRecords requestDepth) dimension width) (data : Fin total → Fin requestWidth → Bool) (targets : Fin total → Fin dimension → BinaryExtension width) (previous : WellScheduled state targets) (menu : Fin (Sorting.networkRecords menuDepth) → Fin (Sorting.networkRecords requestDepth) → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (phase : Circuit DeMorgan.signature (BufferInput.inputWidth completed (Sorting.networkRecords requestDepth) requestWidth (2 ^ width) (dimension * width)) (Sorting.networkRecords requestDepth * (1 + BufferInput.storedWidth requestWidth (2 ^ width) (dimension * width)))) (split : accepted + remaining = Sorting.networkRecords requestDepth) (correct : GeometricPhase.CorrectOutput positive menu (pendingRecord state data) (pendingTargets state targets) (occupied state targets) accepted (phase.eval DeMorgan.interpretation (input positive state data targets))) : ∃ (next : State total (completed + accepted) remaining dimension width), (BufferAdvance.circuit phase split).eval DeMorgan.interpretation (input positive state data targets) = input positive next data targets ∧ WellScheduled next targets

A correct geometric phase plus free compaction preserves the full encoded-state invariant needed by the next halving phase.