Selecting a candidate from computed clean flags

The clean-flag circuit is evaluated once, request payloads are attached by free wiring, and the complete candidate-selection circuit chooses one row. All original records survive as a permutation; the required prefix is clean.

def Algebraic.MassProduction.Nonuniform.SelectRows.circuit {inputs menuDepth requestDepth payloadWidth needed : ℕ} (flags : Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth)) (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)

Compute the clean flags, attach payloads, and select one complete row.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.SelectRows.circuit_size {inputs menuDepth requestDepth payloadWidth needed : ℕ} (flags : Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth)) (payloads : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth) → Fin payloadWidth → DeMorgan.Wiring inputs) (positive : 0 < needed) (fits : needed ≤ Sorting.networkRecords requestDepth) : (circuit flags payloads positive fits).size = (FlaggedRows.circuit flags payloads).size + (CandidateSelection.circuit menuDepth requestDepth payloadWidth needed positive fits).size

Row selection has exactly the gates of the flagged rows followed by candidate selection.

def Algebraic.MassProduction.Nonuniform.SelectRows.record {inputs menuDepth requestDepth payloadWidth : ℕ} (flags : Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth)) (payloads : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth) → Fin payloadWidth → DeMorgan.Wiring inputs) (input : Fin inputs → Bool) (candidate : Fin (Sorting.networkRecords menuDepth)) (request : Fin (Sorting.networkRecords requestDepth)) : Fin (1 + payloadWidth) → Bool

One original flagged record, with its complete payload.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.SelectRows.circuit_selects {inputs menuDepth requestDepth payloadWidth needed : ℕ} (flags : Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth)) (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) (available : ∃ (candidate : Fin (Sorting.networkRecords menuDepth)), needed ≤ Nat.card { request : Fin (Sorting.networkRecords requestDepth) // flags.eval DeMorgan.interpretation input (finProdFinEquiv (candidate, request)) = true }) : ∃ (candidate : Fin (Sorting.networkRecords menuDepth)), Sorting.Semantics.SequencePermutes (Sorting.flatRecords ((circuit flags payloads positive fits).eval DeMorgan.interpretation input)) (record flags payloads input candidate) ∧ ∀ (request : Fin (Sorting.networkRecords requestDepth)), ↑request < needed → FlagSelection.flag ((circuit flags payloads positive fits).eval DeMorgan.interpretation input) request = true

The output permutes one candidate's original records and has a clean prefix.

theorem Algebraic.MassProduction.Nonuniform.SelectRows.circuit_selects_indices {inputs menuDepth requestDepth payloadWidth needed : ℕ} (flags : Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth)) (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) (available : ∃ (candidate : Fin (Sorting.networkRecords menuDepth)), needed ≤ Nat.card { request : Fin (Sorting.networkRecords requestDepth) // flags.eval DeMorgan.interpretation input (finProdFinEquiv (candidate, request)) = true }) (distinct : ∀ (candidate : Fin (Sorting.networkRecords menuDepth)), Function.Injective (record flags payloads input candidate)) : ∃ (candidate : Fin (Sorting.networkRecords menuDepth)) (order : Equiv.Perm (Fin (Sorting.networkRecords requestDepth))), (∀ (request : Fin (Sorting.networkRecords requestDepth)), Sorting.flatRecords ((circuit flags payloads positive fits).eval DeMorgan.interpretation input) request = record flags payloads input candidate (order request)) ∧ ∀ (request : Fin (Sorting.networkRecords requestDepth)), ↑request < needed → flags.eval DeMorgan.interpretation input (finProdFinEquiv (candidate, order request)) = true

Distinct request payloads give an actual permutation of request indices. Every accepted index is one of the original clean requests.

theorem Algebraic.MassProduction.Nonuniform.SelectRows.circuit_cost_le {inputs menuDepth requestDepth payloadWidth needed : ℕ} (flags : Circuit DeMorgan.signature inputs (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth)) (payloads : Fin (Sorting.networkRecords menuDepth * Sorting.networkRecords requestDepth) → Fin payloadWidth → DeMorgan.Wiring inputs) (positive : 0 < needed) (fits : needed ≤ Sorting.networkRecords requestDepth) : (circuit flags payloads positive fits).cost DeMorgan.standardCost ≤ flags.cost DeMorgan.standardCost + (Sorting.networkRecords menuDepth * (48 * requestDepth * requestDepth * Sorting.networkRecords requestDepth * (1 + payloadWidth)) + 48 * menuDepth * menuDepth * Sorting.networkRecords menuDepth * (1 + CandidateSelection.rowBits requestDepth payloadWidth))

The flag computation is charged once; both selection sorts have their explicit linear record-count bounds.