Recovery from the constructive schedule

This module connects the explicit unrolled scheduler circuit to the abstract local-recovery identity. It proves that summing a resource over the actual request-major point records emitted by the circuit recovers every requested target value.

The resource codomain is kept abstract. In particular, this layer needs no new global finite-field or decidable-equality instances; classical equality is introduced only inside the finite-sum proof.

theorem Algebraic.MassProduction.ScheduledRecovery.scheduledLinePoint_injective_of_formula {width requests dimension : ℕ} (widthPositive : 0 < width) (output : Fin (requests * SchedulerIteration.lineBitWidth dimension width) → Bool) (targets : Fin requests → Fin dimension → BinaryExtension width) (directions : Fin requests → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (pointFormula : ∀ (request : Fin requests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)), SchedulerIteration.scheduledLinePoint widthPositive output request scalar = targets request + LineEnumeration.enumeratedNonzeroScalar scalar • normalizeBinaryExtensionVector (directions request).rep) (request : Fin requests) : Function.Injective (SchedulerIteration.scheduledLinePoint widthPositive output request)

Under the scheduler's pointwise line formula, different scalar positions decode to different emitted points.

theorem Algebraic.MassProduction.ScheduledRecovery.sum_scheduledLinePoint_eq_sum_scheduledLineSet {width requests dimension : ℕ} {valueType : Type u_1} [AddCommMonoid valueType] (widthPositive : 0 < width) (output : Fin (requests * SchedulerIteration.lineBitWidth dimension width) → Bool) (resource : (Fin dimension → BinaryExtension width) → valueType) (request : Fin requests) (injective : Function.Injective (SchedulerIteration.scheduledLinePoint widthPositive output request)) : ∑ scalar : Fin (LineEnumeration.nonzeroScalarCount width), resource (SchedulerIteration.scheduledLinePoint widthPositive output request scalar) = ∑ point ∈ SchedulerIteration.scheduledLineSet widthPositive output request, resource point

Summing over the scalar-indexed output records is the same as summing over the decoded finite recovery set, provided those records are distinct.

theorem Algebraic.MassProduction.ScheduledRecovery.greedyScheduleCircuit_recovers {width depth dimension : ℕ} {valueType : Type u_1} [AddCommMonoid valueType] (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (requests : ℕ) (allFit : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (capacity : requests * LineEnumeration.nonzeroScalarCount width < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (targets : Fin requests → Fin dimension → BinaryExtension width) (resource : (Fin dimension → BinaryExtension width) → valueType) (lineRecovery : ∀ (target : Fin dimension → BinaryExtension width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), resource target = ∑ point ∈ ForbiddenRanks.binaryExtensionPuncturedLine target direction, resource point) : ∃ (directions : Fin requests → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (∀ (request : Fin requests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)), SchedulerIteration.scheduledLinePoint widthPositive (SchedulerIteration.greedyScheduleOutput dimension widthPositive depth requests allFit targets) request scalar = targets request + LineEnumeration.enumeratedNonzeroScalar scalar • normalizeBinaryExtensionVector (directions request).rep) ∧ (∀ (request : Fin requests), SchedulerIteration.scheduledLineSet widthPositive (SchedulerIteration.greedyScheduleOutput dimension widthPositive depth requests allFit targets) request = ForbiddenRanks.binaryExtensionPuncturedLine (targets request) (directions request)) ∧ SchedulerIteration.PairwiseDisjointFamily (SchedulerIteration.scheduledLineSet widthPositive (SchedulerIteration.greedyScheduleOutput dimension widthPositive depth requests allFit targets)) ∧ ∀ (request : Fin requests), ∑ scalar : Fin (LineEnumeration.nonzeroScalarCount width), resource (SchedulerIteration.scheduledLinePoint widthPositive (SchedulerIteration.greedyScheduleOutput dimension widthPositive depth requests allFit targets) request scalar) = resource (targets request)

Exact recovery theorem for the concrete greedy scheduler circuit. Any resource family satisfying the punctured-line identity recovers all targets when read in the circuit's emitted request/scalar order.