diff --git a/packs/number-theory/problems/848/BOUNDED_VERIFICATION_PLAN.md b/packs/number-theory/problems/848/BOUNDED_VERIFICATION_PLAN.md index 9e0437f..cb22032 100644 --- a/packs/number-theory/problems/848/BOUNDED_VERIFICATION_PLAN.md +++ b/packs/number-theory/problems/848/BOUNDED_VERIFICATION_PLAN.md @@ -41,6 +41,8 @@ Current progress: - the repo now has an exact small-`N` certificate for `1..10000` - an incremental verifier replaced the misleading earlier cost wall and made larger exact tranches practical again +- local ignored rollout artifacts extend exact small-`N` evidence to `1..40500`, but the + 440 MB raw packet is not committed or bundled; see `EXACT_INTERVAL_BOOKKEEPING.md` What this lane is not: - not brute force to `2.64 x 10^17` diff --git a/packs/number-theory/problems/848/CLAIM_LOOP.json b/packs/number-theory/problems/848/CLAIM_LOOP.json index 7ae2b01..a5be98f 100644 --- a/packs/number-theory/problems/848/CLAIM_LOOP.json +++ b/packs/number-theory/problems/848/CLAIM_LOOP.json @@ -11,9 +11,15 @@ "currentState": { "theoremLoopMode": "bridge_backed", "activeRoute": "finite_check_gap_closure", - "nextHonestMove": "Decide whether to extend exact verified coverage beyond `40500` or switch method class.", + "nextHonestMove": "Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed.", "routeSummary": "Convert the sufficiently-large-N theorem into a complete all-N resolution without overstating what is already closed or confusing imported thresholds with repo-owned claims.", - "sourceRefresh": "erdos number-theory bridge-refresh 848" + "sourceRefresh": "erdos number-theory bridge-refresh 848", + "exactIntervalBookkeeping": { + "publicRepoRawExactInterval": "1..10000", + "localIgnoredRolloutInterval": "1..40500", + "bookkeepingArtifact": "EXACT_INTERVAL_BOOKKEEPING.md", + "raw40500PacketCommitted": false + } }, "featureExtractors": [ { @@ -141,7 +147,7 @@ "status": "ready", "source": "theorem_agenda", "summary": "Choose the next finite-gap closure move and keep the theorem-facing claim surface honest.", - "why": "Decide whether to extend exact verified coverage beyond `40500` or switch method class.", + "why": "Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed.", "support": [ "next_unmatched_equals_282_failure", "completed_tail_vs_search_leader_split", @@ -249,7 +255,7 @@ "item_id": "choose_next_finite_gap_move", "status": "ready", "task": "Choose the next finite-gap closure move and keep the theorem-facing claim surface honest.", - "why": "Decide whether to extend exact verified coverage beyond `40500` or switch method class." + "why": "Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed." }, { "item_id": "explain_next_unmatched_alignment", diff --git a/packs/number-theory/problems/848/CLAIM_LOOP.md b/packs/number-theory/problems/848/CLAIM_LOOP.md index 8f876af..195b60a 100644 --- a/packs/number-theory/problems/848/CLAIM_LOOP.md +++ b/packs/number-theory/problems/848/CLAIM_LOOP.md @@ -8,7 +8,7 @@ This claim loop generalizes theorem-search-verification work using the theorem l - Current claim surface: `bridge_backed_frontier_support`. - Active route: `finite_check_gap_closure`. - Route summary: Convert the sufficiently-large-N theorem into a complete all-N resolution without overstating what is already closed or confusing imported thresholds with repo-owned claims. -- Next honest move: Decide whether to extend exact verified coverage beyond `40500` or switch method class. +- Next honest move: Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed. ## Feature Extractors @@ -40,7 +40,7 @@ This claim loop generalizes theorem-search-verification work using the theorem l ## Candidate Claims -- `choose_next_finite_gap_move`: ready | Choose the next finite-gap closure move and keep the theorem-facing claim surface honest. | Decide whether to extend exact verified coverage beyond `40500` or switch method class. +- `choose_next_finite_gap_move`: ready | Choose the next finite-gap closure move and keep the theorem-facing claim surface honest. | Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed. - `explain_next_unmatched_alignment`: ready | Explain structurally why shared-prefix representative `137720141` aligns with the first failure of tail `282`. | If that alignment is structural rather than accidental, it turns a search coincidence into a theorem-facing obstruction class. - `explain_completed_vs_search_leader_split`: ready | Explain why completed structured tail `332` differs from current family-aware leader `432`. | That split tells us whether the live frontier is a finite-window artifact or a genuinely better structural continuation class. - `model_repair_pool_growth`: ready | Model the repaired square-modulus pool as a growing family rather than treating it as already closed. | Recent packets introduced new square moduli, so the theorem lane should aim for controlled growth, not premature closure. diff --git a/packs/number-theory/problems/848/CLAIM_PASS.json b/packs/number-theory/problems/848/CLAIM_PASS.json index 20e7593..750be37 100644 --- a/packs/number-theory/problems/848/CLAIM_PASS.json +++ b/packs/number-theory/problems/848/CLAIM_PASS.json @@ -10,10 +10,16 @@ "currentClaimSurface": "bridge_backed_frontier_support", "currentState": { "activeRoute": "finite_check_gap_closure", - "nextHonestMove": "Decide whether to extend exact verified coverage beyond `40500` or switch method class.", + "nextHonestMove": "Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed.", "routeSummary": "Convert the sufficiently-large-N theorem into a complete all-N resolution without overstating what is already closed or confusing imported thresholds with repo-owned claims.", - "latestVerifiedInterval": "1..40500", - "sourceRefresh": "erdos number-theory bridge-refresh 848" + "latestVerifiedInterval": "1..10000", + "sourceRefresh": "erdos number-theory bridge-refresh 848", + "exactIntervalBookkeeping": { + "publicRepoRawExactInterval": "1..10000", + "localIgnoredRolloutInterval": "1..40500", + "bookkeepingArtifact": "EXACT_INTERVAL_BOOKKEEPING.md", + "raw40500PacketCommitted": false + } }, "summary": { "hooks": { @@ -78,7 +84,7 @@ "theoremReady": false, "supportSatisfied": true, "summary": "Choose the next finite-gap closure move and keep the theorem-facing claim surface honest.", - "rationale": "The current canonical exact base is 1..40500; the next interval is still open.", + "rationale": "The local exact rollout reaches 1..40500, but the public raw packet remains 1..10000 until compact promotion is committed.", "nextAction": "decide_post_40500_verification_lane" }, { @@ -167,7 +173,7 @@ "recommendation_id": "decide_post_40500_verification_lane", "priority": "high", "lane": "exact_verifier", - "reason": "The canonical exact base currently ends at 1..40500. The next verification move is still open.", + "reason": "Resolve the local 1..40500 promotion boundary; public raw packet currently ends at 1..10000.", "command": "erdos number-theory dispatch 848" }, { diff --git a/packs/number-theory/problems/848/CLAIM_PASS.md b/packs/number-theory/problems/848/CLAIM_PASS.md index ba1d035..0624e59 100644 --- a/packs/number-theory/problems/848/CLAIM_PASS.md +++ b/packs/number-theory/problems/848/CLAIM_PASS.md @@ -8,8 +8,8 @@ This claim pass evaluates theorem-search claims against the canonical claim loop - Current claim surface: `bridge_backed_frontier_support`. - Active route: `finite_check_gap_closure`. - Route summary: Convert the sufficiently-large-N theorem into a complete all-N resolution without overstating what is already closed or confusing imported thresholds with repo-owned claims. -- Next honest move: Decide whether to extend exact verified coverage beyond `40500` or switch method class. -- Latest verified interval: `1..40500` +- Next honest move: Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed. +- Latest exact interval: public raw `1..10000`; local rollout `1..40500` ## Summary @@ -25,7 +25,7 @@ This claim pass evaluates theorem-search claims against the canonical claim loop ## Claim Assessments -- `choose_next_finite_gap_move`: actionable | Choose the next finite-gap closure move and keep the theorem-facing claim surface honest. | The current canonical exact base is 1..40500; the next interval is still open. +- `choose_next_finite_gap_move`: actionable | Choose the next finite-gap closure move and keep the theorem-facing claim surface honest. | The local exact rollout reaches 1..40500, but the public raw packet remains 1..10000 until compact promotion is committed. - `explain_next_unmatched_alignment`: actionable | Explain structurally why shared-prefix representative `137720141` aligns with the first failure of tail `282`. | If that alignment is structural rather than accidental, it turns a search coincidence into a theorem-facing obstruction class. - `explain_completed_vs_search_leader_split`: actionable | Explain why completed structured tail `332` differs from current family-aware leader `432`. | That split tells us whether the live frontier is a finite-window artifact or a genuinely better structural continuation class. - `model_repair_pool_growth`: actionable | Model the repaired square-modulus pool as a growing family rather than treating it as already closed. | Recent packets introduced new square moduli, so the theorem lane should aim for controlled growth, not premature closure. @@ -37,7 +37,7 @@ This claim pass evaluates theorem-search claims against the canonical claim loop - `formalize_282_alignment`: high | theorem_formalization | The bridge matches shared-prefix representative 137720141 with tracked tail 282 first failure 137720141. | erdos problem formalization 848 - `formalize_top_repair_cluster`: high | theorem_formalization | Top cluster 432, 782, 832 shares repaired-known=26, repaired-predicted=242, clean-through=250075000. | erdos problem formalization 848 -- `decide_post_40500_verification_lane`: high | exact_verifier | The canonical exact base currently ends at 1..40500. The next verification move is still open. | erdos number-theory dispatch 848 +- `decide_post_40500_verification_lane`: high | exact_verifier | Resolve the local 1..40500 promotion boundary; public raw packet currently ends at 1..10000. | erdos number-theory dispatch 848 - `model_repair_pool_growth`: medium | theorem_formalization | Recent bridge packets introduced new square moduli: 1369, 841, 17161, 1849. | erdos problem formalization 848 ## Commands diff --git a/packs/number-theory/problems/848/EXACT_BREAKPOINT_CERTIFICATE.json b/packs/number-theory/problems/848/EXACT_BREAKPOINT_CERTIFICATE.json index ab71398..b6cfe65 100644 --- a/packs/number-theory/problems/848/EXACT_BREAKPOINT_CERTIFICATE.json +++ b/packs/number-theory/problems/848/EXACT_BREAKPOINT_CERTIFICATE.json @@ -2,7 +2,7 @@ "generatedAt": "2026-04-11T02:57:10.497Z", "method": "candidate_plateau_endpoint_monotonicity", "problemId": "848", - "sourceResultsPath": "/Volumes/Code_2TB/code/erdos-problems/packs/number-theory/problems/848/EXACT_SMALL_N_1_40500_RESULTS.json", + "sourceResultsPath": "output/p848-exact-small-n-rollouts/EXACT_SMALL_N_1_40500_RESULTS.json", "status": "certified_from_endpoint_monotonicity", "summary": { "interval": "1..40500", @@ -19482,5 +19482,10 @@ } ], "failedEndpointChecks": [], - "rowFailures": [] + "rowFailures": [], + "sourceResultsStatus": "local_ignored_large_raw_packet", + "sourceResultsSha256": "da3546ab3f30faef879c2d4da680f826711361e2c685de8f384eb116df1f8fbc", + "publicRepoRawExactPacket": "EXACT_SMALL_N_1_10000_RESULTS.json", + "publicRepoRawExactInterval": "1..10000", + "bookkeepingArtifact": "EXACT_INTERVAL_BOOKKEEPING.md" } diff --git a/packs/number-theory/problems/848/EXACT_BREAKPOINT_SCOUT.json b/packs/number-theory/problems/848/EXACT_BREAKPOINT_SCOUT.json index 12920b5..60f2a19 100644 --- a/packs/number-theory/problems/848/EXACT_BREAKPOINT_SCOUT.json +++ b/packs/number-theory/problems/848/EXACT_BREAKPOINT_SCOUT.json @@ -2,7 +2,7 @@ "generatedAt": "2026-04-11T02:57:09.787Z", "method": "exact_rows_breakpoint_scout", "problemId": "848", - "sourceResultsPath": "/Volumes/Code_2TB/code/erdos-problems/packs/number-theory/problems/848/EXACT_SMALL_N_1_40500_RESULTS.json", + "sourceResultsPath": "output/p848-exact-small-n-rollouts/EXACT_SMALL_N_1_40500_RESULTS.json", "sourceSummary": { "interval": "1..40500", "rows": 40500, @@ -35706,5 +35706,10 @@ "claimLevel": "scout_not_proof", "note": "This artifact summarizes already-certified exact rows. It does not prove coverage between unchecked rows or replace a Regime B monotonicity/breakpoint lemma.", "nextUse": "Use the plateau and breakpoint pattern to propose a structured-breakpoint certificate with an explicit monotonicity justification." - } + }, + "sourceResultsStatus": "local_ignored_large_raw_packet", + "sourceResultsSha256": "da3546ab3f30faef879c2d4da680f826711361e2c685de8f384eb116df1f8fbc", + "publicRepoRawExactPacket": "EXACT_SMALL_N_1_10000_RESULTS.json", + "publicRepoRawExactInterval": "1..10000", + "bookkeepingArtifact": "EXACT_INTERVAL_BOOKKEEPING.md" } diff --git a/packs/number-theory/problems/848/EXACT_INTERVAL_BOOKKEEPING.json b/packs/number-theory/problems/848/EXACT_INTERVAL_BOOKKEEPING.json new file mode 100644 index 0000000..417a0aa --- /dev/null +++ b/packs/number-theory/problems/848/EXACT_INTERVAL_BOOKKEEPING.json @@ -0,0 +1,25 @@ +{ + "schema": "erdos.problem848_exact_interval_bookkeeping/1", + "problemId": "848", + "statusDate": "2026-04-15", + "publicRepoRawExactPacket": { + "interval": "1..10000", + "certificate": "EXACT_SMALL_N_1_10000_CERTIFICATE.md", + "rawResultPacket": "EXACT_SMALL_N_1_10000_RESULTS.json", + "rawResultSha256": "96748efe7a355621016f4987209e1b634b1d14ac3f79f135dcc3a0a55a3dfcb2" + }, + "localIgnoredRollout": { + "interval": "1..40500", + "certificate": "output/p848-exact-small-n-rollouts/EXACT_SMALL_N_1_40500_CERTIFICATE.md", + "rawResultPacket": "output/p848-exact-small-n-rollouts/EXACT_SMALL_N_1_40500_RESULTS.json", + "rawResultSha256": "da3546ab3f30faef879c2d4da680f826711361e2c685de8f384eb116df1f8fbc", + "rawResultApproximateSize": "440 MB" + }, + "committedCompactDerivatives": [ + "EXACT_BREAKPOINT_SCOUT.json", + "EXACT_BREAKPOINT_CERTIFICATE.json" + ], + "claimRule": "Use 1..10000 for the public repo raw exact packet. Use 1..40500 only when explicitly described as local ignored rollout evidence or compact breakpoint/endpoint evidence derived from that rollout.", + "npmRule": "The npm package intentionally excludes raw exact small-N result JSON.", + "nextResearchUse": "Use the 1..40500 rollout as regression and structure-mining evidence while prioritizing theorem compression over raw interval extension." +} diff --git a/packs/number-theory/problems/848/EXACT_INTERVAL_BOOKKEEPING.md b/packs/number-theory/problems/848/EXACT_INTERVAL_BOOKKEEPING.md new file mode 100644 index 0000000..606fa6a --- /dev/null +++ b/packs/number-theory/problems/848/EXACT_INTERVAL_BOOKKEEPING.md @@ -0,0 +1,52 @@ +# Problem 848 Exact Interval Bookkeeping + +This note fixes the claim boundary between public repo artifacts, local rollout +artifacts, and npm package contents. + +## Current distinction + +- Public repo raw exact packet: `1..10000` + - Certificate: `EXACT_SMALL_N_1_10000_CERTIFICATE.md` + - Raw result packet: `EXACT_SMALL_N_1_10000_RESULTS.json` + - Result SHA-256: + `96748efe7a355621016f4987209e1b634b1d14ac3f79f135dcc3a0a55a3dfcb2` +- Local ignored rollout: `1..40500` + - Certificate: `output/p848-exact-small-n-rollouts/EXACT_SMALL_N_1_40500_CERTIFICATE.md` + - Raw result packet: `output/p848-exact-small-n-rollouts/EXACT_SMALL_N_1_40500_RESULTS.json` + - Result SHA-256: + `da3546ab3f30faef879c2d4da680f826711361e2c685de8f384eb116df1f8fbc` + - Raw result size: about `440 MB` +- Committed compact derivatives from the local rollout: + - `EXACT_BREAKPOINT_SCOUT.json` + - `EXACT_BREAKPOINT_CERTIFICATE.json` + +## Claim rule + +Use `1..10000` when referring to the public repo's committed raw exact packet. +Use `1..40500` only when it is explicitly described as a local ignored rollout +or as compact breakpoint/endpoint evidence derived from that local rollout. + +Do not say that npm bundles either raw exact interval packet. The npm package +intentionally excludes raw exact small-`N` result JSON. + +## Promotion rule + +To promote `1..40500` from local rollout evidence into a public compact interval +claim, commit a compact certificate surface that includes: + +- the interval and method class +- the raw local result hash +- the reproduction command family +- the compact endpoint certificate used for review +- an explicit note that the 440 MB raw packet is not committed or bundled + +Until that promotion is complete, user-facing status should say: + +`public raw exact packet: 1..10000; local compact rollout evidence: 1..40500`. + +## Next research use + +The `1..40500` rollout is useful as regression and structure-mining evidence. +It should not distract from the current theorem lane: prove the four-anchor +obstruction or the split-core symbolic matching lift that can replace raw +interval extension. diff --git a/packs/number-theory/problems/848/FORMALIZATION.json b/packs/number-theory/problems/848/FORMALIZATION.json index a5fc2f6..46f28b9 100644 --- a/packs/number-theory/problems/848/FORMALIZATION.json +++ b/packs/number-theory/problems/848/FORMALIZATION.json @@ -11,9 +11,15 @@ "currentState": { "activeRoute": "finite_check_gap_closure", "routeSummary": "Convert the sufficiently-large-N theorem into a complete all-N resolution without overstating what is already closed or confusing imported thresholds with repo-owned claims.", - "nextHonestMove": "Decide whether to extend exact verified coverage beyond `40500` or switch method class.", - "latestVerifiedInterval": "1..40500", - "sourceRefresh": "erdos number-theory bridge-refresh 848" + "nextHonestMove": "Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed.", + "latestVerifiedInterval": "1..10000", + "sourceRefresh": "erdos number-theory bridge-refresh 848", + "exactIntervalBookkeeping": { + "publicRepoRawExactInterval": "1..10000", + "localIgnoredRolloutInterval": "1..40500", + "bookkeepingArtifact": "EXACT_INTERVAL_BOOKKEEPING.md", + "raw40500PacketCommitted": false + } }, "currentTarget": { "formalizationId": "p848_282_alignment_formalization_v1", @@ -34,7 +40,7 @@ "The current family menu already contains representative 137720141 with tuple key 4, 23^2, 7^2, 9, 17^2, 11^2 and tuple rows 7->4/1, 32->529/281, 57->49/6, 82->9/8, 132->289/81, 182->121/119.", "On that family-menu row, only continuation 282 fails among the tracked tails, and it does so via witness modulus 841.", "The strongest completed structured tail remains 332, so this packet isolates the 282 obstruction mechanism rather than conflating it with the current family-aware leader 432.", - "The finite exact base is already certified through 1..40500, so the open work is structural rather than basic interval bookkeeping.", + "The public raw exact packet is committed through 1..10000, while local compact rollout evidence reaches 1..40500; the open work is still structural rather than raw interval bookkeeping.", "Formalization-work checker p848_132_activation_row_certificate_checker_v1 replayed 17 activation rows with 0 failures.", "Formalization-work checker p848_132_lift_crt_checker_v1 proved the 132-row lift with k=147 and residue 504 mod 841.", "The top repair-class side packet is also checked: +2 finite-menu replay plus 74 mod-50 lane exchange rows pass." @@ -183,7 +189,7 @@ "theoremReady": false, "supportSatisfied": true, "summary": "Choose the next finite-gap closure move and keep the theorem-facing claim surface honest.", - "rationale": "The current canonical exact base is 1..40500; the next interval is still open.", + "rationale": "The local exact rollout reaches 1..40500, but the public raw packet remains 1..10000 until compact promotion is committed.", "nextAction": "decide_post_40500_verification_lane" }, { @@ -272,7 +278,7 @@ "recommendation_id": "decide_post_40500_verification_lane", "priority": "high", "lane": "exact_verifier", - "reason": "The canonical exact base currently ends at 1..40500. The next verification move is still open.", + "reason": "Resolve the local 1..40500 promotion boundary; public raw packet currently ends at 1..10000.", "command": "erdos number-theory dispatch 848" }, { diff --git a/packs/number-theory/problems/848/FORMALIZATION.md b/packs/number-theory/problems/848/FORMALIZATION.md index dd4129c..3707036 100644 --- a/packs/number-theory/problems/848/FORMALIZATION.md +++ b/packs/number-theory/problems/848/FORMALIZATION.md @@ -8,8 +8,8 @@ This formalization packet promotes the current claim-pass recommendation into a - Current claim surface: `bridge_backed_frontier_support`. - Active route: `finite_check_gap_closure`. - Route summary: Convert the sufficiently-large-N theorem into a complete all-N resolution without overstating what is already closed or confusing imported thresholds with repo-owned claims. -- Next honest move: Decide whether to extend exact verified coverage beyond `40500` or switch method class. -- Latest verified interval: `1..40500` +- Next honest move: Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed. +- Latest exact interval: public raw `1..10000`; local rollout `1..40500` ## Current Target @@ -39,7 +39,7 @@ The canonical bridge freezes next unmatched representative 137720141, and the cl - The current family menu already contains representative 137720141 with tuple key 4, 23^2, 7^2, 9, 17^2, 11^2 and tuple rows 7->4/1, 32->529/281, 57->49/6, 82->9/8, 132->289/81, 182->121/119. - On that family-menu row, only continuation 282 fails among the tracked tails, and it does so via witness modulus 841. - The strongest completed structured tail remains 332, so this packet isolates the 282 obstruction mechanism rather than conflating it with the current family-aware leader 432. -- The finite exact base is already certified through 1..40500, so the open work is structural rather than basic interval bookkeeping. +- The public raw exact packet is committed through 1..10000, while local compact rollout evidence reaches 1..40500; the open work is still structural rather than raw interval bookkeeping. - Formalization-work checker p848_132_activation_row_certificate_checker_v1 replayed 17 activation rows with 0 failures. - Formalization-work checker p848_132_lift_crt_checker_v1 proved the 132-row lift with k=147 and residue 504 mod 841. - The top repair-class side packet is also checked: +2 finite-menu replay plus 74 mod-50 lane exchange rows pass. diff --git a/packs/number-theory/problems/848/FORMALIZATION_WORK.json b/packs/number-theory/problems/848/FORMALIZATION_WORK.json index b5dcec1..e1debfa 100644 --- a/packs/number-theory/problems/848/FORMALIZATION_WORK.json +++ b/packs/number-theory/problems/848/FORMALIZATION_WORK.json @@ -11,8 +11,14 @@ "currentState": { "activeRoute": "finite_check_gap_closure", "routeSummary": "Convert the sufficiently-large-N theorem into a complete all-N resolution without overstating what is already closed or confusing imported thresholds with repo-owned claims.", - "nextHonestMove": "Decide whether to extend exact verified coverage beyond `40500` or switch method class.", - "latestVerifiedInterval": "1..40500" + "nextHonestMove": "Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed.", + "latestVerifiedInterval": "1..10000", + "exactIntervalBookkeeping": { + "publicRepoRawExactInterval": "1..10000", + "localIgnoredRolloutInterval": "1..40500", + "bookkeepingArtifact": "EXACT_INTERVAL_BOOKKEEPING.md", + "raw40500PacketCommitted": false + } }, "currentWork": { "workId": "p848_282_first_failure_mechanism_packet_v1", @@ -113,7 +119,7 @@ "remainingGaps": [ "Prove structural-lift atom D2_p13_matching_lower_bound: For p=13 threatening rows, maxMatching(H_{x,N}) is at least the required matching bound extracted from the margin inequality.", "Advance the same atomic packet toward target D4_matching_bound_implies_sMaxMixed_bound: If maxMatching(H_{x,N}) >= K(N), then sMixed(x,N) <= |L| + |R| - K(N).", - "Decide and run the next post-40500 verification lane using local CPU and opt-in local 4090 compute only." + "Resolve the local 1..40500 promotion boundary, then use further exact runs only as local/free regression evidence." ], "proofObligations": [ { diff --git a/packs/number-theory/problems/848/FORMALIZATION_WORK.md b/packs/number-theory/problems/848/FORMALIZATION_WORK.md index 6c2417d..be01e98 100644 --- a/packs/number-theory/problems/848/FORMALIZATION_WORK.md +++ b/packs/number-theory/problems/848/FORMALIZATION_WORK.md @@ -8,8 +8,8 @@ This packet turns the current formalization target into one concrete work unit t - Current claim surface: `bridge_backed_frontier_support`. - Active route: `finite_check_gap_closure`. - Route summary: Convert the sufficiently-large-N theorem into a complete all-N resolution without overstating what is already closed or confusing imported thresholds with repo-owned claims. -- Next honest move: Decide whether to extend exact verified coverage beyond `40500` or switch method class. -- Latest verified interval: `1..40500` +- Next honest move: Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed. +- Latest exact interval: public raw `1..10000`; local rollout `1..40500` ## Current Work @@ -116,7 +116,7 @@ This packet turns the current formalization target into one concrete work unit t - Prove structural-lift atom D2_p13_matching_lower_bound: For p=13 threatening rows, maxMatching(H_{x,N}) is at least the required matching bound extracted from the margin inequality. - Advance the same atomic packet toward target D4_matching_bound_implies_sMaxMixed_bound: If maxMatching(H_{x,N}) >= K(N), then sMixed(x,N) <= |L| + |R| - K(N). -- Decide and run the next post-40500 verification lane using local CPU and opt-in local 4090 compute only. +- Resolve the local 1..40500 promotion boundary, then use further exact runs only as local/free regression evidence. ## Atomic Proof Obligations diff --git a/packs/number-theory/problems/848/FORMALIZATION_WORK.svg b/packs/number-theory/problems/848/FORMALIZATION_WORK.svg index c8beb8f..9fd9af1 100644 --- a/packs/number-theory/problems/848/FORMALIZATION_WORK.svg +++ b/packs/number-theory/problems/848/FORMALIZATION_WORK.svg @@ -1 +1 @@ -Erdos Problem #848 formalization work diagramDiagram of the 848 shared-prefix row progression showing when tracked anchors hit witness 841 and why anchor 282 is special at row index 0.Erdos Problem #848: 282 / 841 MechanismRepresentative 137720141 on tuple 4, 23^2, 7^2, 9, 17^2, 11^2Witness 841 is the extra repair witness; the row progression itself still traverses all residues modulo 841.Tuple-row CRT projects to 504 mod 841, stabilizing when anchor 132 is added.Verdictcontrolled_congruence_candidateRepresentative residue504 mod 841282 row startt = 0Next same-row 282 hit27443256270065Verified base1..40500Shared-Prefix Row ProgressionEach point shows the first row index t where a tracked anchor can hit witness 841 along n = residue + modulus * t.never0210420630841157t=610232no solution282t=0332t=67382t=592432t=318782t=164832t=379Residue Match SliceRepresentative residue 504 matches only the 282 failure residue class.157needs 766later/other residueres=75232needs noneunsolvableres=30282needs 504matches repres=0332needs 803later/other residueres=811382needs 284later/other residueres=781432needs 329later/other residueres=751782needs 784later/other residueres=541832needs 187later/other residueres=511Earlier Boundary RowsEarlier rows stay nonzero mod 841 before the first 282 failure lands.127484267res=7369, 17^2, 4, 29^2, 7^2, 11^2127682743res=736131^2, 11^2, 4, 29^2, 13^2, 9136702637res=4574, 43^2, 11^2, 9, 7^2, 19^2Tuple-Row CRT ProjectionAs tuple congruences are added, the projected residue modulo 841 evolves toward the boundary value 504.a=7mod 4res 1a=32mod 2116res 281a=57mod 103684res 36a=82mod 933156res 400a=132mod 269682084res 504a=182mod 32631532164res 504North-star reading: the row does not force 841 by itself, but the boundary representative is the unique tracked start-point of the 282 witness class inside that row progression. \ No newline at end of file +Erdos Problem #848 formalization work diagramDiagram of the 848 shared-prefix row progression showing when tracked anchors hit witness 841 and why anchor 282 is special at row index 0.Erdos Problem #848: 282 / 841 MechanismRepresentative 137720141 on tuple 4, 23^2, 7^2, 9, 17^2, 11^2Witness 841 is the extra repair witness; the row progression itself still traverses all residues modulo 841.Tuple-row CRT projects to 504 mod 841, stabilizing when anchor 132 is added.Verdictcontrolled_congruence_candidateRepresentative residue504 mod 841282 row startt = 0Next same-row 282 hit27443256270065Verified base1..10000 raw / 40500 localShared-Prefix Row ProgressionEach point shows the first row index t where a tracked anchor can hit witness 841 along n = residue + modulus * t.never0210420630841157t=610232no solution282t=0332t=67382t=592432t=318782t=164832t=379Residue Match SliceRepresentative residue 504 matches only the 282 failure residue class.157needs 766later/other residueres=75232needs noneunsolvableres=30282needs 504matches repres=0332needs 803later/other residueres=811382needs 284later/other residueres=781432needs 329later/other residueres=751782needs 784later/other residueres=541832needs 187later/other residueres=511Earlier Boundary RowsEarlier rows stay nonzero mod 841 before the first 282 failure lands.127484267res=7369, 17^2, 4, 29^2, 7^2, 11^2127682743res=736131^2, 11^2, 4, 29^2, 13^2, 9136702637res=4574, 43^2, 11^2, 9, 7^2, 19^2Tuple-Row CRT ProjectionAs tuple congruences are added, the projected residue modulo 841 evolves toward the boundary value 504.a=7mod 4res 1a=32mod 2116res 281a=57mod 103684res 36a=82mod 933156res 400a=132mod 269682084res 504a=182mod 32631532164res 504North-star reading: the row does not force 841 by itself, but the boundary representative is the unique tracked start-point of the 282 witness class inside that row progression. \ No newline at end of file diff --git a/packs/number-theory/problems/848/FRONTIER_NOTE.md b/packs/number-theory/problems/848/FRONTIER_NOTE.md index d80d098..4fb4ec8 100644 --- a/packs/number-theory/problems/848/FRONTIER_NOTE.md +++ b/packs/number-theory/problems/848/FRONTIER_NOTE.md @@ -35,7 +35,8 @@ Chosen next lane: - prove the four-anchor obstruction and turn it into a breakpoint theorem candidate Why this lane wins the next cycle: -- the exact verifier now reaches `1..10000`, so the finite-check surface is no longer tiny +- the committed raw exact packet reaches `1..10000`, and local ignored rollout evidence reaches + `1..40500`; this distinction is now frozen in `EXACT_INTERVAL_BOOKKEEPING.md` - the exact packet already exhibits a rigid breakpoint law: clique size only jumps at `N equiv 7 (mod 25)` - the new anchor recon suggests a fixed finite obstruction set `{7, 32, 57, 82}` beyond the diff --git a/packs/number-theory/problems/848/INTERVAL_WORK_QUEUE.yaml b/packs/number-theory/problems/848/INTERVAL_WORK_QUEUE.yaml index bc256c4..4cbe555 100644 --- a/packs/number-theory/problems/848/INTERVAL_WORK_QUEUE.yaml +++ b/packs/number-theory/problems/848/INTERVAL_WORK_QUEUE.yaml @@ -15,14 +15,27 @@ intervals: data_packet: EXACT_SMALL_N_1_10000_RESULTS.json next_move: Use this as the current trusted base interval and decide whether the next extension is another exact interval or an imported-computation audit. - interval_id: N848.V2 - label: exact_small_n_extension - range: "10001..?" - status: ready + label: exact_small_n_local_rollout + range: "10001..40500" + status: local_unpromoted + method_class: exact_small_n + claim_level: local_compact_evidence + certificate: output/p848-exact-small-n-rollouts/EXACT_SMALL_N_1_40500_CERTIFICATE.md + data_packet: output/p848-exact-small-n-rollouts/EXACT_SMALL_N_1_40500_RESULTS.json + compact_derivatives: + - EXACT_BREAKPOINT_SCOUT.json + - EXACT_BREAKPOINT_CERTIFICATE.json + bookkeeping: EXACT_INTERVAL_BOOKKEEPING.md + next_move: Promote a compact public certificate for the local `1..40500` rollout or keep public raw claims at `1..10000`. + - interval_id: N848.V2B + label: exact_small_n_next_extension + range: "40501..?" + status: deferred method_class: exact_small_n claim_level: target certificate: "" data_packet: "" - next_move: Decide whether exact coverage should continue directly beyond `10000` or whether the next gain should come from a different method class. + next_move: Do not extend raw exact coverage blindly; use additional exact checks only as regression evidence for the theorem lane. - interval_id: N848.V3 label: imported_computation_audit range: "public_claimed_interval" diff --git a/packs/number-theory/problems/848/OPS_DETAILS.yaml b/packs/number-theory/problems/848/OPS_DETAILS.yaml index 4a726be..34d2041 100644 --- a/packs/number-theory/problems/848/OPS_DETAILS.yaml +++ b/packs/number-theory/problems/848/OPS_DETAILS.yaml @@ -210,5 +210,10 @@ atoms: route_id: finite_check_gap_closure ticket_id: N848 status: ready - summary: The repo now has a four-anchor obstruction candidate with no failures in `30..10000`, plus a minimality ledger showing that `{7, 32, 57, 82}` is unusually strong among small anchor sets. The next move is to package that into a proof-shaped lemma with explicit obligations. + summary: >- + The repo now has public raw exact evidence through `1..10000`, local + ignored rollout evidence through `1..40500`, and a four-anchor obstruction + candidate with no failures in `30..10000`; `EXACT_INTERVAL_BOOKKEEPING.md` + is the authority for that boundary. The next move is to package the + four-anchor candidate into a proof-shaped lemma with explicit obligations. next_move: Write the theorem candidate and proof-obligation surface for the four-anchor obstruction. diff --git a/packs/number-theory/problems/848/STRUCTURAL_LIFT_CHECKLIST.json b/packs/number-theory/problems/848/STRUCTURAL_LIFT_CHECKLIST.json index 5719f2b..9bfa33e 100644 --- a/packs/number-theory/problems/848/STRUCTURAL_LIFT_CHECKLIST.json +++ b/packs/number-theory/problems/848/STRUCTURAL_LIFT_CHECKLIST.json @@ -7,7 +7,10 @@ "sourceArtifacts": { "fullMixedBaseStructuralVerifier": "FULL_MIXED_BASE_STRUCTURAL_VERIFIER.json", "structuralLiftMiner": "STRUCTURAL_LIFT_MINER.json", - "exactBaseCertificate": "EXACT_SMALL_N_1_40500_RESULTS.json" + "exactBaseCertificate": "EXACT_INTERVAL_BOOKKEEPING.md", + "publicRawExactPacket": "EXACT_SMALL_N_1_10000_RESULTS.json", + "localIgnoredRolloutPacket": "output/p848-exact-small-n-rollouts/EXACT_SMALL_N_1_40500_RESULTS.json", + "exactBaseCertificateMeaning": "bookkeeping surface; raw 1..40500 packet is local and ignored" }, "northStar": "Turn the bounded mixed-base structural verifier into an all-N proof lane by proving the cross-side matching reduction, then the p=13 and p=17 margin lifts, while keeping exact finite coverage separate.", "currentFocus": { @@ -138,59 +141,59 @@ }, { "stepId": "C2_two_cliques_plus_cross_edges", - "status": "done", - "statement": "For fixed outsider x, the compatible mixed-base graph is one clique on B7-compatible vertices, one clique on B18-compatible vertices, plus arbitrary cross edges.", - "dependsOn": [ - "C1_same_side_base_clique" - ], - "proofType": "graph_decomposition", - "proofArtifact": "p848_C2_two_cliques_plus_cross_edges_checker_v1", - "falsifierBoundary": "The graph has a same-side missing edge or an extra vertex outside the two compatible sides." - }, - { - "stepId": "C3_missing_cross_graph_definition", - "status": "done", - "statement": "Define H_{x,N} as the bipartite graph whose edges are precisely missing cross edges between compatible B7 and B18 vertices.", - "dependsOn": [ - "C2_two_cliques_plus_cross_edges" - ], - "proofType": "definition", - "proofArtifact": "p848_C3_missing_cross_graph_definition_checker_v1", - "falsifierBoundary": "A cross edge is assigned the wrong sign between compatibility and missing-cross membership." - }, - { - "stepId": "C4_clique_to_vertex_cover_duality", - "status": "done", - "statement": "A mixed-base clique equals all compatible vertices minus a vertex cover of H_{x,N}; hence max clique size is |L| + |R| minus minimum vertex cover size.", - "dependsOn": [ - "C3_missing_cross_graph_definition" - ], - "proofType": "graph_duality", - "proofArtifact": "p848_C4_clique_to_vertex_cover_duality_checker_v1", - "falsifierBoundary": "A selected clique contains a missing cross edge or a vertex cover removes more vertices than necessary." - }, - { - "stepId": "C5_konig_matching_reduction", - "status": "done", - "statement": "Because H_{x,N} is bipartite, minimum vertex cover size equals maximum matching size.", - "dependsOn": [ - "C3_missing_cross_graph_definition" - ], - "proofType": "konig_theorem", - "proofArtifact": "p848_C5_konig_matching_reduction_checker_v1", - "falsifierBoundary": "H_{x,N} is not bipartite or Konig's theorem is used outside its hypotheses." - }, - { - "stepId": "C6_mixed_clique_matching_formula", - "status": "done", - "statement": "sMixed(x,N) = |L| + |R| - maxMatching(H_{x,N}).", - "dependsOn": [ - "C4_clique_to_vertex_cover_duality", - "C5_konig_matching_reduction" - ], - "proofType": "graph_formula", - "proofArtifact": "p848_C6_mixed_clique_matching_formula_checker_v1", - "falsifierBoundary": "The formula disagrees with the verifier's Hopcroft-Karp mixed-clique computation on a certified row." + "status": "done", + "statement": "For fixed outsider x, the compatible mixed-base graph is one clique on B7-compatible vertices, one clique on B18-compatible vertices, plus arbitrary cross edges.", + "dependsOn": [ + "C1_same_side_base_clique" + ], + "proofType": "graph_decomposition", + "proofArtifact": "p848_C2_two_cliques_plus_cross_edges_checker_v1", + "falsifierBoundary": "The graph has a same-side missing edge or an extra vertex outside the two compatible sides." + }, + { + "stepId": "C3_missing_cross_graph_definition", + "status": "done", + "statement": "Define H_{x,N} as the bipartite graph whose edges are precisely missing cross edges between compatible B7 and B18 vertices.", + "dependsOn": [ + "C2_two_cliques_plus_cross_edges" + ], + "proofType": "definition", + "proofArtifact": "p848_C3_missing_cross_graph_definition_checker_v1", + "falsifierBoundary": "A cross edge is assigned the wrong sign between compatibility and missing-cross membership." + }, + { + "stepId": "C4_clique_to_vertex_cover_duality", + "status": "done", + "statement": "A mixed-base clique equals all compatible vertices minus a vertex cover of H_{x,N}; hence max clique size is |L| + |R| minus minimum vertex cover size.", + "dependsOn": [ + "C3_missing_cross_graph_definition" + ], + "proofType": "graph_duality", + "proofArtifact": "p848_C4_clique_to_vertex_cover_duality_checker_v1", + "falsifierBoundary": "A selected clique contains a missing cross edge or a vertex cover removes more vertices than necessary." + }, + { + "stepId": "C5_konig_matching_reduction", + "status": "done", + "statement": "Because H_{x,N} is bipartite, minimum vertex cover size equals maximum matching size.", + "dependsOn": [ + "C3_missing_cross_graph_definition" + ], + "proofType": "konig_theorem", + "proofArtifact": "p848_C5_konig_matching_reduction_checker_v1", + "falsifierBoundary": "H_{x,N} is not bipartite or Konig's theorem is used outside its hypotheses." + }, + { + "stepId": "C6_mixed_clique_matching_formula", + "status": "done", + "statement": "sMixed(x,N) = |L| + |R| - maxMatching(H_{x,N}).", + "dependsOn": [ + "C4_clique_to_vertex_cover_duality", + "C5_konig_matching_reduction" + ], + "proofType": "graph_formula", + "proofArtifact": "p848_C6_mixed_clique_matching_formula_checker_v1", + "falsifierBoundary": "The formula disagrees with the verifier's Hopcroft-Karp mixed-clique computation on a certified row." } ] }, @@ -311,7 +314,7 @@ { "stepId": "F1_exact_base_certificate", "status": "available", - "statement": "The exact verifier certifies N <= 40500.", + "statement": "The local compact exact rollout reaches N <= 40500; the committed raw packet reaches N <= 10000.", "dependsOn": [], "proofType": "repo_artifact_certificate", "falsifierBoundary": "The exact certificate is stale, missing, or fails rerun." diff --git a/packs/number-theory/problems/848/STRUCTURAL_LIFT_CHECKLIST.md b/packs/number-theory/problems/848/STRUCTURAL_LIFT_CHECKLIST.md index e994f29..c43ecdf 100644 --- a/packs/number-theory/problems/848/STRUCTURAL_LIFT_CHECKLIST.md +++ b/packs/number-theory/problems/848/STRUCTURAL_LIFT_CHECKLIST.md @@ -65,7 +65,7 @@ Each step is complete only when it has: ## F. Finite Closure -- `F1_exact_base_certificate` [available]: Use the exact verifier certificate for `N <= 40500`. +- `F1_exact_base_certificate` [available]: Use the local compact exact rollout for `N <= 40500`, while remembering the committed raw packet only covers `N <= 10000`. - `F2_bounded_structural_certificate` [available]: Use the full mixed-base structural verifier for `7307..7600`. - `F3_threshold_overlap` [blocked_by_E2_E4_E5]: Verify symbolic thresholds overlap the finite exact or structural certificates. - `F4_all_ranges_cover_positive_integers` [blocked_by_F3]: Combine exact base plus symbolic structural lift into an all-range cover. diff --git a/packs/number-theory/problems/848/TASK_LIST.json b/packs/number-theory/problems/848/TASK_LIST.json index fcb8e4b..1c9db91 100644 --- a/packs/number-theory/problems/848/TASK_LIST.json +++ b/packs/number-theory/problems/848/TASK_LIST.json @@ -11,13 +11,19 @@ "activeRoute": "finite_check_gap_closure", "currentClaimSurface": "bridge_backed_frontier_support", "routeSummary": "Convert the sufficiently-large-N theorem into a complete all-N resolution without overstating what is already closed or confusing imported thresholds with repo-owned claims.", - "nextHonestMove": "Decide whether to extend exact verified coverage beyond `40500` or switch method class.", - "latestVerifiedInterval": "1..40500" + "nextHonestMove": "Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed.", + "latestVerifiedInterval": "1..10000", + "exactIntervalBookkeeping": { + "publicRepoRawExactInterval": "1..10000", + "localIgnoredRolloutInterval": "1..40500", + "bookkeepingArtifact": "EXACT_INTERVAL_BOOKKEEPING.md", + "raw40500PacketCommitted": false + } }, "finiteGapStrategy": { "status": "ready", "verdict": "exact_endpoint_rollout_is_not_a_sole_all_N_closure_strategy", - "latestVerifiedInterval": "1..40500", + "latestVerifiedInterval": "1..10000", "exactMax": 40500, "operationalThreshold": { "raw": "2.64 x 10^17", @@ -32,7 +38,10 @@ "rowCount": 40500, "endpointCheckCount": 1621, "compressionRatio": 24.98457742134485, - "approximateRowsPerEndpointCheck": 24.98457742134485 + "approximateRowsPerEndpointCheck": 24.98457742134485, + "sourceStatus": "compact derivative of local ignored 1..40500 rollout", + "raw40500PacketCommitted": false, + "publicRawPacketInterval": "1..10000" }, "projectedEndpointChecksToOperationalThreshold": "10566518518516898", "projectedEndpointChecksToOperationalThresholdLabel": "10,566,518,518,516,898", @@ -42,7 +51,13 @@ "Do not wait for direct endpoint checks to close the imported finite gap.", "Prioritize auditing the imported threshold handoff or proving a stronger structural verifier lane.", "Use GPU/frontier sweeps to generate structural candidates and counterexamples, not as a substitute for the all-N handoff proof." - ] + ], + "publicRepoRawExactInterval": "1..10000", + "localIgnoredRolloutInterval": "1..40500", + "publicRepoRawExactMax": 10000, + "localIgnoredRolloutMax": 40500, + "exactMaxMeaning": "local ignored rollout max, not public raw packet max", + "bookkeepingArtifact": "EXACT_INTERVAL_BOOKKEEPING.md" }, "granularBreakdownMode": { "status": "core_loop_enabled", @@ -19631,7 +19646,7 @@ { "stepId": "verify_verifier_boundary", "title": "Verify the current exact/verifier boundary and next target", - "task": "Verify that the certified interval 1..40500 and the next verifier target remain current across the pack surfaces.", + "task": "Verify that the public raw interval `1..10000`, the local rollout `1..40500`, and the next verifier target remain current across the pack surfaces.", "completionRule": "The interval work queue or verifier boundary packet still matches the theorem-facing status.", "command": "erdos number-theory dispatch 848" }, @@ -19706,7 +19721,7 @@ "taskId": "verify_verifier_boundary", "status": "ready", "title": "Verify the current exact/verifier boundary and next target", - "task": "Verify that the certified interval 1..40500 and the next verifier target remain current across the pack surfaces.", + "task": "Verify that the public raw interval `1..10000`, the local rollout `1..40500`, and the next verifier target remain current across the pack surfaces.", "why": null, "completionRule": "The interval work queue or verifier boundary packet still matches the theorem-facing status.", "command": "erdos number-theory dispatch 848" @@ -19958,7 +19973,7 @@ { "stepId": "gap_3", "status": "next", - "task": "Decide and run the next post-40500 verification lane using local CPU and opt-in local 4090 compute only.", + "task": "Resolve the local 1..40500 promotion boundary, then use further exact runs only as local/free regression evidence.", "source": "formalization_work", "command": "erdos problem formalization-work-refresh 848" }, @@ -19979,7 +19994,7 @@ { "stepId": "decide_post_40500_verification_lane", "status": "high", - "task": "The canonical exact base currently ends at 1..40500. The next verification move is still open.", + "task": "Resolve the local 1..40500 promotion boundary; public raw packet currently ends at 1..10000.", "source": "exact_verifier", "command": "erdos number-theory dispatch 848" }, @@ -22198,7 +22213,7 @@ { "stepId": "regime_b_endpoint_verifier_backend", "status": "high", - "task": "Continue the active endpoint-monotonicity exact verifier beyond 1..40500 (1621 endpoint checks cover 40500 rows; compression 24.98x).", + "task": "Treat endpoint-monotonicity checks beyond the local 1..40500 rollout as deferred regression evidence; do not promote them before the compact certificate boundary is settled.", "source": "exact_breakpoint_certificate", "command": "erdos number-theory dispatch 848 --apply --action exact_followup_rollout --exact-chunks 5 --exact-chunk-size 1000 --endpoint-monotonicity" } diff --git a/packs/number-theory/problems/848/TASK_LIST.md b/packs/number-theory/problems/848/TASK_LIST.md index 1b2676c..9cd3eac 100644 --- a/packs/number-theory/problems/848/TASK_LIST.md +++ b/packs/number-theory/problems/848/TASK_LIST.md @@ -8,8 +8,8 @@ This task list is the canonical research-loop surface for the problem. It gives - Active route: `finite_check_gap_closure`. - Current claim surface: `bridge_backed_frontier_support`. - Route summary: Convert the sufficiently-large-N theorem into a complete all-N resolution without overstating what is already closed or confusing imported thresholds with repo-owned claims. -- Next honest move: Decide whether to extend exact verified coverage beyond `40500` or switch method class. -- Latest verified interval: `1..40500` +- Next honest move: Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed. +- Latest exact interval: public raw `1..10000`; local rollout `1..40500` ## Execution Rule @@ -399,7 +399,7 @@ This task list is the canonical research-loop surface for the problem. It gives - `audit_theorem_surfaces`: Audit theorem, claim, and formalization surfaces for consistency | Audit the theorem loop, claim loop, claim pass, formalization packet, and formalization work packet for drift or contradictory wording. | completion: The canonical theorem/search surfaces tell one consistent story about what is supported, what is open, and what the active work unit is. | command: `erdos problem task-list 848` - `verify_canonical_inputs`: Verify canonical bridge inputs against the latest harvested compute artifacts | Verify that the bridge-backed theorem surfaces still match the latest harvested compute and frontier evidence. | completion: The canonical input packet for this loop remains current and trustworthy. | command: `erdos number-theory bridge-refresh 848` - `verify_primary_structural_hook`: Verify the primary structural hook remains canonical | Verify that the `282 <-> 137720141` alignment remains canonical across theorem, claim, and bridge surfaces. | completion: The primary theorem-facing hook still survives refresh and remains narrow enough to formalize honestly. | command: `erdos problem claim-pass-refresh 848` -- `verify_verifier_boundary`: Verify the current exact/verifier boundary and next target | Verify that the certified interval 1..40500 and the next verifier target remain current across the pack surfaces. | completion: The interval work queue or verifier boundary packet still matches the theorem-facing status. | command: `erdos number-theory dispatch 848` +- `verify_verifier_boundary`: Verify the current exact/verifier boundary and next target | Verify that the public raw interval `1..10000`, the local rollout `1..40500`, and the next verifier target remain current across the pack surfaces. | completion: The interval work queue or verifier boundary packet still matches the theorem-facing status. | command: `erdos number-theory dispatch 848` - `apply_granular_breakdown`: Apply ORP granular breakdown before execution | Run ORP granular breakdown on the active topic `problem 848 | Explain the 282 First-Failure Mechanism | active atom D2_p13_matching_lower_bound | target D4_matching_bound_implies_sMaxMixed_bound` and compress it into one active target plus one verification command. | completion: The broad work packet has been decomposed into boundary, lanes, atomic obligations, dependency ladder, active target, durable checklist, and next verification. | command: `orp mode breakdown granular-breakdown --topic "problem 848 | Explain the 282 First-Failure Mechanism | active atom D2_p13_matching_lower_bound | target D4_matching_bound_implies_sMaxMixed_bound" --json` - `execute_current_work_packet`: Explain the 282 First-Failure Mechanism | Isolate the extra square witness that makes continuation 282 fail first on the shared-prefix boundary class. | completion: The first remaining gap is either discharged, narrowed, or replaced by a sharper one: Prove structural-lift atom D2_p13_matching_lower_bound: For p=13 threatening rows, maxMatching(H_{x,N}) is at least the required matching bound extracted from the margin inequality. | command: `erdos problem formalization-work 848` - `refresh_and_rerank`: Refresh the task list and rerank the next step | Refresh the canonical task list after the completed work so the next iteration is driven by the newest theorem/search/verifier evidence. | completion: The refreshed task list records the next highest-value action instead of relying on a stale fixed script. | command: `erdos problem task-list-refresh 848` @@ -419,7 +419,7 @@ This task list is the canonical research-loop surface for the problem. It gives - `audit_theorem_surfaces` [ready] Audit theorem, claim, and formalization surfaces for consistency | Audit the theorem loop, claim loop, claim pass, formalization packet, and formalization work packet for drift or contradictory wording. | completion: The canonical theorem/search surfaces tell one consistent story about what is supported, what is open, and what the active work unit is. | command: `erdos problem task-list 848` - `verify_canonical_inputs` [ready] Verify canonical bridge inputs against the latest harvested compute artifacts | Verify that the bridge-backed theorem surfaces still match the latest harvested compute and frontier evidence. | completion: The canonical input packet for this loop remains current and trustworthy. | command: `erdos number-theory bridge-refresh 848` - `verify_primary_structural_hook` [ready] Verify the primary structural hook remains canonical | Verify that the `282 <-> 137720141` alignment remains canonical across theorem, claim, and bridge surfaces. | completion: The primary theorem-facing hook still survives refresh and remains narrow enough to formalize honestly. | command: `erdos problem claim-pass-refresh 848` -- `verify_verifier_boundary` [ready] Verify the current exact/verifier boundary and next target | Verify that the certified interval 1..40500 and the next verifier target remain current across the pack surfaces. | completion: The interval work queue or verifier boundary packet still matches the theorem-facing status. | command: `erdos number-theory dispatch 848` +- `verify_verifier_boundary` [ready] Verify the current exact/verifier boundary and next target | Verify that the public raw interval `1..10000`, the local rollout `1..40500`, and the next verifier target remain current across the pack surfaces. | completion: The interval work queue or verifier boundary packet still matches the theorem-facing status. | command: `erdos number-theory dispatch 848` - `apply_granular_breakdown` [ready] Apply ORP granular breakdown before execution | Run ORP granular breakdown on the active topic `problem 848 | Explain the 282 First-Failure Mechanism | active atom D2_p13_matching_lower_bound | target D4_matching_bound_implies_sMaxMixed_bound` and compress it into one active target plus one verification command. | completion: The broad work packet has been decomposed into boundary, lanes, atomic obligations, dependency ladder, active target, durable checklist, and next verification. | command: `orp mode breakdown granular-breakdown --topic "problem 848 | Explain the 282 First-Failure Mechanism | active atom D2_p13_matching_lower_bound | target D4_matching_bound_implies_sMaxMixed_bound" --json` - `execute_current_work_packet` [in_progress] Explain the 282 First-Failure Mechanism | Isolate the extra square witness that makes continuation 282 fail first on the shared-prefix boundary class. | The live 137720141 / 282 obstruction packet is checked at finite-menu scope; the remaining theorem work is the narrower symbolic-lift boundary. | completion: The first remaining gap is either discharged, narrowed, or replaced by a sharper one: Prove structural-lift atom D2_p13_matching_lower_bound: For p=13 threatening rows, maxMatching(H_{x,N}) is at least the required matching bound extracted from the margin inequality. | command: `erdos problem formalization-work 848` - `discharge_first_remaining_gap` [ready] Discharge the first remaining gap in the active theorem packet | Prove structural-lift atom D2_p13_matching_lower_bound: For p=13 threatening rows, maxMatching(H_{x,N}) is at least the required matching bound extracted from the margin inequality. | This is the sharpest unresolved statement already named by the active theorem-work packet. | completion: The first remaining gap is either resolved or replaced by a more precise successor gap. | command: `erdos problem formalization-work-refresh 848` @@ -470,10 +470,10 @@ This task list is the canonical research-loop surface for the problem. It gives - `gap_1` [next] Prove structural-lift atom D2_p13_matching_lower_bound: For p=13 threatening rows, maxMatching(H_{x,N}) is at least the required matching bound extracted from the margin inequality. | source: formalization_work | command: `erdos problem formalization-work-refresh 848` - `gap_2` [next] Advance the same atomic packet toward target D4_matching_bound_implies_sMaxMixed_bound: If maxMatching(H_{x,N}) >= K(N), then sMixed(x,N) <= |L| + |R| - K(N). | source: formalization_work | command: `erdos problem formalization-work-refresh 848` -- `gap_3` [next] Decide and run the next post-40500 verification lane using local CPU and opt-in local 4090 compute only. | source: formalization_work | command: `erdos problem formalization-work-refresh 848` +- `gap_3` [next] Resolve the local 1..40500 promotion boundary, then use further exact runs only as local/free regression evidence. | source: formalization_work | command: `erdos problem formalization-work-refresh 848` - `formalize_282_alignment` [high] The bridge matches shared-prefix representative 137720141 with tracked tail 282 first failure 137720141. | source: theorem_formalization | command: `erdos problem formalization 848` - `formalize_top_repair_cluster` [high] Top cluster 432, 782, 832 shares repaired-known=26, repaired-predicted=242, clean-through=250075000. | source: theorem_formalization | command: `erdos problem formalization 848` -- `decide_post_40500_verification_lane` [high] The canonical exact base currently ends at 1..40500. The next verification move is still open. | source: exact_verifier | command: `erdos number-theory dispatch 848` +- `decide_post_40500_verification_lane` [high] Resolve the local 1..40500 promotion boundary; public raw packet currently ends at 1..10000. | source: exact_verifier | command: `erdos number-theory dispatch 848` - `model_repair_pool_growth` [medium] Recent bridge packets introduced new square moduli: 1369, 841, 17161, 1849. | source: theorem_formalization | command: `erdos problem formalization 848` - `finite_gap_strategy_handoff` [high] Use the finite-gap strategy readout: endpoint rollout is useful, but exact-only closure would still require about 10,566,518,518,516,898 endpoint checks to reach the imported 2.64 x 10^17 handoff. | source: finite_gap_strategy | command: `erdos problem task-list-refresh 848` - `implement_full_common_core_pair_export` [done] Extend the matching-pattern miner so every split profile exports the full common matching core, not only commonMatchingPairSample. | source: split_core_atomization_plan | command: `erdos problem task-list-refresh 848` @@ -636,7 +636,7 @@ This task list is the canonical research-loop surface for the problem. It gives - `mixed_base_failure_scout` [ready] Use the mixed-base failure scout: status sampled_union_failures_repaired_by_mixed_base_clique; analyzed 8 union-failure rows with 0 mixed-base failures. | source: mixed_base_failure_scout | command: `erdos number-theory dispatch 848 --apply --action mixed_base_failure_scout --mixed-base-max-rows 40` - `full_mixed_base_structural_verifier` [ready] Use the full mixed-base structural verifier: status bounded_full_mixed_base_structural_verifier_certified over 7307..7600; exact threatening-outsider checks 1733, mixed failures 0. | source: full_mixed_base_structural_verifier | command: `erdos number-theory dispatch 848 --apply --action full_mixed_base_structural_verifier --structural-min 7307 --structural-max 7600` - `structural_lift_miner` [ready] Use the structural lift miner: status structural_lift_obligation_packet_ready; mined 64 exact mixed rows; next theorem lane formalize_cross_side_matching_bound_then_exact_prime_margin_lift. | source: structural_lift_miner | command: `erdos number-theory dispatch 848 --apply --action structural_lift_miner` -- `regime_b_endpoint_verifier_backend` [high] Continue the active endpoint-monotonicity exact verifier beyond 1..40500 (1621 endpoint checks cover 40500 rows; compression 24.98x). | source: exact_breakpoint_certificate | command: `erdos number-theory dispatch 848 --apply --action exact_followup_rollout --exact-chunks 5 --exact-chunk-size 1000 --endpoint-monotonicity` +- `regime_b_endpoint_verifier_backend` [high] Treat endpoint-monotonicity checks beyond the local 1..40500 rollout as deferred regression evidence; do not promote them before the compact certificate boundary is settled. | source: exact_breakpoint_certificate | command: `erdos number-theory dispatch 848 --apply --action exact_followup_rollout --exact-chunks 5 --exact-chunk-size 1000 --endpoint-monotonicity` ## Commands diff --git a/packs/number-theory/problems/848/TASK_LOOP_RUN.json b/packs/number-theory/problems/848/TASK_LOOP_RUN.json index af42ce1..efbad8a 100644 --- a/packs/number-theory/problems/848/TASK_LOOP_RUN.json +++ b/packs/number-theory/problems/848/TASK_LOOP_RUN.json @@ -4544,5 +4544,9 @@ "taskListMarkdownPath": "/Volumes/Code_2TB/code/erdos-problems/packs/number-theory/problems/848/TASK_LIST.md", "taskLoopRunJsonPath": "/Volumes/Code_2TB/code/erdos-problems/packs/number-theory/problems/848/TASK_LOOP_RUN.json", "taskLoopRunMarkdownPath": "/Volumes/Code_2TB/code/erdos-problems/packs/number-theory/problems/848/TASK_LOOP_RUN.md" - } + }, + "bookkeepingStatus": "historical_run_log_not_current_interval_authority", + "currentIntervalAuthority": "EXACT_INTERVAL_BOOKKEEPING.md", + "publicRepoRawExactInterval": "1..10000", + "localIgnoredRolloutInterval": "1..40500" } diff --git a/packs/number-theory/problems/848/TASK_LOOP_RUN.md b/packs/number-theory/problems/848/TASK_LOOP_RUN.md index f4c32a4..2601a11 100644 --- a/packs/number-theory/problems/848/TASK_LOOP_RUN.md +++ b/packs/number-theory/problems/848/TASK_LOOP_RUN.md @@ -1,5 +1,7 @@ # Erdos Problem #848 Task Loop Run +Historical bookkeeping note: this is a run log, not the current interval authority. Use `EXACT_INTERVAL_BOOKKEEPING.md` for the current distinction between public raw `1..10000` and local rollout `1..40500`. + - Problem id: `848` - Requested passes: `250` - Executed passes: `250` @@ -8,7 +10,7 @@ - Converged at pass: `2` - Active route: `finite_check_gap_closure` - Current claim surface: `bridge_backed_frontier_support` -- Latest verified interval: `1..11300` +- Historical run latest interval: `1..11300` - Highest-value next step: `gap_1` | Show whether the 132-activation sequence should be described as a controlled interaction between the shared-prefix class and the 282 repair congruence rather than as a packet-specific coincidence. - Highest-value command: `erdos problem formalization-work-refresh 848` diff --git a/packs/number-theory/problems/848/THEOREM_LOOP.json b/packs/number-theory/problems/848/THEOREM_LOOP.json index 7aa00f5..11dafa9 100644 --- a/packs/number-theory/problems/848/THEOREM_LOOP.json +++ b/packs/number-theory/problems/848/THEOREM_LOOP.json @@ -17,7 +17,13 @@ "problemSolved": false, "currentClaimSurface": "bridge_backed_frontier_support", "routeSummary": "Convert the sufficiently-large-N theorem into a complete all-N resolution without overstating what is already closed or confusing imported thresholds with repo-owned claims.", - "nextHonestMove": "Decide whether to extend exact verified coverage beyond `40500` or switch method class." + "nextHonestMove": "Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed.", + "exactIntervalBookkeeping": { + "publicRepoRawExactInterval": "1..10000", + "localIgnoredRolloutInterval": "1..40500", + "bookkeepingArtifact": "EXACT_INTERVAL_BOOKKEEPING.md", + "raw40500PacketCommitted": false + } }, "theoremHooks": [ { @@ -46,7 +52,7 @@ "item_id": "choose_next_finite_gap_move", "status": "ready", "task": "Choose the next finite-gap closure move and keep the theorem-facing claim surface honest.", - "why": "Decide whether to extend exact verified coverage beyond `40500` or switch method class." + "why": "Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed." }, { "item_id": "explain_next_unmatched_alignment", diff --git a/packs/number-theory/problems/848/THEOREM_LOOP.md b/packs/number-theory/problems/848/THEOREM_LOOP.md index 55aa0fb..e8807cd 100644 --- a/packs/number-theory/problems/848/THEOREM_LOOP.md +++ b/packs/number-theory/problems/848/THEOREM_LOOP.md @@ -13,7 +13,7 @@ This theorem loop is generated from a richer search/theorem bridge, then exposed - Open problem: `no`. - Theorem module: `(none)`. - Route summary: Convert the sufficiently-large-N theorem into a complete all-N resolution without overstating what is already closed or confusing imported thresholds with repo-owned claims. -- Next honest move: Decide whether to extend exact verified coverage beyond `40500` or switch method class. +- Next honest move: Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed. ## Theorem Hooks @@ -24,7 +24,7 @@ This theorem loop is generated from a richer search/theorem bridge, then exposed ## Theorem Agenda -- `choose_next_finite_gap_move`: ready | Choose the next finite-gap closure move and keep the theorem-facing claim surface honest. | Decide whether to extend exact verified coverage beyond `40500` or switch method class. +- `choose_next_finite_gap_move`: ready | Choose the next finite-gap closure move and keep the theorem-facing claim surface honest. | Promote or reject the local `1..40500` rollout; public raw exact claims remain `1..10000` until that handoff is committed. - `explain_next_unmatched_alignment`: ready | Explain structurally why shared-prefix representative `137720141` aligns with the first failure of tail `282`. | If that alignment is structural rather than accidental, it turns a search coincidence into a theorem-facing obstruction class. - `explain_completed_vs_search_leader_split`: ready | Explain why completed structured tail `332` differs from current family-aware leader `432`. | That split tells us whether the live frontier is a finite-window artifact or a genuinely better structural continuation class. - `model_repair_pool_growth`: ready | Model the repaired square-modulus pool as a growing family rather than treating it as already closed. | Recent packets introduced new square moduli, so the theorem lane should aim for controlled growth, not premature closure. diff --git a/packs/number-theory/problems/848/VERIFICATION_REGIMES.md b/packs/number-theory/problems/848/VERIFICATION_REGIMES.md index 8b8c069..5110d2f 100644 --- a/packs/number-theory/problems/848/VERIFICATION_REGIMES.md +++ b/packs/number-theory/problems/848/VERIFICATION_REGIMES.md @@ -86,7 +86,6 @@ Desired certificate: - Regime D: public asymptotic theorem exists; imported explicit thresholds are tracked but not yet repo-audited -So the next honest move is to decide whether exact-small-`N` coverage should be extended -directly beyond `10000`, or whether the next gain comes from -auditing imported computation or -switching method class. +So the next honest move is to resolve the local `1..40500` promotion boundary while keeping +the committed raw exact packet at `1..10000`, then decide whether the next gain comes from +auditing imported computation, compacting the local rollout, or switching method class. diff --git a/packs/number-theory/problems/848/context.yaml b/packs/number-theory/problems/848/context.yaml index bb0e884..aa0f9de 100644 --- a/packs/number-theory/problems/848/context.yaml +++ b/packs/number-theory/problems/848/context.yaml @@ -5,7 +5,7 @@ default_active_route: finite_check_gap_closure bootstrap_focus: Treat Problem 848 as a finite-gap closure problem and freeze the certificate surface before claiming bounded verification progress. route_story: Problem 848 is already asymptotically resolved in public, but not yet closed here for all N. The honest job is to shrink the finite remainder with audited threshold tracking and reproducible bounded verification, and then turn the exact packet into a short structural theorem. frontier_label: finite_check_gap_closure -frontier_detail: The repo now has a verified exact interval `1..10000`, a four-anchor obstruction candidate with no failures in `30..10000`, and evidence that this is the first serious theorem route. The next question is how to prove that obstruction and convert it into a breakpoint law. +frontier_detail: The repo now has a committed raw exact interval `1..10000`, local ignored rollout evidence through `1..40500`, a four-anchor obstruction candidate with no failures in `30..10000`, and evidence that this is the first serious theorem route. The next question is how to prove that obstruction and convert it into a breakpoint law. checkpoint_focus: Preserve the distinction between existential N0, explicit N0, sample finite checks, and full closure. next_honest_move: Promote the four-anchor obstruction from recon to a proof-shaped lemma candidate with explicit proof obligations. related_core_problems: @@ -50,6 +50,7 @@ question_ledger: - The repo now has an audited explicit candidate package distinct from the imported public threshold timeline. - The repo has now chosen bounded finite verification as the next closure lane. - The repo now has an exact verified base interval `1..10000`. + - Local ignored rollout artifacts extend exact evidence to `1..40500`, but the public raw packet remains `1..10000` until a compact promotion is committed. - The exact verifier now uses an incremental update rule rather than rebuilding every instance from scratch. - The repo now has a four-anchor obstruction candidate with no failures in `30..10000`. problem_solved: [] diff --git a/problems/848/EVIDENCE.md b/problems/848/EVIDENCE.md index 95ca291..5335958 100644 --- a/problems/848/EVIDENCE.md +++ b/problems/848/EVIDENCE.md @@ -75,6 +75,9 @@ Current public evidence captured locally: truth. - A reproducible exact maximum-clique scan now verifies the expected extremal size for every `N` in `1..10000`, giving the bounded-verification lane a much larger trusted covered interval. +- Local ignored rollout artifacts extend exact small-`N` evidence to `1..40500`; because the + raw packet is about 440 MB, public-facing claims must distinguish this local rollout from the + committed `1..10000` raw result packet. - The exact verifier has been rebuilt incrementally, so the old post-`3000` cost wall is now understood to have been mostly a tooling artifact rather than a serious mathematical barrier. - The exact packet now exposes a structural clue: every maximum witness through `10000` is the @@ -111,6 +114,8 @@ Claim-safe local posture: - Exact: the repo now also has a theorem-style proof artifact for the current candidate. - Exact: the current candidate package is now surfaced for both paper-writing and public review workflows. +- Exact: the committed public raw exact interval is `1..10000`; the `1..40500` interval is + local compact rollout evidence until a public compact certificate is promoted. - Exact: the paper bundle for the current candidate is now fully drafted at the section-shell level and no longer depends on placeholder text in its public-facing sections. - Heuristic: the lowest-friction route from here is to work both sides of the bridge: diff --git a/problems/848/ROUTES.md b/problems/848/ROUTES.md index d2b3dbf..3f165fd 100644 --- a/problems/848/ROUTES.md +++ b/problems/848/ROUTES.md @@ -75,6 +75,8 @@ - a certificate format for bounded interval claims - an audit ledger for imported verification work - an exact verified base interval `1..10000` + - local ignored exact rollout evidence through `1..40500`, tracked separately from the + committed raw packet - an incremental verifier that makes larger exact tranches practical - The next concrete task is to turn the four-anchor obstruction clue into a proof-shaped lemma candidate and then use it to attack the breakpoint law. diff --git a/problems/848/SHARE_READY_SUMMARY.md b/problems/848/SHARE_READY_SUMMARY.md index 0b15f9e..10b6c0d 100644 --- a/problems/848/SHARE_READY_SUMMARY.md +++ b/problems/848/SHARE_READY_SUMMARY.md @@ -24,6 +24,8 @@ What is ready now: - a bounded finite-verification lane with regimes, certificate requirements, and external audit notes - an exact verified base interval `1..10000` +- local ignored exact rollout evidence through `1..40500`, not yet promoted as a public raw + artifact - a four-anchor obstruction candidate and minimality ledger for the first theorem-style route What is not being claimed: