Constructive Cauchy–Davenport

Every explicitly decoded entry of a genuine bit prefix is zero or one.

Membership in a genuine finite characteristic set is constructively decidable.

Every positive witnessed bit count supplies an actual bounded member.

Actual subset inclusion gives pointwise monotonicity of the characteristic bits.

Subset inclusion implies the exact inequality between the two witnessed finite cardinalities.

The two genuine finite-order witnesses add componentwise.

A strict left inequality and weak right inequality give a strict sum inequality.

A weak left inequality and strict right inequality give a strict sum inequality.

Every genuinely decoded summand is bounded by the exact finite sum containing it.

An actual bounded member rules out zero for the witnessed set cardinality.

A genuine strict pointwise witness makes otherwise monotone finite sums strictly ordered.

A witnessed missing member makes a proper subset strictly smaller in exact cardinality.

If a bit count is not the ambient size, finite search returns an actual zero position.

A characteristic set with at least two elements has a genuine nonzero canonical member.

A pointwise four-prefix balance gives the exact corresponding balance of all four finite sums.

The product of two actual zero-or-one values is again zero or one.

An actual pointwise product code has exactly the membership of the finite-set intersection.

Construct an actual characteristic intersection code and its exact finite count.

Construct the genuine characteristic complement and prove its count adds to the ambient size.

Membership in the constructed complement is exactly constructive nonmembership in its source.

Actual characteristic complements and intersection construct the exact union by decidable finite De Morgan reasoning.

Construct an actual beta characteristic union and a genuinely witnessed finite cardinality.

The two characteristic-bit values are constructively distinct.

For an actual decoded entry, being one is exactly characteristic membership.

Constructive nonmembership at a bounded index exposes its actual zero bit.

The exact finite Boolean union/intersection truth table preserves the sum of the two input bits.

The genuinely counted union and intersection have cardinalities summing exactly to those of both inputs.

Construct an actual finite beta code for composition of two arbitrary decoded beta functions.

Construct actual canonical modular-translation indices by a range code and genuine quotient/remainder recoding.

Every actual decoded modular-translation index has the canonical bound and the required congruence.

Canonical modular translation is a genuinely beta-coded bounded injection and hence a finite permutation.

The actual modular pullback of a characteristic prefix remains an actual characteristic prefix.

The constructed value-level composition has exact two-way modular-set pullback membership.

Construct the genuine modular pullback set and prove its exact cardinality is unchanged by the finite permutation.

A decoded zero bit excludes characteristic membership without any additional decidability assumption.

Every natural has an actual canonical balanced residue at every nonzero modulus.

A canonical residue has a genuine natural additive complement, including the zero boundary.

Opposite additive shifts invert one another in balanced modular arithmetic by explicit witnesses.

Exact pullback membership constructs and reflects an actual canonical source member.

A coded inverse pullback is exactly the forward translate, with actual source-member witnesses.

Moving a common shift between two summands preserves their exact modular sum.

The literal beta code (0,0) decodes zero at every natural index.

The literal zero code is an actual empty characteristic set with an exact zero sum trace at every ambient size.

The actual empty code is exactly the sumset restricted to the empty second-coordinate prefix.

Skipping an actually absent second-coordinate bit preserves the exact partial sumset.

Adjoining the actual translated first set at a present second-coordinate bit gives the exact next partial sumset.

Genuine finite induction constructs every bounded prefix of the exact modular sumset, including all beta codes and cardinality traces.

Every pair of actual finite modular sets has an actual canonical sumset code with a witnessed exact cardinality.

An exact actual sumset contains each witnessed canonical sum of input members.

Adding the modulus preserves balanced congruence with explicit zero/one witnesses.

An actual bounded inverse proves that every nonzero prime-field step reaches every residue from a given canonical start.

Finite orbit induction either proves membership at the reached residue or constructs an actual first-exit edge.

Every nonempty proper prime-field characteristic set has a witnessed boundary in each nonzero additive direction.

The actual union with a genuine forward translate has exactly the upper Dyson-transform membership.

The genuine pullback of A intersection (B+e) is exactly B intersection (A-e), with actual canonical witnesses.

Construct both actual Dyson-transform sets and their exact cardinalities, preserving the sum of the two input sizes.

The upper Dyson transform contains every actual member of the original first set.

The lower Dyson transform is an actual subset of the original second set.

When zero belongs to B and the shift belongs to A, zero genuinely belongs to the lower Dyson set.

An actual translation-boundary direction is absent from the lower Dyson transform.

Every actual sum from the Dyson pair remains in every coded upper set of the original sumset.

An actual boundary transform keeps both sets nonempty and strictly decreases the second exact cardinality.

When zero is a genuine second-set member, the first set is an actual subset of every upper sumset.

The normalized singleton case has the exact Cauchy--Davenport bound by genuine subset counting.

A normalized nontrivial second set and a non-full upper sumset construct an actual boundary suitable for strict Dyson descent.

Ordinary bounded induction on the actual second-set cardinality proves the full normalized Cauchy--Davenport bound using genuine strict Dyson descent.

Every normalized nonempty prime-field pair has the sharp bound against every actual coded upper sumset.

Pulling back by an actual source member produces an actual set containing zero.

Opposite actual translations of the input sets preserve every coded upper bound for their sumset.

Full Cauchy--Davenport for arbitrary nonempty prime-field characteristic sets, against every actual coded upper sumset.

Exact campaign G051: every actual sumset of two nonempty finite prime-field sets satisfies m >= min(p,k+l-1), in subtraction-free HA form.

Construct the actual canonical sumset and its exact cardinality together with the full sharp Cauchy--Davenport bound.