[mightyOil]

This independently certifies the local phase algebra used by Charles Bethin’s PR1278. All 16 ordered phase pairs and the completed parent map/inverse hold as universal noncommutative block-polynomial identities, with an opaque shared scratch block of arbitrary dimension.

The check needs only four one-sided invariants: P e_y = Q e_y = e_y and e_x^T R = e_x^T S = e_x^T. All other blocks are independent indeterminates; no P/R or Q/S inverse cancellation is assumed. Four explicit invertible shear counterexamples show that omitting one of these invariants can break the displayed family while retaining the other three. The stronger source/target and factor-support conditions remain inputs to PR1278’s separate induction.

Status: independent algebraic verification; no new kappa. PR1278 already supplies the all-size interval theorem and phase formulas. This contribution replaces finite matrix sampling for this local obligation with exact typed free-polynomial normal forms and isolates weaker sufficient local hypotheses. It does not certify the full induction, rounded leaves, precision costs, supplier admission or multiplication theorem, and is not a proof-assistant formalization.

Reproduce

python3.12 scripts/research_package.py --package research/universal-dirty-phase-identities

Expected: PASS_REGISTERED_RESEARCH_PACKAGE research/universal-dirty-phase-identities outcome=completed.

Passed with CPython 3.12.13: 18 universal identities, 18 stronger source-template checks, 540 independent full-matrix substitutions (including unequal data/scratch dimensions and zero scratch), four concrete counterexamples and six package tests. Tests reject actual source, certificate, dense-receipt and noncommutative-order faults, support read-only-file relocation, regenerate byte-identically, and refuse overwrite. Selected-record binding and all 25 existing selected-record tests also pass. No selected cold replay or hosted CI result is claimed.

Source and overlap

Base dadfea6e8a78ff6ba901705f87532a71c6f5bbb8; audited PR1278 head 06b8c006891ae78abe24b30d2fe9d8c188deafe8, with exact original proof, README, notice, Git-blob and SHA256 pins. Only research/universal-dirty-phase-identities/ is added. Final main refresh reached bdd4c63ac7c5d8a46ce070ba133df8d7ba9cb92c; selected record and relevant replay rules are unchanged. Final overlap refresh covered 803 open PRs and 21 discussions with complete comment pagination. The PR1278 head remained unchanged.

OS seed 81 selected independent verification. The original PR1244 follow-up was already solved by PR1278 during live selection; the scope was narrowed to universal algebra verification. Claim: #1166 (comment) . The README includes an explicit next obligation: machine-check dispatcher-to-template invariant preservation, separately from support induction and rounded-leaf substitution.

Credit Charles Bethin (PR1278), Hanson Sun (PR1244/1085), Chafik Boukhalfa (PR628/905), Gareth Davidson (PR877), and retained contributors. Prepared for Philipp / mightyOil with substantial OpenAI Codex (GPT-6 Astra) assistance in research, algebra, implementation, verification and writing. Apache-2.0; retained notices unchanged. No independent human review or literature-priority claim.

[Mister-Meeseeks]

100-PR batch review at 03025ca1d51091a9525203000e77dacccfa6a70d.

Merged to main, preserving the original contributor commits and package attribution.

Reviewed scope: Universal typed noncommutative identities under four one-sided interface constraints with arbitrary shared scratch. Exact symbolic checks cover the stated identities; no support-induction or multiplication theorem is inferred.

The pinned scoped command passed; the batch ledger contains its command, input hashes, environment and log. This incorporates the research/tooling contribution and does not change the selected κ or discharge the inherited multiplication-theorem assumptions.

Batch review, attribution and evidence. Thank you for the contribution.