diff --git a/research/bit-fixed-source-price-gates/PROOF.md b/research/bit-fixed-source-price-gates/PROOF.md new file mode 100644 index 0000000000..17348dd52e --- /dev/null +++ b/research/bit-fixed-source-price-gates/PROOF.md @@ -0,0 +1,180 @@ +# Two fixed-source BIT price gates + +These are two separate applications of complete paid and target accounting. +Neither gives a new supplier or a multiplication kappa value. + +## 1. Fresh commuting axes on the fixed PR589 word + +Fix the original scalar events, native frame paths, and owned operations. +All free maps act as the identity on the added axes. The main boundaries and +all target credits outside the selected helper set stay unchanged. A field +state can carry any subset of the new commuting axes. Scalar contacts must +have the same subset. A native MOVE with original rank r and a change of s +new axes has rank r+s; this direct-sum charge is part of the lift contract. + +Choose a nonempty set of helpers and add k>0 fresh commuting axes to each +chosen final helper job. The physical k is an integer. The original helper +job has rank eight. Each chosen helper starts with no new axis and ends with +k new axes. Along its own register path, let s_j count the changed new axes +at MOVE j. Every final axis must change at least once, so sum_j s_j>=k. +Scalar events cannot make this change. An owned COPY does not change its +persistent source register. + +The exact source census shows that every helper has a paid MOVE and that +every such MOVE has original rank r_j<=7. Different persistent helper paths +use distinct MOVE events. For f(r)=r^(1-C), 0=g(a+b). This follows by writing each increment as an integral of +the decreasing derivative of f. Hence the paid increment on one helper path +is at least + + sum_j [f(r_j+s_j)-f(r_j)] + >= sum_j g(s_j) + >= g(sum_j s_j) + >= g(k) + > f(8+k)-f(8). + +The final strict inequality follows from strict concavity and 7<8. This is +larger than the new helper target credit. Distinct helper paths give distinct +charges. Further copied fields and boundary work have nonnegative cost. +Every nonempty choice loses. The same proof permits different positive k +values on different chosen helpers. + +Reversing the source leaves each helper's own MOVE ranks unchanged. The BIT +rank-eight helper job is an involution, so the same target rank and argument +apply in the reverse direction. The verifier checks the two rank censuses; +it does not claim a new native reverse-word replay. + +This proof fixes the original word and its contact rules. It does not cover +new scalar operations, status-changing free maps, different output jobs, +preloaded added-axis status, shared persistent ownership, or a different +native operation. No mincut computation is needed for the theorem. + +## 2. The retained paired-k3 p12 source + +Fix the paired-triple geometry parameter at 12. The retained generator and +frozen matching give h=24, v=1760, R=19788 and centre debt c=528. Let L_r be +the complete local paid histogram, including both main boundary legs. Let +H=R H24 be the complete local helper target list. The source compiler gives + + sum_r r L_r - 24 R = 2 v (24-1) + 528. + +The verifier reconstructs L from the unchanged generator, checks the scalar +decoder, and includes its target-side main legs and source-side main legs. +Each main side has rank mass v(24-1). No productive helper is made free or +credited twice. The retained compiler's modular-rank argument and native +invoice convention are inherited; this is not a new native admission proof. +The predecessor's standalone independent `check_paired_cube_bit.py` is not +rerun. The tariff conclusion applies to the reconstructed generator invoice. + +Let p>=1 now denote the balanced controller parameter, not the geometry +parameter. Put d=23 and let a=floor((p-1)/2), b=p-1-a. Its paid list is + + (p+2)L + v(p-1)H1 + + 2v sum_(s in {a,b}) sum_(j=1)^s H_(d(j+1)). + +Its target list is + + (p+2)R H24 + 2v H_(1+d(p+2)) + + 2v sum_(s in {a,b}) sum_(j=1)^s H_(1+d(j+1)). + +The exact target rank minus paid rank is 1232p+704. This positive rank +surplus is not enough to obtain a useful exponent. + +Set C=1/500 and t=1-C. Let delta be the local paid moment minus local helper +moment, and let M(p) be the complete target moment minus paid moment. Each +side pair contributes at most one unit before multiplication by 2v: + + (x+1)^t-x^t <= 1. + +There are p-1 such pairs. Subtracting the thin calls gives + + M(p) <= U(p) + U(p) = -(p+2)delta + v(p-1) + 2v(1+d(p+2))^t. + +The verifier uses exact rational enclosures from the retained positive-series +engine. It proves M(p)<0 for p=1,...,64. It also proves U(64)<0 and U'(64)<0, +using a lower enclosure for delta and upper enclosures for the positive +endpoint terms. Since U''(p)<0, the derivative decreases. Therefore U(p)<0 +and M(p)<0 for every real p>=64. These checks cover every positive integer +controller parameter. + +To interpret this as a raw-saving bound, normalize M by 24^t. Every local +paid rank is less than 24, which the verifier checks. The normalized negative +local term decreases with C. The normalized thin debit also decreases. The +endpoint rank exceeds 24, so its normalized credit decreases with C. Every +side pair has x>=46>24. The function + + ((x+1)/24)^t-(x/24)^t + +increases with t>0: the derivative of y^t log y in y is positive for y>1. +Hence each normalized side credit decreases with C. Thus M/24^t is strictly +decreasing for 00 and M(1/500)<0, the raw crossing +for each p is strictly below 1/500. + +The retained p=11 crossing lies in + + (0.00164539220, 0.00164539221). + +It is a positive sign-change control. This package does not claim that p=11 +is the global optimum. It performs no floating root search, matching search, +or scan over other source geometries. + +This second gate fixes the p12 module, decoder, matching, full unnormalized +invoice, and balanced caller. It does not cover a changed local recipe, +partial-gauge optimization, another geometry parameter, or another caller. +Its raw crossing is not the complete multiplication exponent. + +## Source-rank appendix: permutation-only completion + +This appendix bounds binary correction rank, not native factorization cost. +Let J be the 111-by-111 noCOPY matrix in the pinned PR589-H-NATIVE source. +The source factors A=J+I as U V, with rank nine. Thus U and V both have rank +nine, and A and U have the same column code. The 511 nonzero words in this +code all have weight at least 48. The verifier checks this exact +code and its full weight distribution. + +Suppose a permutation matrix P had rank(J+P)<=8. Then + + rank(P+I) <= rank(J+P)+rank(J+I) <= 17. + +A nontrivial permutation cycle of length l moves l rows and contributes +l-1 to rank(P+I). Since l<=2(l-1) for l>=2, P can move at most 34 rows. +Delete these moved rows from A. The remaining rows still have rank nine: +a nonzero vector in the column code of U cannot be supported on only 34 rows, +because its minimum weight is 48. On every remaining row P equals I, so J+P +agrees with A there. Hence rank(J+P)>=9, a contradiction. + +The identity permutation attains rank nine. Thus + + min_(P a permutation matrix) rank(J+P) = 9. + +The retained arbitrary-invertible completion changes three rows and yields +an invertible output code. Its target code need not be a permutation. That +rank-three construction does not contradict this permutation-only theorem. +Conversely, this theorem gives no lower bound on the native cost of a new +factorization, a general invertible output code, or a multi-call controller. +The direct-sum plane price screen is not part of this appendix. + +## Exact evidence and controls + +RESULT.json contains outward rational enclosures, rounded by integer floor +and ceiling to a denominator of 10^12. The verifier checks the unrounded +exact signs first and checks that every displayed enclosure contains them. +No floating-point value enters either gate. + +Ten live input files are pinned before external source code is loaded. The +verifier executes those source bytes directly and does not use an inherited +bytecode cache. Changed bytes in every source are rejected. It also rejects +an own helper MOVE of rank eight, a helper without a paid path, a missing +paid rank-one job, an unearned helper credit, and omission of the local gap +from the analytic tail. The appendix rejects a changed decoder row and a +zero-rank defect. + +These checks verify the stated source census, declared complete invoice, and +price implications. They do not verify a common-cover supplier, full native +payload, ordinary movement and precision budget, uniform compiler, or outer +multiplication theorem. diff --git a/research/bit-fixed-source-price-gates/README.md b/research/bit-fixed-source-price-gates/README.md new file mode 100644 index 0000000000..784e5c96e5 --- /dev/null +++ b/research/bit-fixed-source-price-gates/README.md @@ -0,0 +1,140 @@ +# Two complete fixed-source BIT price gates + +This package closes two price questions without another discovery search. +For the fixed PR589 word, adding fresh commuting axes to any nonempty helper +set loses for every positive axis count and every tariff r^(1-C), 0(8+k)^(1-C)-8^(1-C). Distinct helper paths use distinct paid events.", + "reverse": { + "helpers": 439, + "maximum_own_paid_rank": 7, + "own_paid_move_events": 2159, + "owner_maximum_rank_counts": { + "2": 322, + "3": 64, + "4": 41, + "5": 10, + "6": 1, + "7": 1 + }, + "target_rank": 8 + }, + "scope": "Any nonempty helper subset, positive integer number of new commuting axes, and real 0(8+k)^(1-C)-8^(1-C). Distinct helper paths use distinct paid events.', + 'mincut_run':False, 'negative_controls':controls} + + +def profile(p,v,h,local,helpers): + d = h-1 + paid = Counter({r:(p+2)*count for r,count in local.items()}) + paid[1] += (p-1)*v + targets = Counter({h:(p+2)*helpers}) + targets[1+d*(p+2)] += 2*v + left = (p-1)//2 + for arm in (left,p-1-left): + for j in range(1,arm+1): + targets[1+d*(j+1)] += 2*v + paid[d*(j+1)] += 2*v + return paid,targets + + +def mass(values): + return sum(r*count for r,count in values.items()) + + +def rounded(interval): + lo,hi = interval + scale = 10**12 + a,b = lo*scale,hi*scale + lower = F(a.numerator//a.denominator,scale) + upper = F(-(-b.numerator//b.denominator),scale) + need(lower<=lo<=hi<=upper, 'The displayed rational enclosure fails') + return [str(lower),str(upper)] + + +def cube_gate(data): + module = load('retained_paired_cube',ROOT/(CUBE+'paired_cube_bit_word.py'),data[CUBE+'paired_cube_bit_word.py']) + exact = load('retained_exact_series',ROOT/ENGINE,data[ENGINE]) + source_manifest = json.loads(data[CUBE+'SOURCE.json']) + for name,digest in source_manifest['data'].items(): + need(sha256(data[CUBE+'data/'+name]).hexdigest()==digest, 'The retained cube data pin differs') + plan = json.loads(data[CUBE+'data/pair_module_p12.json']) + graph = module.BitGraph(12).finish(plan,module.pinned_all_but_one('qmod_p12.json',10),merge=True,l1=True) + need(module.check_decoder(graph)==0, 'The retained scalar decoder fails') + local,witness = module.compile_word(graph,frozen=json.loads(data[CUBE+'data/arcs_p12.json'])) + h,v,helpers = local['h'],local['v'],local['R'] + need((h,v,helpers,local['loss'])==(24,1760,19788,528), 'The retained cube dimensions differ') + source = Counter({1:v,h-4:v//2,2:v//2,h-2:v//2}) + paid = Counter(witness['H'])+source+Counter(witness['targetH']) + paid.pop(0,None) + targets = {h:helpers} + def invoice_check(paid_,targets_): + need(mass(source)==mass(witness['targetH'])==v*(h-1), 'A main boundary is unpaid') + need(mass(paid_)-mass(targets_)==2*v*(h-1)+528, 'The full local invoice loses a charge or debit') + need(max(paid_)0>bracket[1][1], 'The retained positive crossing control fails') + bad_paid = paid.copy();bad_paid[1]-=1 + controls = [reject('missing_paid_rank_one',lambda:invoice_check(bad_paid,targets)), + reject('unearned_helper_credit',lambda:invoice_check(paid,{h:helpers+1})), + reject('missing_local_gap_in_tail',lambda:tail(F(0)))] + return {'status':'PASS_PAIRED_TRIPLE_P12_ALL_PARAMETER_PRICE_GATE', + 'geometry_parameter':12,'h':h,'ports':v,'helpers':helpers,'centre_debt':528, + 'local_paid':dict(sorted(paid.items())),'local_helper_targets':targets, + 'source_main':dict(source),'target_main':dict(witness['targetH']), + 'finite_prefix':rows,'all_positive_integer_controller_parameters_raw_saving_below':'1/500', + 'tail':{'first_parameter':64,'upper_margin':rounded((tail_value,tail_value))[1], + 'upper_derivative':rounded((tail_slope,tail_slope))[1]}, + 'normalized_margin_decreases_with_C':{'local_paid_ranks_below_h':max(paid)>index & 1: + result ^= row + return result + + +def permutation_certificate(geometry): + j = geometry['J_rows'] + u,v = geometry['U_rows'],geometry['V_rows'] + need(len(j)==len(u)==111 and len(v)==9, 'The defect source shape differs') + defect = [row^(1<>bit)&1)<moved_bound, 'The deleted-row argument has no distance gap') + return {'defect_rank':9,'nonzero_codewords':511,'minimum_code_weight':48, + 'weight_counts':dict(sorted(weights.items())), + 'hypothetical_rank_bound':8,'permutation_difference_rank_bound':17, + 'moved_rows_bound':moved_bound,'minimum_rank_J_plus_permutation':9, + 'attaining_permutation':'identity','native_factorization_cost_bound':False} + + +def permutation_gate(data): + geometry=json.loads(gzip.decompress(data[DEFECT]))['geometry'] + result=permutation_certificate(geometry) + bad=dict(geometry);bad['J_rows']=list(geometry['J_rows']);bad['J_rows'][0]^=1 + zero=dict(geometry);zero['J_rows']=[1<