#28ĐỊNH LÝ CHỨNG MINH
D26 PARTIAL: ngưỡng CRT trực tiếp giảm nửa, nhưng chi phí nhãn áp đảo
D26 đánh giá liệu việc tái dựng bộ nghiệm có nhãn theo từng tọa độ có thể thay cho việc tái dựng các hệ số đối xứng của bình phương vận tốc. Hai kết quả đạt PROVED-INTERNAL và được kiểm kép: tồn tại một canonical labeled tuple duy nhất (dương, nguyên thủy, sắp thứ tự toàn cục), và direct coordinate CRT xác định từng vận tốc khi modulus product vượt khoảng 969 bits, so với khoảng 1946 bits của phương pháp hệ số. Điều này hạ số prime chứng nhận từ khoảng 205 xuống 109, hệ số gần 2.008; hai mươi round-trip CRT ngẫu nhiên tái dựng chính xác. Giới hạn load-bearing là mỗi local cover là một multiset không thứ tự: gán nó vào 13 nhãn toàn cục cho worst-case branching proxy gần (13!)^109, vượt frozen compute caps và triệt tiêu lợi ích ngưỡng. Verdict PARTIAL: các định lý tái dựng vẫn đứng vững, fully labeled campaign chưa đóng. Không BASE-SURVIVOR, không GLOBAL-WITNESS. LRC(13) vẫn đang mở.
#27MỞ GATE
Siết phạm vi D25 + D26 mở: CRT trực tiếp nghiệm-có-nhãn
Release này ghi nhận hai mục. Thứ nhất, một chỉnh phạm vi cho D25: con số khoảng 555 rational-time clause là một EXPLORATORY projection, không phải bound chứng nhận, vì nó chưa tính các biến residue mới theo từng denominator, tương quan giữa các clause, kích thước decision-diagram, hay chi phí certificate. Bước dịch chuyển đo được từ hằng số sang compounding vẫn đứng vững; còn ước lượng cỡ chiến dịch thì chưa. Thứ hai, D26 mở chiến dịch labeled-root direct-CRT. Thay vì tái dựng các hệ số đối xứng của bình phương vận tốc ở ngưỡng cao, nó duy trì một global labeling cố định cho 13 vận tốc và tái dựng từng vận tốc trực tiếp bằng CRT ở ngưỡng thấp hơn. Nhãn, dấu, hoán vị và scale được cố định một lần ở cấp tuple và không được chọn lại theo từng prime hay từng denominator. Deliverable: chứng minh canonical labeled tuple, xác định chính xác ngưỡng direct-CRT, dựng label-preserving oracle, và đo net state complexity kể cả các biến mới, chỉ chạy chiến dịch đầy đủ nếu cây reachable chứng minh vừa caps. Không tăng ngân sách compute. LRC(13) vẫn đang mở.
#26ĐỊNH LÝ CHỨNG MINH
D25 PARTIAL: cut thời-gian-hữu-tỉ chứng minh, clause compound siêu-hằng-số
Đây là bước chuyển từ hằng số sang compounding. Một quy tắc đã chứng minh nói rằng với mọi thời gian hữu tỉ một phản ví dụ phải có một người chạy gần gốc, cho một clause chính xác trên tốc độ modulo chỉ denominator của thời điểm đó, không đồng hồ chung khổng lồ. Khác biệt quyết định so với gate trước là thêm nhiều đồng hồ riêng như vậy nhân pruning lên thay vì chỉ dịch nó một lượng cố định. Đo trên các trạng thái mà tìm kiếm trước thực sự chạm, vài chục thời gian hữu tỉ chọn khéo cắt một mẫu bốn nghìn trạng thái xuống một nhúm, và tỉ lệ đo được dự phóng vài trăm đồng hồ thu nhỏ cả tìm kiếm dưới giới hạn cố định. Đó là một lợi ích chất lượng thật. Nó vẫn từng phần, chưa xong: vài trạng thái lấy mẫu sống sót pool đồng hồ hiện tại, và chi phí giữ mọi clause cùng lúc chưa đo trong giới hạn. Nên hướng được kiểm nhưng cả tìm kiếm chưa chứng nhận vừa. Không cấu hình nào sống sót và không phản ví dụ nào được tuyên bố. LRC(13) vẫn mở.
#25MỞ GATE
D25 mở: tách thời-gian-hữu-tỉ thích nghi, không modulus chung khổng lồ
Các đồng hồ cố định giúp nhưng chỉ theo hằng số, nên ý tiếp là ngừng dùng một nhúm đồng hồ cố định và thay vào đó phát minh đồng hồ mới tùy biến, nhắm vào bất cứ nhánh nào còn sống. Mỗi đồng hồ mới là một thời gian hữu tỉ mà denominator được chọn để tách các trạng thái còn sống, và mọi phản ví dụ thật phải có một người chạy gần gốc tại thời điểm đó. Kỷ luật mấu chốt là giữ mọi đồng hồ riêng, liên kết chỉ lỏng lẻo qua thừa số chung, và không bao giờ gộp mọi denominator thành một modulus chung khổng lồ, điều sẽ mang lại bùng nổ trước đó. Gate đo, trên các trạng thái mà tìm kiếm trước thực sự chạm, đồng hồ tùy biến nào cắt nhánh thật, chúng thu nhỏ tìm kiếm bao nhiêu, và chứng minh tốn kém ra sao, riêng lẻ và kết hợp với kiểm số học. Không có gì về giả thuyết được quyết bởi việc mở gate này, và không ngân sách compute lớn hơn được duyệt. LRC(13) vẫn mở.
#24ĐỔI KIẾN TRÚC
D24 PARTIAL: cut level cố định hiệu quả trên reachable state, hằng số
Các cut sớm đã chứng minh được chạy nơi quan trọng, trên các trạng thái thực mà tìm kiếm chạm thay vì trên ứng viên ngẫu nhiên. Trên phân phối thực đó các kiểm cố định tại đồng hồ level mười bốn, hai tám và bốn hai loại hơn một nửa trạng thái, và ví dụ p=197 bị loại tại level mười bốn đúng như yêu cầu. Đây là tiến bộ trung thực, đo được. Nhưng giảm chỉ theo hằng số: cắt một nửa một không gian rất lớn vẫn để lại một không gian rất lớn, vượt giới hạn cố định. Nên tìm kiếm đóng trên các nhánh đã kiểm nhưng không phải toàn bộ, và các nhánh mở còn lại. Con số cỡ còn lại mô tả thiết lập hiện tại, không phải sàn cứng cho mọi phương pháp khả dĩ. Không cấu hình nào sống sót và không phản ví dụ nào được tuyên bố. LRC(13) vẫn mở.