Problem 5 of Brešar, Hedžet and Herrman: m(C_n × P_m, 2)

In r-neighbour bootstrap percolation a vertex becomes infected once it has at least r infected neighbours, and m(G, r) is the least size of a nonempty initial set that eventually infects every vertex. For the direct product C_n × P_m of a cycle and a path, Brešar, Hedžet and Herrman (arXiv:2403.10957, Discuss. Math. Graph Theory 46 (2026)) ask:

Problem 5. Determine m(C_n × P_m, 2).

Their Proposition 3 gives m(C_n × P_m, 2) ≤ n, and they note that equality appears to hold for small examples.

D5/S3/StatisticalMechanics/Percolation/DirectProductCyclePathBootstrap.result proves m(C_n × P_m, 2) = n for every n ≥ 3 and m ≥ 1.

Issue #10650 preregisters the readings, the proof route and the literature check. arXiv searches for bootstrap percolation and hull numbers on direct products return only the source paper and unrelated models, and the citing works found concern other graph families; the repository and pinned Mathlib have no bootstrap percolation. not-found-in-searched-scope.

1. The layer {(a, 0)} percolates: (a, b + 1) has the two distinct neighbours (a ± 1, b) in layer b.
2. With D(A) = Σ_{v ∈ A} |N(v) ∩ A|, one round adds a set B disjoint from A whose vertices each have at least 2 neighbours in A; double counting the adjacent pairs between A and B gives D(A ∪ B) ≥ D(A) + 4|B|, so 4|A| − D(A) never increases.
3. On the whole vertex set, deg(a, b) = 2 deg_{P_m}(b) and Σ_b deg_{P_m}(b) = 2(m − 1), so 4|V| − D(V) = 4n; a percolating set A satisfies 4n ≤ 4|A| − D(A) ≤ 4|A|.

The proof would fail if some round increased the potential of step 2, or if a set of fewer than n vertices percolated.

Exhaustive search over all vertex subsets gives m(C_n × P_m, 2) = n for n = 3, …, 6, m = 1, …, 4 (nm ≤ 20), and the layer {(a, 0)} percolates for 3 ≤ n, m ≤ 15; the same search reproduces the paper's values m(P_3 × P_4, 2) = 6 and m(P_4 × P_4, 2) = 8 (issue #10650).

The canonical source is D5/S3/StatisticalMechanics/Percolation/DirectProductCyclePathBootstrap.lean. Its public declarations are dirProd, step, Percolates, percolationNumber, claim and result, with decidability instances for the direct product and the path graph. The frozen module state has statement identity sha256:69d8f41abf99c351717ab3929380eec70a7a5d0805c4d6533a62b37ee8bea65f. The result declaration has statement identity sha256:66586e9d4df394e6f9789928ecbb3695154b9c7a20a4c55bc8dd3cdf247908e4. The Freeze event is sha256:84f19ee39d98dd6ac7ee9e9fa4d3a75047d093bf913158cb69c40d41e9a5bf4a. It has no project-level frozen prerequisite. The proof uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.

Tier 1 external named open problem, preregistered in issue #10650 before the probe. theorem; resolution proved. The public theorem has proof_shape: content: the monotonicity of the potential under a round of percolation and its value 4n on C_n × P_m are new propositions on the live proof path. Its admission basis is open-problem-resolution; utility none.

The bounded literature check does not establish exhaustive worldwide novelty, priority, or the absence of an independent proof.