[unpaidmoon]

Change and mathematical scope

Negative result for monotonicity of the fixed L/2 firing set. No new κ. Selected conditional κ stays 0.001672660197076918.

For a nonzero linear functional, the fixed substitution fires when base(n, L) < excess <= base + d^2, with base(n, L) = (L/2)*(L/2-1) - (2^{n-1}-1). The firing set at (n, L) is the set of masks that fire on at least one canonical simple restored universal word.

On F_2^4, every level set is an affine 3-flat. Subset excesses of an 8-point flat are at most 0,0,0,0,3,3,8,14,21 for sizes 0 through 8. Every 14-point set splits as (8,6) or (7,7), so its excess is at most max(21+8, 14+14) = 29. base(4,14) = 35, and 29 < 35. The full space splits (8,8) with excess 42 < base(4,16) = 49. So every 14-point subset, and the full 16-point space, is sound for every nonzero linear functional. This bound is not a walk hypothesis: the canonical census still finds 392 universal words at length 14 and 112 at length 16, and none fire.

The canonical firing-set sizes are 9,10,13,0,0 at n=4 lengths 8,10,12,14,16. Lengths 8, 10 and 12 are strictly nested, and lengths 14 and 16 are empty. Monotonicity fails. Witness 010201031213 has prefix states 0,1,3,2,6,7,5,4,12,14,10,8, returns to 0, and mask 1 splits them (8,4) with excess 24, so 23 < 24 <= 27. CrocSwap#3733 records 16 such mask-1 words at (4,12). The same mask fires on no 14-point set.

At n=5 the firing set is still monotone through length 16: 24 masks at length 12, then the same 25 masks of weight at most 3 at lengths 14 and 16. Mask 11010 is silent at length 12, fires 170 times at length 14 and 1728 times at length 16. No weight-4 or weight-5 mask fires.

This is a finite certificate at n=4 (every subset, not only walks) plus a finite census at n=5. It is not a multiplication theorem, not a repair of a retained seven-label exclusion, and not a statement that the firing set eventually becomes empty for every n.

Task and overlap

Base commit 12fa8c5c844be21bfefb38a19503fbd867a11244 (autoresearch revision 7). This fork PR is based on cursor/upstream-main-pin-a7d3, which points at that commit, so the diff is only this package. Fork main is a different history.

Task census-pruning-audit, scope refined. The chronological CrocSwap#1166 handoff taken is comment 19022438, handoff 1: whether the firing set is monotone in L for fixed n, first step (4,14) and (5,16). Handoff 2 of that comment is already CrocSwap#4148 (codimension-one soundness on double transversals) and is not rerun. The (7,18) / (7,20) census from comment 19021170 stays open; the card assigns it a separate budget, and this package does not run it.

Nearest predecessors are CrocSwap#3699 (per-mask tables at (4,8), (4,10), (5,12)) and CrocSwap#3733 (tables at (4,12) and (5,14), and the monotone question). No open upstream PR and no other fork cursor/* branch classifies (4,14) or (5,16). The added value is the flat-excess proof of silence at those two n=4 lengths and the (5,16) firing set, which shows the n=4 drop is not copied through length 16.

Validation

Python 3.12, standard library only. From the repository root:

python3 -B research/f7-monotone-firing-classification/verify.py
python3 -B research/f7-monotone-firing-classification/test_verify.py
python3 -B scripts/research_package.py --package research/f7-monotone-firing-classification

verify.py checks the flat maxima, the caps 29 < 35 and 42 < 49, exact published per-mask counts through (5,14), the new censuses, the nesting failure, the witness bill, agreement of the bitset and set excess routes, and agreement of the canonical and unconstrained n=4 enumerators. It prints PASS_F7_MONOTONE_FIRING_CLASSIFICATION with firing sizes 9,10,13,0,0 and 24,25,25. test_verify.py prints PASS_F7_MONOTONE_FIRING_TESTS groups=3. The registered replay prints PASS_REGISTERED_RESEARCH_PACKAGE with outcome negative-result. A local CPython 3.12 run of verify.py finished in about one minute.

Author-checked only. No independent human review and no formal-kernel check.

Not run: survey(7,18), survey(7,20), (5,18), Lean, Docker, and the selected cold replay. (6,16) has 2,262,380 canonical closed words and was not classified.

Credit

The prefix walk is the PR943 model used by CrocSwap#2542, CrocSwap#2634 and CrocSwap#2691. Nicholas Stone wrote the word-census correction (CrocSwap#2973). Nick Petalas classified the functionals in CrocSwap#3699 and extended them through (5,14) in CrocSwap#3733; the monotone question is handoff 1 of discussion comment 19022438. CrocSwap#4148 proved the separate double-transversal statement and left this classification open. James Reed's bit-0 audit is CrocSwap#3096. Douglas Colkitt supplied the selected frontier this package does not change.

Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.

Open next questions

See research/f7-monotone-firing-classification/README.md.

1. For n=5, which even length first makes every functional sound? First step: classify (5,18) and compare with the 25 masks of weight at most 3. Blocker: length 16 already has 267,890 canonical closed words, and no general cap is proved.
2. Which functionals fire at (7,18) and (7,20)? That census can change a maintained exclusion. Blocker: the seven-label state count and the card's separate-budget rule. This package does not run it.
3. Does any n>5 repeat the n=4 collapse one step after every low-weight mask has started firing? Blocker: (6,16) is already 2,262,380 closed words, and no threshold theorem is proved here.

Workflow feedback (optional)

Basing the fork PR on cursor/upstream-main-pin-a7d3 keeps the review diff to this package. Fork main does not contain the current upstream history.