Skip to content

Count complete headers for nonidentity scalar Schur pivots - #5366

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
aliromman:codex/five-harder-20261023-r2-scalar
Oct 24, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
aliromman:codex/five-harder-20261023-r2-scalar

Conversation

@aliromman

Copy link
Copy Markdown
Contributor

This answers the nonidentity header-frequency question in Nick Petalas's PR #4785. It gives exact complete-header weights for every common nonzero scalar pivot, with the three shifts 0, lambda and 2lambda-1 and their collision cases. For the named F5 profile (1,2,2,2), d=2 and lambda=2, the fixed H=J2(3) case has 442368000 sharp splits. The full profile has 42577920000 sharp splits and conditional sharp probability 154/505. Each split has exactly |GL5(F5)| complete-header extensions.

The proof, executable law, receipt and source pins define the scope. The complete kappa calculation is unchanged. This is a one-block algebraic count; later guards, physical cover selection, header emission, paid consumption, native admission and outer recovery remain open. Prime-power q and the scalar equality class are supplied premises of the integer-only API.

Predecessor credit is explicit. @petalas supplies the scalar criterion and named caller, and the two-shift law in PR #4803 and its proof. @aliromman supplied the retained multi-shift law in Discussion #5261. The factor counts and completion argument come from ssafwann's PR #4678 and source. The new part is the nonidentity scalar weight and its actual nonbinary consumer, not the incidence formula or sharpness criterion.

Validation on CPython 3.12.13, standard library only:

python3.12 -B scripts/research_package.py --package research/scalar-pivot-header-counts
python3.12 -B scripts/check_research_commit.py --package research/scalar-pivot-header-counts

Both registered isolated, warning-strict normal and optimized modes pass PASS_SCALAR_PIVOT_HEADER_COUNTS. Five nonidentity matrix contexts cover 5683 matrices, including F4 and F8. An independent F4 split oracle checks all 4032 candidate pairs, constructs actual headers and Schur complements, and confirms 27 admissible sharp splits: 4860 complete headers, probability 3/112. Retained checks cover 25291 two-shift matrices, 11527 factor pairs, 382 product targets, five binary source comparisons and all 20160 binary GL4 headers. The generic q=4,d=12 case evaluates 455 strata over 2^288 matrices. Four disposable mutations reject in both modes before receipt comparison, including the wrong third shift and wrong half-scalar collision.

Committed bytes, direct ancestry for every source pin, official export integrity and both read-only Git-free export commands pass. All 16 exported files remain unchanged. The full-history wrapper, selected cold replay, native production run, Lean and Docker were not run. Independent human and proof-kernel acceptance remain open. Hosted CI is separate.

Base is canonical main 7c47256, priority7, refreshed before submission. Current public PR/Discussion bodies and relevant main notes were checked; arbitrary historical diffs and unpublished work remain unsearched. The earlier general-H gluing scope was handed off as corroboration for a concurrent claim. This PR adds only this package. Prepared by Ali Romman with substantial OpenAI Codex assistance in derivation, implementation, review and verification. Apache-2.0.

@jwr404

jwr404 commented Oct 23, 2026

Copy link
Copy Markdown
Contributor

Independent review (James Reed, with Claude Code). Head 78c04d885a7af3449baa1c57df3ae9be4ff489b6.

Verdict: the factor-count formulas and the named F₅ numbers are correct.

Brute force of U and A

My own code enumerates all pairs X ∈ F_q^(d×r), Y ∈ F_q^(r×d) and tallies XY per target T. It compares the counts with your U(r,d,ρ) = Σ_k G(d−ρ, k−ρ) I(r,k) q^(d(r−k)) and, restricted to X onto and Y injective, with A(r,d,ρ) = I(r,d) q^(ρ(r−d)) I(r−d, d−ρ).

Cases run, with (r, d) per field:

  • q = 2: (1,2), (2,2), (3,2), (3,1);
  • q = 3: (1,2), (2,2), (3,1);
  • q = 5: (1,2), (2,2).

Result: 931 targets, 0 mismatches. The checked targets include every rank ρ ∈ {0,1,2} and the r < d zero case of A.

Named F₅ caller (λ = 2, d = 2, profile (1,2,2,2))

  • T₀₀ = H − 3I (since 2λ − 1 = 3), T₁₀ = T₀₁ = 2I − H and T₁₁ = H. A(2,2,ρ) is nonzero only at ρ = 2, so sharpness needs H and 2I − H invertible, and r₀₀ = 1 forces rank(H − 3I) ≤ 1.
  • U(1,2,1) = 4 and A(2,2,2) = 480, so H = J₂(3) gives 4·480³ = 442,368,000. ✓
  • U(1,2,0) = 25 + 6·4 = 49. ✓
  • The rank-one N = H − 3I over F₅ number 144: 24 nilpotent and 30 per nonzero trace. Eigenvalues 3 + t and −1 − t exclude t = 2 and t = 4, which leaves 24 + 2·30 = 84. ✓
  • Full profile: (49 + 84·4)·480³ = 42,577,920,000, matching the README. ✓

The shift-collision bookkeeping (λ = 1 gives 2λ − 1 = λ; 2λ = 1 gives 0, only in odd characteristic) is right. The registered replay passes locally.

Not re-derived: the F₄ split/Schur oracle figures (4032 pairs, 4860 headers, 3/112) and the q = 4, d = 12 stratum count. The multi-shift incidence inversion rests on the convolution law I checked separately in #5365.

@Mister-Meeseeks
Mister-Meeseeks merged commit e36f783 into CrocSwap:main Oct 24, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants