Forbidden intersections

../

corollary_1_6: Derives the uniform-layer product bound from the fully weighted theorem.

definitions: Fixes the ambient normalization, pattern compatibility, and exponential losses.

entropy_estimates: Proves the binomial and factorial estimates used in the density arguments.

external_inputs: Separates Harper isoperimetry from background results not used as hidden dependencies.

large_set_construction: Proves the entropy-size construction from the introduction with integer thresholds.

lemma_4_1: Proves the popular-fiber estimate used throughout the counting refinements.

numerical_corollaries_scope: Records the exact advertised constants without certifying the omitted optimization or an unsupported coefficient.

product_measure_separation: Supplies the concentration estimate needed to expand the weighted deletion proof.

proposition_10_1: Derives the sharp product bound and characterizes equality.

proposition_10_4: Proves the arbitrary-field projection bound without a coordinate-basis assumption.

proposition_2_3: Proves the numerical inequality behind the unweighted branching step.

proposition_7_2: Proves the sufficient two-tolerance averaging form and records the source loss.

slice_separation: Supplies uniform proximity of dense layer families at the averaging endpoint.

source_scope: Inventories the complete chains, historical inputs, and uncompiled printed claims.

theorem_10_2: Proves the two parity bounds and the equality information used for constant intersections.

theorem_10_3: Proves the modular bounds using affine slices over the correct field.

theorem_10_5: Proves the affine-dimension bound and its strict improvement away from the middle distance.

theorem_11_1: Proves the odd-parameter lower bound and the elementary cyclic-window upper construction.

theorem_1_1: Deduces the exponential bound and handles the diagonal convention explicitly.

theorem_1_10: Completes the coding argument by constructing a positive integral pattern matrix.

theorem_1_11: Proves the full asymptotic cube argument and distinguishes the printed finite range.

theorem_1_13: Proves rotation averaging, the correct dimension comparison, and all finite endpoints.

theorem_1_14: Completes the noncircular reduction from arbitrary interior cell sizes to the middle layer.

theorem_1_15: Proves the complete partition-pair counting induction with all fiber thresholds.

theorem_1_16: Proves the full multiarray counting theorem used by the later simplex arguments.

theorem_1_4: Reconstructs the deletion argument with explicit stopping and parameter choices.

theorem_1_5: Completes the weighted deletion and complement arguments with uniform parameters.

theorem_1_7: Preserves the Section 4 counting proof and its transfer from a general dense family.

theorem_1_9: Proves the neighbor-family induction with distinct members and explicit eventual scope.

theorem_2_1: Proves the entropy product bound relative to the exact Harper input.

theorem_2_2: Proves the complementary entropy bound and its exponential consequence.

theorem_3_1: Proves monotonicity of up-sets and the weighted entropy bound.

theorem_6_1: Reconstructs the two-stage counting and fiber argument with the corrected fiber bound.

theorem_9_1_scope: Records Theorem 9.1 as printed and the exact feasible-array consequence that Theorem 1.16 proves.

weighted_deletion_inequality: Expands the biased branching step omitted from the source Section 3 sketch.

---

Peter Frankl and Vojtěch Rödl, Forbidden intersections, Transactions of the American Mathematical Society 300 (1), March 1987, 259–286. DOI.

The copy read for this card is the 28-page published scan, retrieved from Frankl's author archive on 2026-09-05. The source record gives that copy's identity, publication metadata, and version scope. The title-page received date, 24 October 1985, is distinct from the March 1987 publication date. No different manuscript version or author-issued erratum is asserted. The file prints "©1987 American Mathematical Society" on its first page (printed p. 259) and, in every page's footer, "License or copyright restrictions may apply to redistribution; see http://www.ams.org/journal-terms-of-use", every other right reserved.

The principal forbidden-intersection theorem says that, for any fixed positive buffer away from zero and half the ground-set size, forbidding one intersection size forces a family below $(2-\epsilon)^n$. The one-family proof and the stronger two-family product bound use an iterative deletion of coordinates while tracking a widening forbidden interval. The weighted proof in theorem_1_5 is expanded beyond the source's outline, including both bias regimes. The large-set construction provides the source's contrasting entropy lower bound.

The counting refinements pass through the middle-layer argument, the containing-set averaging lemma, and general two-set count to the matrix theorem and full joint-array theorem. The last result controls every atom of the intersection of several ordered partitions. It includes distinct families and compatible marginals, and gives a positive exponential fraction of the exact full-family count. This is the input used by the later simplex arguments; pairwise intersection estimates alone would not supply it.

The separate Section 4 method is preserved in theorem_1_7, followed by the weak delta-system induction, the asymptotic cube-orthogonality result, and the sphere bound. The coding proof constructs the positive integral pattern matrix needed by the source sketch. Section 10's constant-intersection, parity, modular, and constant-distance arguments are reconstructed, as is the Galvin-family bound.

The coverage record states the exact limits. In particular, the advertised numerical constants are not certified by the qualitative proofs, and the literal unrestricted Theorem 9.1 metric claim has a concrete obstruction. Theorem 1.11's proof is recorded in its proved eventual range; the printed finite range is not silently included. Theorem 1.18 is an announcement whose proof the source explicitly defers to another paper. None of these qualifications limits the fully expanded compatible joint-array theorem. Harper's isoperimetry and invariant rotation measure remain the precisely identified external inputs.

Bears on. #703 through the proportional forbidden-intersection bound; #174 through the joint-pattern input to the 1990 simplex source and the 2004 simplex source. These are source relationships, without a new problem-status claim.

No file of this source is held: no license on record permits its redistribution, and the card cites the edition it names above.