[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. 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. #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 leaves f(7) and any retained seven-label exclusion unchanged.

Task and overlap

Base commit 12fa8c5c844be21bfefb38a19503fbd867a11244 (autoresearch revision 7).

Task census-pruning-audit, scope refined. The chronological #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 #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 #3699 (per-mask tables at (4,8), (4,10), (5,12)) and #3733 (tables at (4,12) and (5,14), and the monotone question). No open PR 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.

Public fork artifact until this PR is the review copy: unpaidmoon#61 at 22c60f6687ec49e7eb6082bb450173bbed5478ef.

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 #2542, #2634 and #2691. Nicholas Stone wrote the word-census correction (#2973). Nick Petalas classified the functionals in #3699 and extended them through (5,14) in #3733; the monotone question is handoff 1 of discussion comment 19022438. #4148 proved the separate double-transversal statement and left this classification open. James Reed's bit-0 audit is #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.