Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Charges and connectivity of original minimal zero supports

Abstract

Separated original minimal supports have nonzero designated-coordinate charge sums.

Theorem 1.1 (A singleton designated set).

Lean statement: D5/S3/Combinatorics/Sequenceability/BooleanRowChargeConnectivity.supportIntersectionGraphOutside_singleton

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Sequenceability/BooleanRowChargeConnectivity.supportIntersectionGraphOutside_singleton (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any finite family E of original supports, supportIntersectionGraphOutside E Q retains every vertex of E and joins distinct supports precisely when they share an original coordinate outside Q. When Q is the singleton {q}, this is exactly supportIntersectionGraph E q, with the same vertex identities and paths.

Theorem 1.2 (Separated components cannot cancel their designated charges).

Lean statement: D5/S3/Combinatorics/Sequenceability/BooleanRowChargeConnectivity.separated_component_charge_sum_ne_zero

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Sequenceability/BooleanRowChargeConnectivity.separated_component_charge_sum_ne_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let f label an arbitrary index type in an additive commutative group, let Y be a finite set of original indices, and let E contain exactly all proper inclusion-minimal nonempty zero supports in Y. Fix any finite designated set Q; it need not lie in Y. In supportIntersectionGraphOutside E Q, choose a finite nonempty family U of representatives in pairwise distinct components. Each selected support B must meet Q and have nonempty puncture B minus Q. Then the total charge, the sum over B in U of the sum of f(i) over i in B intersect Q, is nonzero. No incidence, injectivity, nonzero-label, finite-group, saturation or zero-sum-free hypothesis is imposed. Q-free and exception-only supports remain vertices of the graph; the two nonemptiness conditions exclude them only from U.

Component separation makes the selected punctures pairwise disjoint. Their union A has sum equal to the negative of the total designated charge. If that charge vanished, the original zero_decomposition union projection would supply a nonempty minimal zero block D through a puncture port of a fixed representative B0, with D contained in A. A designated coordinate of B0 is outside A, so D is proper in Y and belongs to E. Its port connects D to B0. Every coordinate of D belongs to another selected puncture and connects D to that representative. Separation forces each such representative to be B0, hence D is contained in B0. Original minimality forces D=B0, contradicting the designated coordinate omitted from A. This uses the cover of the single zero_decomposition_pairwise_disjoint recursion through its public union projection.

For any nonempty subfamily V of such a fixed family U, the hypotheses restrict to V. Applying the same theorem to V makes every nonempty charge subsum nonzero. Equal group values still count as distinct sequence entries when their original supports differ. If a selected support were contained in Q, its charge would be zero and the conclusion would fail; such supports are retained as graph vertices but excluded by the puncture condition.

All charges lie in the additive subgroup H generated by the finitely many designated labels f(i), i in Q. Conditional on H being finite and on the standard Davenport property that every length-D(H) sequence in H has a nonempty zero-sum subsequence, the nonzero-subsum conclusion bounds the number of eligible mixed components by D(H)-1. Exception-only components require separate accounting. This is a conditional standard consequence, not an additional formal invariant bound. No finite uniform bound is asserted for infinite H, and coefficient-one designated charges are not identified with signed star charges or used to infer charge-lattice saturation.

Theorem 1.3 (A two-charge connectivity inference).

Lean statement: D5/S3/Combinatorics/Sequenceability/BooleanRowChargeConnectivity.two_charge_supports_connected

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Sequenceability/BooleanRowChargeConnectivity.two_charge_supports_connected (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let Y be a finite set of original indices and let f label them in any additive commutative group. Let E contain exactly the proper subsets of Y that are inclusion-minimal nonempty coefficient-one zero supports for the original labels. The graph supportIntersectionGraph has every member of E as a vertex. Distinct vertices are adjacent exactly when they share an original index other than q. If f(q)+f(q)=0, any two vertices containing q have equal connected components. There is no finiteness assumption on the label group or ambient index type, and no injectivity, nonzero-label, incidence or fixed support-size hypothesis.

Suppose the two components differ. Their supports can intersect only at q. Minimality gives a non-q index i in the second support: otherwise that support is contained in the first, forcing equality. Delete q from their union. Its two disjoint erased pieces have sums -f(q), so the union has sum zero. It is nonempty and proper in Y. Apply DisjointMinimalZeroOrdering.zero_decomposition, the public union projection of zero_decomposition_pairwise_disjoint, to this set. The single finite-deletion recursion is retained in the strengthened supplier. Its union cover supplies an original minimal zero support B containing i. Every such block is a proper subset of Y and hence a vertex of E. Sharing i joins B to the second support. Any intersection of B with the first would join the separated components. Thus B lies in the second support; minimality forces equality, contradicting the exclusion of q. Pairwise disjointness of the decomposition is not used.

All vertices remain available along a path. In particular, with three indices, all labels one in ZMod 2, and Y the full index set, E consists of the three two-element supports. The two q-containing vertices connect through the third, q-free support. The induced graph on only the q-containing vertices is disconnected. The theorem therefore makes no induced-connectivity claim.

For the original integer row lattice M, take f(i)=M.mkQ(Pi.single i 1). The sum of these labels over a support is M.mkQ of its coefficient-one Boolean row. Consequently the original Complete predicate and its inclusion-minimality yield exactly the original MinimalZeroSupport vertices, with no coordinate identifications. Membership of twice the singleton row at q in M gives f(q)+f(q)=0. Under the separate original incidence-at-most-two hypothesis, two distinct rows sharing a non-q index force its incidence to equal two; this intersection graph then equals the ordinary graph that records twice-occurring original indices. These are applications of the general inference, not additional retained specialization theorems.

The support argument adapts Section 2 of the saved native single-ternary proof, SHA256 485b60f2f519cb1000e89ed96c65fe88c5667e689cb804c9d9ccf3838bf18740, as preserved in OriginalTwoChargeExclusion.lean, SHA256 228676b458e43ce51613181e7f39084f1f12e603f0408ee1b2a050c8dd8a4a16. The arbitrary-group formulation removes unnecessary draft hypotheses. No literature novelty is asserted. Full original Good, its unrestricted blocker, arbitrary-r residual, AM and the separate two-exception charge-lattice problem remain open.

References