Repository navigation
Research: independent COPY floor for arbitrary one-column P112 corrections - #1468
Conversation
|
Batch review at Merged to Reviewed scope: All-pair P112 singleton-sided free-correction COPY64 theorem for arbitrary complex GL3 mixing, including the charged pure-factor branch. Independent exact geometric premises and complete decoder fixtures pass; other rectangles and shared-COPY contracts remain outside this proof. 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. |
An arbitrary free correction on one P112 column can invalidate the earlier rank-eight-per-child argument. This independent proof still bounds the complete COPY power bill when any two original coordinate terms and that correction are mixed by any
GL(3,C)change of factors. All 28 coordinate pairs, 112 singleton sites, arbitrary complex amplitudes and every subset of the 52 odd neighbors are covered; transposition gives one-row corrections. Six original terms remain fixed.The three replacement ranks satisfy
sum r_j^q >= 2*8^qfor every0<q<=1. The complete COPY sum has sharp floor 64, and the complete power bill has sharp floor 8*8^q, attained by identity mixing for every allowed correction. The proof accounts for the pure correction factor through lower envelopes(8,8,0),(6,6,6)or(6,6,4)and uses the coupled inverse-factor identity. Added physical overhead is optimistically zero for this COPY screen; width, normalization, multiplicity and separate charging remain fixed.Only
research/p112-column-correction-floor/is added (14 files): written proof, explicit task/source/replay metadata, complete certificate, two geometry representations, exact Gaussian-rational full-decoder examples and controls.Validation:
6d621ea5ffffc4079cc50a8bf4a0e4d83305ec48ce78b7d95e844da97a4c0627; all runtime input bytes remain unchanged. Semantic mutations, real source/receipt corruption, source pins, package selection and clean patch application pass.Overlap and attribution: commdata2338's PR1375 supplies the small-rectangle theorem, support/erasure method and 24-row boundary; Cinna Davis's PR1373 supplies the three-active branch for pair (4,6); Arham Tahir's PR1331 supplies the earlier handoff. The final refresh found Hanson Sun/bbMisk's PR1432 (
4bcc49e3f4041018b0607da46a87d8928a6e0fd0), which already proves the fixed 24-row case and the same(7,8,7)example, and PR1460 (8d53667d9bb09d9b1ffb0f865b5c8dc230eb02f6), an independent arbitrary-rectangle compensation bound at (4,6). Those findings are credited; this package provides an independently derived all-pair one-column proof and complete certificate. No pending theorem or code is assumed. Discussion1360's all-nine-factor singleton completion and the newer two-column claim are also recorded. The final overlap snapshot covered 824 open PRs and 159 discussion records, fully paginated.One OS draw selected
complex-mechanisms / complex-masked-decoder, nonce149d7583c4efedede03fc432c003699f, scope key2a6f2c726b78f9ae7d26, priority revision 2. The required complex-field starting example passed. Discussion1434 records the refined scope and handoff. Research and refreshed submission base are410026dc5513b87db92ae98571d1d5984c69a983, with both live inputs unchanged.Reproduce:
Limits: this package does not prove a floor for general two-sided rectangles, more mixed coordinates, other punctures or shared COPY billing. No physical word, frame/restoration schedule, owner/hosting admission, native run, selected cold replay, precision/tape, all-size compiler or analytic transfer is supplied. The universal argument is written, not proof-assistant checked. No new supplier or improved κ. Hosted CI and maintainer review remain separate from local validation.
Retains credit to Mihir Srivastava/PR845, DreamingOfClouds/PR717/446/595, GamingPuzzled/PR620, themilkman216/PR968 and woklerx/PR1077/1180. New work by Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance in mathematics, both implementations, tests and writing; Apache-2.0. No subagents or independent human review.