From cd7afb9e812c84c1bc2e2034956256996e9b6c93 Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 18:07:48 +1100 Subject: [PATCH 1/2] research: prove P104 whole-fiber coverage and helper-inventory gate --- research/p104-coverage-gate/PROOF.md | 148 ++++++++++++++++++++ research/p104-coverage-gate/README.md | 98 +++++++++++++ research/p104-coverage-gate/RESULT.json | 113 +++++++++++++++ research/p104-coverage-gate/SOURCES.json | 36 +++++ research/p104-coverage-gate/TASK.json | 106 ++++++++++++++ research/p104-coverage-gate/VALIDATION.json | 26 ++++ research/p104-coverage-gate/VERIFY.json | 48 +++++++ research/p104-coverage-gate/independent.py | 58 ++++++++ research/p104-coverage-gate/test_verify.py | 91 ++++++++++++ research/p104-coverage-gate/verify.py | 148 ++++++++++++++++++++ 10 files changed, 872 insertions(+) create mode 100644 research/p104-coverage-gate/PROOF.md create mode 100644 research/p104-coverage-gate/README.md create mode 100644 research/p104-coverage-gate/RESULT.json create mode 100644 research/p104-coverage-gate/SOURCES.json create mode 100644 research/p104-coverage-gate/TASK.json create mode 100644 research/p104-coverage-gate/VALIDATION.json create mode 100644 research/p104-coverage-gate/VERIFY.json create mode 100644 research/p104-coverage-gate/independent.py create mode 100644 research/p104-coverage-gate/test_verify.py create mode 100644 research/p104-coverage-gate/verify.py diff --git a/research/p104-coverage-gate/PROOF.md b/research/p104-coverage-gate/PROOF.md new file mode 100644 index 0000000000..00a8a0bb36 --- /dev/null +++ b/research/p104-coverage-gate/PROOF.md @@ -0,0 +1,148 @@ +# Whole-fiber coverage and the conditional helper-sharing gate + +## Named model and source boundary + +This is a scoped theorem for selecting whole calls from the proposed 104 by +104, nine by nine tensor scaffold of PR3954, head +`f1e2839819959cd0534d008be91ed5b79ec55a6a`. It does not embed that scaffold in +the selected h=28 producer. The pinned canonical native-channel witness has +104 X ports, 104 Y ports and 72 arbitrary dirty helpers. A whole local word +uses every port. Its source and target dimension increments are eight each, +and its helper increment is nine: P=104*8+104*8+72*9=2312. The witness has +rank mass2368. We conditionally grant the corrected mass M=2368+208=2576 +from PR3882/3894/3940, including the unproved opposite orientation. No native +correction is independently recompiled here. + +As in PR3954, let p_i be the 104 distinct odd physical root labels in F2^9. +Each grid pair is the nondegenerate line span(p_i tensor p_j), in dimension +m=81. A first-axis call fixes j and uses every i; a second-axis call fixes i +and uses every j. Swapping the names row and column has no effect below. +This study uses only those exact incidence sets. It neither chooses a new +physical gauge nor grants a free permutation, source decoder or owner move. + +The retained caller in notes/copied-centers-complex.tex fixes two logical +stages S(x,y)=(x,x+y), R(x,y)=(x-y,y); the required composition is +R S(x,y)=(-y,x+y), before its paid physical correction and phase wrappers. +We grant the corrected calls this ideal unencoded logical interface to make +the pruning test favorable. Actual encoded boundaries remain obligations. + +## Whole-call closure theorem + +Select a row set A and column set B, of sizes a and b (0<=a,b<=104). +Their whole-word incidence union is + + U = (A x [104]) union ([104] x B), + N = |U| = 104(a+b)-ab. + +Exactly ab pairs receive both calls. Exactly + + d = 104(a+b)-2ab = a(104-b)+b(104-a) + +pairs receive one call. These are dangling endpoints. On any such pair the +logical map is S or R rather than R S. The differences are nonzero on arbitrary +inputs: at (x,y)=(1,0), S=(1,1), R=(1,0), and R S=(0,1). Chart changes cannot +turn this logical endpoint equality into a proof; any changed physical +completion must be established and billed separately. + +Consequently, if every touched pair must receive the retained two-stage +endpoint and no replacement completion is supplied, d=0 is necessary and +sufficient at the incidence level. Since each summand in d is nonnegative, +nonempty A forces b=104 and nonempty B forces a=104. The only closed masks +are empty or all208 calls. This is not an impossibility theorem for paid +native completion or a new partial-port word. A rectangle A x B is not the +support of these whole calls: removing its other incident ports changes the +word/interface. Treating them as padding still incurs their acquisition, +return and physical inventory obligations. + +## Most favorable complete-cost gate for every mask + +Now permit arbitrary replacement completion of dangling endpoints. Grant one +initial rank unit at every touched pair, including pairs whose retained +second stage is absent. This is an optimistic relaxation, not an established +physical initial/final boundary for the pruned caller. Let H be any number of +physical helper owners and W=2N+H. Helper owners may be reused at disjoint +times, provided the stated entrance/exit and progress hypotheses are retained. + +The named hypotheses are: every persistent owner must finish under full F; +touched data sources receive the N initial rank credits; each whole call has +mass at least M and net persistent progress at most P; remaining work has rank +tariff at least its net persistent dimension progress; child ranks are <=81; +and the equal physical-role normalization is1/W. Unknown acquisition, +intertwiners, completion, copy/add/disposal, routing, holding, control, tape, +precision and admission costs are nonnegative and additional. This is the +same conditional progress accounting used by PR3954; changed translated +frames that invalidate its P cap require a new proof, not this bound. + +For c=a+b calls, persistent progress required is81W-N. Remaining paid rank is +at least max(0,81W-N-cP). Therefore + + total rank >= cM + max(0,81W-N-cP) + >= 81W + c(M-P)-N. + +The excess over capacity is at least + + Delta = 264(a+b)-[104(a+b)-ab] = 160(a+b)+ab. + +Every nonempty mask has Delta>=160>0. Thus pruning whole calls cannot rescue +the unchanged corrected profile even with optimistic initial credits and free +new boundary work. For 0<=alpha<1 and 0<=r<=81, +(r/81)^(1-alpha)>=r/81, so the complete moment also exceeds one. +The full mask gives44096, reproducing the named source model as a boundary +case of the new all-mask theorem, not as its only evidence. + +H cancels from Delta. Hence reducing the number of helper owners by reuse, +while retaining these hypotheses, cannot reverse the rejection. This does +not establish legal helper reuse. In the actual retained caller arbitrary +dirty helpers are original inputs and must receive full F, including after +their last local use. Calling their local last use 'retirement' does not erase +the remaining endpoint. Deleting b such owners while retaining their b +independent arbitrary input arrays would contradict injectivity; transferring +their information to other owners changes capacity and requires a paid map. +Aliasing independent helpers across different calls reduces the declared +input space and is a different owner contract, which the conditional H-bound +already grants if all other hypotheses hold. Private COPY disposal is a +separate question and is not audited or newly lower-bounded here. + +## Exact criterion after an actual profile change + +Let e_R=M_R-P_R and e_C=M_C-P_C be proved per-call excesses for the two axes. +Let A>=0 denote additional paid rank with no already-counted progress. The +same relaxed numerator is + + Delta(a,b) = (e_R-104)a+(e_C-104)b+ab+A. + +At A=0 this is bilinear. Over [0,104]^2 its minimum occurs at a corner, by +minimizing each affine coordinate in succession. Equivalently its value is +the bilinear convex interpolation of its four corner values. Therefore a +nonempty mask can have negative relaxed Delta iff e_R<104 or e_C<104. +If at least one call from each axis is required, the corresponding corners +are (1,1),(1,104),(104,1),(104,104). Testing those four is exact. If the retained +two-shear endpoint must be incidence-closed, only the full corner remains: + + Delta_full = 104(e_R+e_C-104)+A. + +For a common excess e, a two-axis partial mask can pass the relaxed test iff +e<207/2=103.5, whereas an incidence-closed caller requires e<52 (and must pay A). +The first statement follows from ab/(a+b)>=1/2 for positive integers a,b, +with equality only at a=b=1; the second follows from a=b=104. + +A concrete discrimination control is e_R=e_C=100. Selecting one call per axis +produces relaxed Delta=-7, yet leaves206 dangling pairs. The complete closed +mask has Delta=9984. This is a warning against treating a passing sparse +relaxation as a constructed caller, not a lower bound on every possible paid +completion of those206 pairs. Even forgiving all208 correction units per call +leaves e=56, for which the closed-mask excess is832. That conditional arithmetic +is not a new COPY floor; PR3045 and the concurrent private-COPY audit own the +literal lifetime question. The earlier #3620 threshold concerns a different +caller and is not used in this proof. + +## Decision and remaining obligations + +NARROW: stop expansion of unchanged-profile partial-fiber and inventory-only +reuse variants. A reopening result must supply a changed excess/coverage law, +or disprove one named progress hypothesis with an actual translated call. +For sparse candidates it must also implement each dangling endpoint and all +encoded/physical owner boundaries, and include those costs in A. No scalar +incidence theorem proves physical supplier execution, signed-floor or finite +precision correctness, recursive admission, a new kappa or a universal P104 +barrier. No selected files or shared verification controls are changed. diff --git a/research/p104-coverage-gate/README.md b/research/p104-coverage-gate/README.md new file mode 100644 index 0000000000..0a23234625 --- /dev/null +++ b/research/p104-coverage-gate/README.md @@ -0,0 +1,98 @@ +# P104 whole-fiber coverage and helper-sharing gate + +**Scoped result:** selecting partial sets of whole P104 row/column calls cannot +rescue PR3954's unchanged corrected profile. The exact touched-pair count is +`N=104(a+b)-ab`; the optimistic rank excess is +`264(a+b)-N=160(a+b)+ab>0` for every nonempty mask. Reducing the helper-owner +count does not alter this numerator while the named progress/endpoint +hypotheses remain valid. No new kappa, native supplier or frontier change. + +There is also a separate endpoint obligation: the retained two-shear caller +has `104(a+b)-2ab` dangling pairs. Without a changed paid completion, the only +whole-call sets closed under its endpoint are empty or all208 calls. A smaller +rectangle is not the support of an unchanged104-port word. + +The proof gives an exact four-corner test for asymmetric changed profiles. +It distinguishes a passing sparse relaxation from an actual closed caller: +with hypothetical excess100 per axis, one call on each axis has relaxed +excess-7 but206 unresolved endpoints, while the full closed caller has +excess9984. These hypothetical profiles are discrimination controls, not +constructed improvements. The all-correction-free closed value832 is only +conditional arithmetic, not a new private-COPY lifetime floor. + +See [PROOF.md](PROOF.md) for the general incidence proof, source assumptions, +helper-potential cancellation, exact optimization criterion and stop decision. +[RESULT.json](RESULT.json) records the finite evidence. The conditional gate +explicitly grants full-array initial rank credits and leaves new physical +boundary costs nonnegative; it does not infer actual preparation for a +one-sided caller or physical legality of shared helpers. + +## Reproduction and evidence + +Python3.12, standard library only, from the repository root: + +```sh +python3 -B research/p104-coverage-gate/verify.py +python3 -B research/p104-coverage-gate/independent.py +python3 -O -B -m unittest discover -s research/p104-coverage-gate -p test_verify.py -v +python3 scripts/research_package.py --package research/p104-coverage-gate +``` + +The primary checker authenticates three canonical source inputs, recounts the +literal native witness's frame dimensions/rank histogram, and checks all11025 +count pairs. The separate checker imports no producer or primary verifier: +it explicitly forms incidence sets for21844 masks on grids of sizes1..7, +checks actual pair maps and rational asymmetric corner criteria. Seven tests (including six actual optimized CLI faults) +reject rank undercharging, missing ports and helper retirement, and distinguish +overcounted initial credits and an unclosed sparse pass. These finite tests +support the proof; they are not a formal theorem or independent human review. +Checks use explicit exceptions and unittest, and remain active under `-O`. + +Source baseline is canonical main +`20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision6. Frozen inputs +and the selected record remain unchanged. Exact source pins are in +[SOURCES.json](SOURCES.json); no unmerged Git object is required by replay. +Current task/overlap scope and remaining questions are in [TASK.json](TASK.json). +The registered workflow is the publication check; local results do not imply +hosted CI success until its exact published head passes. + +## Predecessor credit and what is new + +- [Rohan Arun's PR1972](https://github.com/CrocSwap/integer-mult-bounds/pull/1972) + owns the retained scalar/frame word. [PR1991](https://github.com/CrocSwap/integer-mult-bounds/pull/1991) + supplies its native realization and2312 persistent progress/2368 mass. +- [PR3882](https://github.com/CrocSwap/integer-mult-bounds/pull/3882), + [PR3894](https://github.com/CrocSwap/integer-mult-bounds/pull/3894) and + [PR3940](https://github.com/CrocSwap/integer-mult-bounds/pull/3940) supply + the correction and caller context; their208 correction units are granted. +- [PR3954](https://github.com/CrocSwap/integer-mult-bounds/pull/3954), head + `f1e2839819959cd0534d008be91ed5b79ec55a6a`, defines the proposed two-axis + scaffold, physical endpoint obligations and full-mask44096 rejection. + The new contribution is the all-mask closure/coverage theorem, the exact + asymmetric changed-profile criterion and the inventory-only reuse consequence. +- [PR3943](https://github.com/CrocSwap/integer-mult-bounds/pull/3943) and + [PR3956](https://github.com/CrocSwap/integer-mult-bounds/pull/3956) own the + residual consumer and matched return-adapter comparison; neither is redone. + [PR3045](https://github.com/CrocSwap/integer-mult-bounds/pull/3045) and the + concurrent private-COPY study concern literal copy lifetimes, a distinct scope. +- Douglas Colkitt and the credited authors of + `notes/copied-centers-complex.tex` supply the retained all-role caller and + paid physical endpoint semantics. + +Clear1nsight, with substantial OpenAI Codex multi-agent assistance. Apache-2.0. + +## Open next questions + +1. **A changed partial-port word or dangling completion.** Produce one actual + completed pair with all owner/encoded boundaries and invoice its work. + This could change the sparse gate; merely removing whole calls cannot. +2. **A changed translated progress law.** Exhibit one actual legally translated + call whose persistent progress exceeds2312, including preparation and + eventual helper return. This is blocked by a source-bound physical owner + schedule, not by the finite incidence search. +3. **A favorable changed profile.** Supply proved per-axis excesses and additional + boundary bill A satisfying the closed gate, then check the full positive- + exponent moment. A passing rank relaxation alone does not admit a supplier. + +Decision: NARROW. No further native expansion is justified by pruning or +inventory reduction under the unchanged conditional profile. diff --git a/research/p104-coverage-gate/RESULT.json b/research/p104-coverage-gate/RESULT.json new file mode 100644 index 0000000000..7f6d3b06ce --- /dev/null +++ b/research/p104-coverage-gate/RESULT.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "scope": "conditional whole-fiber incidence and progress gate", + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "witness": { + "ports": 104, + "helpers": 72, + "progress": 2312, + "native_mass": 2368, + "granted_correction": 208, + "corrected_mass": 2576 + }, + "mask_count": 11025, + "nonempty_masks": 11024, + "closed_masks": [ + [ + 0, + 0 + ], + [ + 104, + 104 + ] + ], + "all_masks_sha256": "56552e880f665d0af7f5ec986d06e852eabd53db9dae4243cf98d4c9d7ea334f", + "minimum_nonempty_excess": 160, + "full_inventory_controls": [ + { + "helpers": 72, + "width": 21704, + "remaining_rank": 1266312, + "lower_rank": 1802120, + "capacity": 1758024, + "excess": 44096 + }, + { + "helpers": 144, + "width": 21776, + "remaining_rank": 1272144, + "lower_rank": 1807952, + "capacity": 1763856, + "excess": 44096 + }, + { + "helpers": 14976, + "width": 36608, + "remaining_rank": 2473536, + "lower_rank": 3009344, + "capacity": 2965248, + "excess": 44096 + } + ], + "changed_profile_controls": [ + { + "row_excess": 264, + "column_excess": 264, + "minimum_two_axis_relaxation": 321, + "closed_excess": 44096 + }, + { + "row_excess": 100, + "column_excess": 100, + "minimum_two_axis_relaxation": -316, + "closed_excess": 9984 + }, + { + "row_excess": 56, + "column_excess": 56, + "minimum_two_axis_relaxation": -4936, + "closed_excess": 832 + }, + { + "row_excess": 51, + "column_excess": 52, + "minimum_two_axis_relaxation": -5460, + "closed_excess": -104 + }, + { + "row_excess": 103, + "column_excess": 104, + "minimum_two_axis_relaxation": 0, + "closed_excess": 10712 + }, + { + "row_excess": 104, + "column_excess": 103, + "minimum_two_axis_relaxation": 0, + "closed_excess": 10712 + }, + { + "row_excess": 0, + "column_excess": 300, + "minimum_two_axis_relaxation": -10516, + "closed_excess": 20384 + }, + { + "row_excess": 300, + "column_excess": 0, + "minimum_two_axis_relaxation": -10516, + "closed_excess": 20384 + } + ], + "sparse_discrimination_control": { + "a": 1, + "b": 1, + "excess_per_axis": 100, + "touched": 207, + "dangling": 206, + "relaxed_excess": -7, + "closed_excess": 9984 + }, + "selected_frontier_changed": false +} diff --git a/research/p104-coverage-gate/SOURCES.json b/research/p104-coverage-gate/SOURCES.json new file mode 100644 index 0000000000..2be8fdff1b --- /dev/null +++ b/research/p104-coverage-gate/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "notes/copied-centers-complex.tex", + "usage": "input", + "git_blob": "fddd7bc7f2a2f749ba6eada19d153bf9243ee31c", + "sha256": "18eac6d5c5755e53230c0c12a633f38b6ce9666ef0322c1aff79394f2952af72" + }, + { + "path": "research/p104-native-channel/PROOF.md", + "usage": "input", + "git_blob": "a69311b74f74a2f8e8f411c1451baacd9bacddce", + "sha256": "5d743145d389ffdfaffc66096fa7e32c7155b18f73d74755403151d0435bb94c" + }, + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e" + } + ] +} diff --git a/research/p104-coverage-gate/TASK.json b/research/p104-coverage-gate/TASK.json new file mode 100644 index 0000000000..173d902027 --- /dev/null +++ b/research/p104-coverage-gate/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "p104-side-correction", + "question": "Can the proposed P104 joint endpoint flags be realized by a chronological correction program with coefficients, dirty restoration and an affordable complete bill?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md", + "research/p104-joint-unit-flags/README.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2981 static joint flags, alongside the reviewed #1991 channel. #2981 is an author-checked source archive, not an independently validated executable correction or a refutation of program-level lifetime floors.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "After checking live handoffs, pin one named collection from #2981 and attach acquisition/delivery times, source dependencies and coefficient requirements. Test legal access and arbitrary dirty restoration; price any completion against the full channel/endpoint/hosting allowance. Stop with the exact missing implication or a scoped counterexample rather than expanding the static cover census.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.", + "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition", + "2981", + "joint unit flags", + "acquisition delivery", + "static nesting" + ], + "existing_checks": [ + { + "scope": "PR #2981 reports static joint endpoint flags and a matching of 208 departure and arrival flags; archival intake is not independent verification.", + "evidence": "research/p104-joint-unit-flags/README.md", + "remaining": "Independent flag check and a chronological coefficient program with dirty restoration and a complete cost.", + "status": "author-checked", + "source_commit": "3d24b92d8ba057b57cb2d480170ec407520e6882", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Source-bound whole-fiber incidence closure, all-mask conditional coverage gate, asymmetric changed-profile criterion and helper-inventory cancellation for the PR3954 proposed two-axis scaffold.", + "scope_change_reason": "Explicit user-directed multi-agent follow-up to PR3954: test changed coverage/owner inventory rather than construct another correction word.", + "bottleneck_link": "Determines whether pruning whole calls or helper inventory reuse can reopen the failed full two-axis gate before native construction.", + "budget_minutes": 50, + "stop_rule": "Stop native expansion if even the favorable all-mask gate fails; any favorable sparse relaxation must still complete every dangling endpoint.", + "outcome": "negative-result", + "evidence": "PROOF.md; source-bound verify.py and RESULT.json; separate independent.py; seven optimized-mode tests including six actual CLI receipt/source faults.", + "author": "Clear1nsight, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for derivation, implementation and multi-agent coordination; no independent human review claimed.", + "open_questions": [ + { + "question": "Can one changed partial-port word or a paid dangling completion satisfy the full caller endpoint?", + "why_it_matters": "Whole-call pruning leaves explicit unmatched shears; a new completion changes the additional bill.", + "first_step": "Pin one dangling pair and derive its encoded physical input/output and complete completion cost.", + "blocked_by": "No supplied physical completion or owner schedule." + }, + { + "question": "Can a legally translated call change the persistent progress cap?", + "why_it_matters": "Inventory-only sharing cancels from the present numerator; a changed progress law may alter it.", + "first_step": "Show one actual translated call with preparation, all-role endpoint and helper return.", + "blocked_by": "Unproved physical translation and complete boundary tariff." + } + ], + "checkpoint": { + "checked_utc": "2026-10-19T07:00:00Z", + "canonical_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "selected_frontier_changed": false, + "overlap": "Root coordination refreshed all662 open PR bodies including drafts over seven REST pages and bounded live Discussion1166/1163/2750/2619 checks; local find_overlap helper explicitly lacks a Discussion cache. No full-board exhaustiveness claimed.", + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/pull/3954#issuecomment-6261590999", + "parallel_scopes": "Adjacent encoded boundaries and private COPY lifetime audits are separate siblings; no savings from those unproved studies are assumed.", + "prepublication_check_utc": "2026-10-19T07:06:00Z", + "prepublication_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "prepublication_overlap": "Latest30 updated open PR bodies rechecked: PR3577 changed head but remains distinct collector-consumer scope; PR3954/3940/3943/3956 unchanged." + } +} diff --git a/research/p104-coverage-gate/VALIDATION.json b/research/p104-coverage-gate/VALIDATION.json new file mode 100644 index 0000000000..110e577f9c --- /dev/null +++ b/research/p104-coverage-gate/VALIDATION.json @@ -0,0 +1,26 @@ +{ + "environment": "3.12.3", + "status": "local-author-checked", + "commands": [ + { + "command": "python3 -B scripts/research_package.py --package research/p104-coverage-gate", + "outcome": "PASS_REGISTERED_RESEARCH_PACKAGE; all three registered commands passed" + }, + { + "command": "python3 -O -B research/p104-coverage-gate/verify.py", + "outcome": "PASS_P104_WHOLE_FIBER_COVERAGE_GATE" + }, + { + "command": "python3 -O -B research/p104-coverage-gate/independent.py", + "outcome": "PASS_INDEPENDENT_INCIDENCE:21844 explicit masks" + } + ], + "independent_review": "Coordinating Codex agent read proof and independently corroborated21844 incidence masks before receipt; not independent human review.", + "limits": [ + "No native execution of either global orientation", + "No actual shared-helper schedule or dangling physical completion", + "No all-size, signed-floor, precision or supplier admission", + "Hosted CI must be checked on the eventual published head" + ], + "result_sha256": "06fd419d46b6b439543cdc523ed2666f2188d0d648bd45866c8cd39b571dc5f9" +} diff --git a/research/p104-coverage-gate/VERIFY.json b/research/p104-coverage-gate/VERIFY.json new file mode 100644 index 0000000000..d13029a234 --- /dev/null +++ b/research/p104-coverage-gate/VERIFY.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "notes/copied-centers-complex.tex", + "research/p104-native-channel/PROOF.md", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source hash, exact native recount, all11025 count masks and asymmetric corner checks." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Independent explicit incidence sets for21844 masks, pair operators and rational corner optimization." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_verify.py", + "-v" + ], + "timeout_seconds": 120, + "checks": "Seven scientific/CLI control tests under optimized Python." + } + ] +} diff --git a/research/p104-coverage-gate/independent.py b/research/p104-coverage-gate/independent.py new file mode 100644 index 0000000000..b158212664 --- /dev/null +++ b/research/p104-coverage-gate/independent.py @@ -0,0 +1,58 @@ +#!/usr/bin/env python3 +"""Direct set/operator checker; imports no package/predecessor verifier.""" +import json +from fractions import Fraction +from pathlib import Path + +P = Path(__file__).resolve().parent + +def need(ok, message): + if not ok: + raise ValueError(message) + +def incidence(n, row_mask, col_mask): + rows = {i for i in range(n) if row_mask >> i & 1} + cols = {j for j in range(n) if col_mask >> j & 1} + touched = {(i,j) for i in rows for j in range(n)} | {(i,j) for j in cols for i in range(n)} + twice = {(i,j) for i,j in touched if i in rows and j in cols} + dangling = touched-twice + return len(rows),len(cols),len(touched),len(dangling) + +def main(): + checked = 0 + for n in range(1,8): + for rows in range(1< 0, 'unchanged profile rejection') + rows.append([a,b,touched,dangling,delta]) + require(closed == [[0,0],[n,n]], 'whole-call closure') + return rows, closed + + +def verify(): + source_bindings() + w = json.loads((ROOT / 'research/p104-native-channel/inputs/LOWRANK-WITNESS.json').read_text()) + progress, native_mass = recount(w) + rows, closed = census() + n, m, correction = 104, 81, 208 + corrected_mass = native_mass + correction + require(corrected_mass-progress == 264, 'conditional corrected excess') + # Explicit physical-owner inventories: retain a bank per call, share one bank, + # or share one bank per stage. No schedule legality is claimed by this control. + full = [] + for helper_count in (72,144,72*208): + width = 2*n*n + helper_count + remaining = m*width-n*n-208*progress + lower = 208*corrected_mass+max(0,remaining) + require(lower-m*width == 44096, 'helper inventory cancellation') + full.append({'helpers':helper_count,'width':width,'remaining_rank':remaining, + 'lower_rank':lower,'capacity':m*width,'excess':lower-m*width}) + # Both-axis four-corner optimization against all integer masks, several + # asymmetric profiles, and the intentionally misleading sparse pass. + optimization = [] + for er,ec in ((264,264),(100,100),(56,56),(51,52),(103,104),(104,103),(0,300),(300,0)): + values = [(er-104)*a+(ec-104)*b+a*b for a in range(1,105) for b in range(1,105)] + corners = [(er-104)*a+(ec-104)*b+a*b for a,b in ((1,1),(1,104),(104,1),(104,104))] + require(min(values)==min(corners), 'bilinear corner criterion') + optimization.append({'row_excess':er,'column_excess':ec,'minimum_two_axis_relaxation':min(values), + 'closed_excess':104*(er+ec-104)}) + sparse = {'a':1,'b':1,'excess_per_axis':100,'touched':207,'dangling':206, + 'relaxed_excess':-7,'closed_excess':9984} + require(200-207==-7 and 104*200-104**2==9984, 'sparse false-admission control') + payload = json.dumps(rows,separators=(',',':')).encode() + return {'schema_version':1,'scope':'conditional whole-fiber incidence and progress gate', + 'base_commit':'20ecf2891d80b5acf18d980b2164fb44ea7faa90', + 'witness':{'ports':104,'helpers':72,'progress':progress,'native_mass':native_mass, + 'granted_correction':208,'corrected_mass':corrected_mass}, + 'mask_count':len(rows),'nonempty_masks':len(rows)-1,'closed_masks':closed, + 'all_masks_sha256':hashlib.sha256(payload).hexdigest(), + 'minimum_nonempty_excess':min(r[4] for r in rows if r[0]+r[1]), + 'full_inventory_controls':full,'changed_profile_controls':optimization, + 'sparse_discrimination_control':sparse,'selected_frontier_changed':False} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--write-result',action='store_true') + args = parser.parse_args() + result = verify() + if args.write_result: + (PACKAGE/'RESULT.json').write_text(json.dumps(result,indent=2)+'\n') + else: + expected = strict_load(PACKAGE/'RESULT.json') + require(json.dumps(result, sort_keys=True, separators=(',', ':')) == + json.dumps(expected, sort_keys=True, separators=(',', ':')), + 'typed committed result equality') + print('PASS_P104_WHOLE_FIBER_COVERAGE_GATE: 11025 masks; conditional scope only') + +if __name__ == '__main__': + main() From f7572974ac7fbcd21fd71c73b64bca0c8487aed6 Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 18:10:12 +1100 Subject: [PATCH 2/2] test: permit mutations only in disposable read-only export fixtures --- research/p104-coverage-gate/test_verify.py | 1 + 1 file changed, 1 insertion(+) diff --git a/research/p104-coverage-gate/test_verify.py b/research/p104-coverage-gate/test_verify.py index d11d7670bc..dff97c32d3 100644 --- a/research/p104-coverage-gate/test_verify.py +++ b/research/p104-coverage-gate/test_verify.py @@ -25,6 +25,7 @@ def cli_fault(self, kind): target=root/row['path'];target.parent.mkdir(parents=True,exist_ok=True) shutil.copyfile(verify.ROOT/row['path'],target) result=package/'RESULT.json' + result.chmod(0o600) # Only the disposable fixture copy is mutated. data=json.loads(result.read_text()) if kind=='boolean': data['schema_version']=True