Skip to content

Research: classify P112 sparse-lift equality and sharp all-active cost 65 - #1325

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
mightyOil:codex/astra-015-sparse-redundant-decoder
Oct 14, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
mightyOil:codex/astra-015-sparse-redundant-decoder

Conversation

@mightyOil

Copy link
Copy Markdown
Contributor

Mihir Srivastava's incorporated PR845 already proves that a real single lift with fixed P112 coordinate readers cannot beat copy cost 64. This scoped structural refinement fixes the ninth normal to the sum of three coordinate normals and classifies all minimum-cost per-root shifts: exactly t=0,r0,r1,r2, each using eight active terms. Requiring all nine terms active has sharp cost 65, attained by (8,8,8,8,8,8,8,8,1). Arbitrary complex row shifts are covered; the normal frame is fixed.

The added package contains a written universal argument with two complete finite compatibility lemmas, exact witnesses and a separate affine-plane/rank-nullity implementation. It checks 32,385 binary planes and 765 single functions, plus every entry of five sharp decoder witnesses. It claims neither priority for the 64 floor nor a general nine-normal theorem. No physical supplier, changed paid histogram, moment barrier or new kappa is claimed.

Validation: full registered Python 3.12.13 replay, six package test groups, optimized Python 3.14.7 replay, receipt/source corruptions, read-only relocation, 20 research tests (one existing skip), five selected-record regressions and source-integrity checks pass. Full selected cold replay, native admission, Lean, hosted-CI success and independent human review are not claimed.

Only research/sparse-redundant-decoder/ is added. Base bce54fb3f895cbe5cd4c0eb477c3afeed100190f; original OS seed 40. Reproduce:

python3.12 scripts/research_package.py --package research/sparse-redundant-decoder

Credit PR845/mihir-s-05 for the prior single-lift obstruction, PR620/GamingPuzzled for coordinate cost 64, PR1224/joaqcoo for the general representation, PR1248 for the deficiency-plane method, and the retained PR446/717/968/1077 lineage. PR1304's A8 P112 frame is distinct. Source heads, overlap and open questions are recorded in the package. Prepared for Philipp/@mightyOil with substantial OpenAI Codex GPT-6 Astra assistance in research, proof, implementation, checking and writing; Apache-2.0.

@Mister-Meeseeks
Mister-Meeseeks merged commit 5668c25 into CrocSwap:main Oct 14, 2026
61 checks passed
@Mister-Meeseeks

Copy link
Copy Markdown
Contributor

100-PR batch review at ba2d1cae64738891dd530b3526fb8ae3b25541aa.

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

Reviewed scope: Sparse ninth-normal decoder: complete cost-64 equality classification and sharp all-nine-active cost 65 for the fixed three-coordinate dependency. Exact independent compatibility censuses cover arbitrary complex row shifts, not all redundant decoders.

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.

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.

2 participants