Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

The affine partition flag maximum

Abstract

The flag partition maximizes the squared sizes of affine parts outside the origin.

Definition 1.1 (Affine partitions of the punctured vector space).

Formalization. D5/S3/Quantum/Magic/AffinePartitionFlagMaximum.isAffinePartition (✓ std3).

Citation. Arne Heimendahl; Markus Heinrich; David Gross (2022). The axiomatic and the operational approaches to resource theories of magic do not coincide. DOI: 10.1063/5.0085774. URL: https://arxiv.org/abs/2011.11651v3.

Commentary.

A finite family of affine subspaces is an affine partition when every part is nonempty, distinct parts are disjoint, and a vector is nonzero exactly when it belongs to one of the parts. This is the partition condition in the source’s stabiliser-operation lemma (lines 986–994).

Definition 1.2 (The squared-cardinality objective).

Formalization. D5/S3/Quantum/Magic/AffinePartitionFlagMaximum.sqSum (✓ std3).

Citation. Arne Heimendahl; Markus Heinrich; David Gross (2022). The axiomatic and the operational approaches to resource theories of magic do not coincide. DOI: 10.1063/5.0085774. URL: https://arxiv.org/abs/2011.11651v3.

Commentary.

sqSum adds the squares of the cardinalities of the affine parts. It is the quantity appearing in the source’s overlap bound (lines 1209–1217).

Definition 1.3 (A coordinate flag cell).

Formalization. D5/S3/Quantum/Magic/AffinePartitionFlagMaximum.flagCell (✓ std3).

Citation. Arne Heimendahl; Markus Heinrich; David Gross (2022). The axiomatic and the operational approaches to resource theories of magic do not coincide. DOI: 10.1063/5.0085774. URL: https://arxiv.org/abs/2011.11651v3.

Commentary.

For an index i and a nonzero or zero coordinate value x, flagCell p n i x consists of vectors whose coordinates before i vanish and whose i-th coordinate equals x. It is the affine tail described by the source’s first-nonzero-coordinate construction (lines 1219–1232).

Definition 1.4 (The partition by first nonzero coordinate).

Formalization. D5/S3/Quantum/Magic/AffinePartitionFlagMaximum.flagPartition (✓ std3).

Citation. Arne Heimendahl; Markus Heinrich; David Gross (2022). The axiomatic and the operational approaches to resource theories of magic do not coincide. DOI: 10.1063/5.0085774. URL: https://arxiv.org/abs/2011.11651v3.

Commentary.

flagPartition is the image of all pairs (i,x) with i in Fin n and x a nonzero element of ZMod p under the flag-cell construction. It encodes the measurement procedure and induced partition in the source (lines 1219–1232).

Definition 1.5 (The value of the flag partition).

Formalization. D5/S3/Quantum/Magic/AffinePartitionFlagMaximum.flagValue (✓ std3).

Citation. Arne Heimendahl; Markus Heinrich; David Gross (2022). The axiomatic and the operational approaches to resource theories of magic do not coincide. DOI: 10.1063/5.0085774. URL: https://arxiv.org/abs/2011.11651v3.

Commentary.

flagValue p n is the finite sum ∑ₖ₍₀≤k<n₎ (p−1)p^(2k), the squared-cardinality value stated for the flag partition in the source (lines 1233–1237).

Definition 1.6 (The flag partition maximum conjecture).

Formalization. D5/S3/Quantum/Magic/AffinePartitionFlagMaximum.claim (✓ std3).

Citation. Arne Heimendahl; Markus Heinrich; David Gross (2022). The axiomatic and the operational approaches to resource theories of magic do not coincide. DOI: 10.1063/5.0085774. URL: https://arxiv.org/abs/2011.11651v3.

Commentary.

For every prime p and natural n, the flag cells form an affine partition of the nonzero vectors, their squared-cardinality sum is flagValue, and every affine partition has no larger squared-cardinality sum. This is the source’s maximising-measurement conjecture under the formal reading that all affine partitions are admitted (lines 1215–1232).

Theorem 1.7 (The affine partition flag maximum is proved).

Proof. Machine-checked in Lean as D5/S3/Quantum/Magic/AffinePartitionFlagMaximum.result (✓ std3). ∎

Resolves. Problems/heimendahl-heinrich-gross-2022-affine-partition-flag (proved) by D5/S3/Quantum/Magic/AffinePartitionFlagMaximum.result.

Source. Repository-derived.

Acknowledgement. Arne Heimendahl; Markus Heinrich; David Gross (2022). The axiomatic and the operational approaches to resource theories of magic do not coincide. DOI: 10.1063/5.0085774. URL: https://arxiv.org/abs/2011.11651v3.

Commentary.

The proof first identifies the cardinality of every nonempty affine part with p raised to the finrank of its direction, and uses disjointness and coverage to show that the part sizes sum to p^n−1. It then introduces a digit potential formed from the base-p digits of s. Its step, affine, and one-unit identities yield the power inequality p^(2k) plus the potential of s−p^k is at most the potential of s whenever p^k ≤ s. Induction over a finite family of powers of p gives the squared-size bound by the potential of the total size, and induction on n evaluates the potential at p^n−1 as flagValue p n.

The flag-cell center Pi.single i x proves nonemptiness; the least nonzero coordinate of a vector gives the unique flag index, proving disjointness and covering exactly the nonzero vectors. Each cell is the space of extensions of Pi.single i x on the record Finset.Iic i. The general record_extension_card theorem gives its cardinality p^(n−1−i). Summing over i and over the p−1 nonzero coordinate values gives flagValue. Combining these facts with the digit-potential bound proves claim (arXiv TeX lines 1219–1245).

References