Scheduled recovery from the low-degree resource table

This module joins the tensor-grid evaluation code to projective affine-line scheduling. It proves the semantic local-recovery gadget from the Boolean mass-production manuscript: every scheduled punctured line recovers its target symbol, and the greedy schedule can make all recovery sets in one group pairwise disjoint.

theorem Algebraic.MassProduction.evaluationCode_sum_puncturedLine {K : Type u_1} {Index : Type u_2} {Coordinate : Type u_3} [Fintype K] [Field K] [DecidableEq K] [CharP K 2] [Fintype Index] [DecidableEq Index] [Fintype Coordinate] [DecidableEq Coordinate] (nodes : Index → K) (message : (Coordinate → Index) → K) (degree : Fintype.card Coordinate * (Fintype.card Index - 1) < Fintype.card K - 1) (target : Coordinate → K) (direction : Projectivization K (Coordinate → K)) : evaluationCode nodes message target = ∑ point ∈ puncturedLine target direction, evaluationCode nodes message point

Every sufficiently low-degree evaluation-code symbol is the sum over any projective punctured line through it.

theorem Algebraic.MassProduction.paperEvaluationCode_sum_puncturedLine (K : Type u_1) [Fintype K] [Field K] [DecidableEq K] [CharP K 2] (dimension : ℕ) (dimensionPositive : 0 < dimension) (message : (Fin dimension → Fin (resourceGridWidth (Fintype.card K) dimension)) → K) (target : Fin dimension → K) (direction : Projectivization K (Fin dimension → K)) : paperEvaluationCode K dimension message target = ∑ point ∈ puncturedLine target direction, paperEvaluationCode K dimension message point

At the paper's canonical grid width, punctured-line recovery holds in every positive dimension.

theorem Algebraic.MassProduction.paperEvaluationCode_recoverySets (K : Type u_1) [Fintype K] [Field K] [DecidableEq K] [CharP K 2] (dimension : ℕ) (dimensionPositive : 0 < dimension) (message : (Fin dimension → Fin (resourceGridWidth (Fintype.card K) dimension)) → K) (targets : List (Fin dimension → K)) (directions : List (Projectivization K (Fin dimension → K))) (equalLength : directions.length = targets.length) : List.map (fun (set : Finset (Fin dimension → K)) => ∑ point ∈ set, paperEvaluationCode K dimension message point) (recoverySets targets directions) = List.map (paperEvaluationCode K dimension message) targets

Aligned target and direction lists recover every target code symbol.

theorem Algebraic.MassProduction.exists_disjoint_paperEvaluationCode_recovery (K : Type u_1) [Fintype K] [Field K] [DecidableEq K] [CharP K 2] (dimension : ℕ) (dimensionPositive : 0 < dimension) (message : (Fin dimension → Fin (resourceGridWidth (Fintype.card K) dimension)) → K) (targets : List (Fin dimension → K)) (cardBound : targets.length * (Nat.card K - 1) < Nat.card (Projectivization K (Fin dimension → K))) : ∃ (directions : List (Projectivization K (Fin dimension → K))), ValidSchedule targets directions ∧ List.map (fun (set : Finset (Fin dimension → K)) => ∑ point ∈ set, paperEvaluationCode K dimension message point) (recoverySets targets directions) = List.map (paperEvaluationCode K dimension message) targets

Under the exact direction-counting condition, every request list has a pairwise-disjoint schedule whose code-symbol sums recover the whole list.

theorem Algebraic.MassProduction.exists_disjoint_paperEvaluationCode_recovery_of_mul_card_lt (K : Type u_1) [Fintype K] [Field K] [DecidableEq K] [CharP K 2] (dimension : ℕ) (dimensionPositive : 0 < dimension) (message : (Fin dimension → Fin (resourceGridWidth (Fintype.card K) dimension)) → K) (targets : List (Fin dimension → K)) (cardBound : targets.length * Nat.card K < Nat.card (Projectivization K (Fin dimension → K))) : ∃ (directions : List (Projectivization K (Fin dimension → K))), ValidSchedule targets directions ∧ List.map (fun (set : Finset (Fin dimension → K)) => ∑ point ∈ set, paperEvaluationCode K dimension message point) (recoverySets targets directions) = List.map (paperEvaluationCode K dimension message) targets

Paper-facing form under the simpler condition requests * |K| < |projective directions|.