Selecting disjoint requests from an enumerated candidate menu

This circuit computes the clean flags of all enumerated recovery sets and selects a clean prefix from one successful candidate. Original request payloads are preserved as a permutation. The remaining obligations for a complete geometric scheduler are point generation, a menu guarantee for the encoded state, and iteration of the resulting phase.

def Algebraic.MassProduction.Nonuniform.MenuSelection.requestSet {candidates requests slots depth inputs keyWidth : ℕ} (layout : Fin candidates × Fin requests × Fin slots ≃ Fin (Sorting.networkRecords depth)) (valid : Fin (Sorting.networkRecords depth) → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) (candidate : Fin candidates) (request : Fin requests) : Finset (Fin keyWidth → Bool)

Recovery set represented by one candidate/request's valid point slots.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.MassProduction.Nonuniform.MenuSelection.RequestClean {candidates requests slots depth inputs keyWidth sources : ℕ} (layout : Fin candidates × Fin requests × Fin slots ≃ Fin (Sorting.networkRecords depth)) (valid : Fin (Sorting.networkRecords depth) → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) (candidate : Fin candidates) (request : Fin requests) : Prop

Cleanliness of the represented recovery set in its candidate.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.MassProduction.Nonuniform.MenuSelection.circuit {menuDepth requestDepth slots depth groupWidth inputs keyWidth sources padding routingDepth payloadWidth needed : ℕ} (layout : Fin (Sorting.networkRecords menuDepth) × Fin (Sorting.networkRecords requestDepth) × Fin slots ≃ Fin (Sorting.networkRecords depth)) (codes : Fin (Sorting.networkRecords menuDepth) → Fin groupWidth → Bool) (valid : Fin (Sorting.networkRecords depth) → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (recordCount : sources + Sorting.networkRecords depth + padding = Sorting.networkRecords routingDepth) (payloads : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth) → Fin payloadWidth → DeMorgan.Wiring inputs) (positive : 0 < needed) (fits : needed ≤ Sorting.networkRecords requestDepth) : Circuit DeMorgan.signature inputs (CandidateSelection.rowBits requestDepth payloadWidth)

The complete clean-test and selection circuit for an enumerated menu.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.Nonuniform.MenuSelection.circuit_size {menuDepth requestDepth slots depth groupWidth inputs keyWidth sources padding routingDepth payloadWidth needed : ℕ} (layout : Fin (Sorting.networkRecords menuDepth) × Fin (Sorting.networkRecords requestDepth) × Fin slots ≃ Fin (Sorting.networkRecords depth)) (codes : Fin (Sorting.networkRecords menuDepth) → Fin groupWidth → Bool) (valid : Fin (Sorting.networkRecords depth) → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (recordCount : sources + Sorting.networkRecords depth + padding = Sorting.networkRecords routingDepth) (payloads : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth) → Fin payloadWidth → DeMorgan.Wiring inputs) (positive : 0 < needed) (fits : needed ≤ Sorting.networkRecords requestDepth) : (circuit layout codes valid keys sourceKeys sourceFlags recordCount payloads positive fits).size = (SelectRows.circuit (MenuClean.circuit layout codes valid keys sourceKeys sourceFlags recordCount) payloads positive fits).size

circuit has exactly the gates of SelectRows.circuit; the surrounding wiring adds none.

theorem Algebraic.MassProduction.Nonuniform.MenuSelection.circuit_selects {menuDepth requestDepth slots depth groupWidth inputs keyWidth sources padding routingDepth payloadWidth needed : ℕ} (layout : Fin (Sorting.networkRecords menuDepth) × Fin (Sorting.networkRecords requestDepth) × Fin slots ≃ Fin (Sorting.networkRecords depth)) (codes : Fin (Sorting.networkRecords menuDepth) → Fin groupWidth → Bool) (codesInjective : Function.Injective codes) (valid : Fin (Sorting.networkRecords depth) → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (recordCount : sources + Sorting.networkRecords depth + padding = Sorting.networkRecords routingDepth) (payloads : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth) → Fin payloadWidth → DeMorgan.Wiring inputs) (positive : 0 < needed) (fits : needed ≤ Sorting.networkRecords requestDepth) (input : Fin inputs → Bool) (withinRequest : ∀ (candidate : Fin (Sorting.networkRecords menuDepth)) (request : Fin (Sorting.networkRecords requestDepth)) (left right : Fin slots), DeMorgan.Wiring.eval input (valid (layout (candidate, request, left))) = true → DeMorgan.Wiring.eval input (valid (layout (candidate, request, right))) = true → ((fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys (layout (candidate, request, left)) bit)) = fun (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (keys (layout (candidate, request, right)) bit)) → left = right) (available : ∃ (candidate : Fin (Sorting.networkRecords menuDepth)), needed ≤ Nat.card { request : Fin (Sorting.networkRecords requestDepth) // RequestClean layout valid keys sourceKeys sourceFlags input candidate request }) (distinct : ∀ (candidate : Fin (Sorting.networkRecords menuDepth)), Function.Injective fun (request : Fin (Sorting.networkRecords requestDepth)) (bit : Fin payloadWidth) => DeMorgan.Wiring.eval input (payloads (finProdFinEquiv (candidate, request)) bit)) : ∃ (candidate : Fin (Sorting.networkRecords menuDepth)) (order : Equiv.Perm (Fin (Sorting.networkRecords requestDepth))), (∀ (request : Fin (Sorting.networkRecords requestDepth)) (bit : Fin payloadWidth), Sorting.flatRecords ((circuit layout codes valid keys sourceKeys sourceFlags recordCount payloads positive fits).eval DeMorgan.interpretation input) request (Fin.natAdd 1 bit) = DeMorgan.Wiring.eval input (payloads (finProdFinEquiv (candidate, order request)) bit)) ∧ ∀ (request : Fin (Sorting.networkRecords requestDepth)), ↑request < needed → RequestClean layout valid keys sourceKeys sourceFlags input candidate (order request)

The chosen candidate preserves all request payloads and has a clean prefix of the requested size. Distinct payloads can be ensured by hardwired request identifiers.

theorem Algebraic.MassProduction.Nonuniform.MenuSelection.circuit_cost_le {menuDepth requestDepth slots depth groupWidth inputs keyWidth sources padding routingDepth payloadWidth needed : ℕ} (layout : Fin (Sorting.networkRecords menuDepth) × Fin (Sorting.networkRecords requestDepth) × Fin slots ≃ Fin (Sorting.networkRecords depth)) (codes : Fin (Sorting.networkRecords menuDepth) → Fin groupWidth → Bool) (valid : Fin (Sorting.networkRecords depth) → DeMorgan.Wiring inputs) (keys : Fin (Sorting.networkRecords depth) → Fin keyWidth → DeMorgan.Wiring inputs) (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceFlags : Fin sources → DeMorgan.Wiring inputs) (recordCount : sources + Sorting.networkRecords depth + padding = Sorting.networkRecords routingDepth) (payloads : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth) → Fin payloadWidth → DeMorgan.Wiring inputs) (positive : 0 < needed) (fits : needed ≤ Sorting.networkRecords requestDepth) : (circuit layout codes valid keys sourceKeys sourceFlags recordCount payloads positive fits).cost DeMorgan.standardCost ≤ 256 * Sorting.networkRecords depth * (depth + (groupWidth + (1 + keyWidth)) + 1) ^ 5 + 128 * Sorting.networkRecords routingDepth * (routingDepth + keyWidth + 1 + 2) ^ 5 + 2 * Sorting.networkRecords depth + Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth * (slots + 1) + (Sorting.networkRecords menuDepth * (48 * requestDepth * requestDepth * Sorting.networkRecords requestDepth * (1 + payloadWidth)) + 48 * menuDepth * menuDepth * Sorting.networkRecords menuDepth * (1 + CandidateSelection.rowBits requestDepth payloadWidth))

Explicit bound for the full enumerated-menu evaluator and selector.