diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 006bf5a3d5..63ba3e9aa8 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,6 +1,23 @@ # CI verification -## Current selected-family replay: #5599 +## Current selected-family replay: #6030 + +The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md), +[validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json), +and [explicit source closure](../certificates/frontier6030-source.json). +`make frontier6030-verify` follows that source-bound selected replay. The review +separates retained normal primary macOS/Linux evidence from fresh independent +word/invoice/native, original caller, adapted caller and optimized primary checks. +Consult its receipts for exact commands, source heads and limits; the #5599 +checkpoint below retains its own historical replay details. + +The five inherited framework assumptions remain. Neither the full uniform word +nor a complete rounded multiplier is materialized. A source/metadata check is +not an operator replay or a formal theorem proof. Routine research submissions +do not need to rerun this selected-family replay. + +## Historical selected-family replay: #5599 The [selected record](../certificates/selected-result.json) binds conditional κ = 0.00310045 to the [proof review](research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md) diff --git a/docs/research/current-status.md b/docs/research/current-status.md index a84ac12213..c49a245adc 100644 --- a/docs/research/current-status.md +++ b/docs/research/current-status.md @@ -1,6 +1,6 @@ # Current reviewed status -Selected conditional κ: **0.003125804 = 781451/250000000**, DreamingOfClouds' +Selected conditional κ: **0.003125804** = 781451/250000000, DreamingOfClouds' PR6030 on the cumulative P104 construction. The complete caller counts 13,444 productive fields and 66,834 paid calls. The saving is about 0.81775% above the preceding selected PR5599 claim 0.00310045. diff --git a/research/power-layer-collapse/README.md b/research/power-layer-collapse/README.md new file mode 100644 index 0000000000..eb13448bc1 --- /dev/null +++ b/research/power-layer-collapse/README.md @@ -0,0 +1,126 @@ +# Power tariffs collapse the fixed-spread antichain to one optimum + +For every integer m >= 1 and 0 <= k <= m, the complete k-spread layer of +[Nick Petalas's PR #5901](https://github.com/CrocSwap/integer-mult-bounds/pull/5901) +`concave-invoice-antichains` family has **one unique cheapest invoice for every +power tariff r^p with 0 < p < 1**: spread precisely blocks 1,...,k. +The result answers that package's second open question. Its 252-member m=10 +layer and 462-member m=11 layer each reduce to one representative under this +narrower tariff family, although every pair remains incomparable under the +larger increasing-concave family. + +This is a scoped proof and exact finite corroboration, not a legal supplier, +a new kappa, a claim about arbitrary invoices, or a refutation of the predecessor. +The predecessor's all-concave theorem remains valid. + +## Contract and proof + +Write H_r for one rank-r paid call. For S subset {1,...,m}, retain the full bill + +``` +P_S = sum_(i not in S) 2 H_(2i) + sum_(i in S) (H_(2i-1)+H_(2i+1)), +I_S = P_S - H_M, M = 2m(m+1). +``` + +All candidates have 2m paid calls, mass M, and the same productive target. +No other fee, boundary, or consumer may differ in this comparison. The theorem +is about the synthetic family defined above; it grants no realization of it. + +Fix p in (0,1). The cost difference made by spreading block i is + +``` +delta_i(p) = (2i-1)^p + (2i+1)^p - 2(2i)^p. +``` + +For x>1, integrating the second derivative twice gives + +``` +delta(x) = p(p-1) integral_[-1,1] (1-|t|) (x+t)^(p-2) dt. +``` + +The identity follows by applying the fundamental theorem of calculus on each +side of x, or by integration by parts on [-1,0] and [0,1]. The kernel is +nonnegative and positive in the interior. Since p-2<0, its power factor strictly +decreases as x increases. Since p(p-1)<0, **delta(x) strictly increases**. +Thus delta_1(p) < ... < delta_m(p) < 0, simultaneously for every p in (0,1). + +Let S0={1,...,k}. If a k-subset S differs from S0, it contains j>k and omits +i<=k. Exchanging j for i decreases its complete bill by +`delta_j(p)-delta_i(p)>0`. Repeating terminates at S0. The target and all +unchanged paid blocks cancel at each exchange. This proves strict simultaneous +dominance and uniqueness for 01 +with a common symmetric spread h satisfying 0 0 and p > 0, "power domain") + a, b = p.numerator, p.denominator + d = 1 << 64 + n = (r ** a) * (d ** b) + lo, hi = 0, (r ** max(1, a)) * d + 1 + while lo + 1 < hi: + mid = (lo + hi) // 2 + if mid ** b <= n: + lo = mid + else: + hi = mid + require(lo ** b <= n < (lo + 1) ** b, "root bracket") + return F(lo, d), F(lo if lo ** b == n else lo + 1, d) + + +def invoice(m, selected): + require(1 <= m <= 11, "m domain") + selected = frozenset(selected) + require(selected <= set(range(1, m + 1)), "subset domain") + hist = {} + for i in range(1, m + 1): + for r in ((2*i-1, 2*i+1) if i in selected else (2*i, 2*i)): + hist[r] = hist.get(r, 0) + 1 + require(sum(hist.values()) == 2*m, "paid count") + require(sum(r*n for r,n in hist.items()) == 2*m*(m+1), "paid mass") + hist[2*m*(m+1)] = -1 + return hist + + +def bounds(hist, p): + lo = hi = F(0) + for r, n in hist.items(): + a,b = power_interval(r,p) + lo += n*(a if n>0 else b) + hi += n*(b if n>0 else a) + return lo,hi + + +def difference(left,right): + return {r:left.get(r,0)-right.get(r,0) for r in left.keys()|right.keys()} + + +def reject(thunk): + try: + thunk() + except ValueError: + return + raise ValueError("negative control accepted") + + +def strict_less(left,right,p): + require(bounds(difference(left,right),p)[1] < 0, "strict dominance") + + +def main(): + source = HERE.parents[1] / 'research/concave-invoice-antichains/README.md' + pins = json.loads((HERE/'SOURCES.json').read_text()) + pin = next(x for x in pins['files'] if x['path'].endswith('concave-invoice-antichains/README.md')) + require(hashlib.sha256(source.read_bytes()).hexdigest()==pin['sha256'], 'source bytes') + ps = sorted({F(a,b) for b in range(2,9) for a in range(1,b)}) + compared = 0 + for m in range(1,12): + for k in range(m+1): + best = invoice(m,range(1,k+1)) + for s in combinations(range(1,m+1),k): + bill = invoice(m,s) + if s != tuple(range(1,k+1)): + for p in ps: + strict_less(best,bill,p) + compared += 1 + for p in (0,1): + require(sum(n*(r**p) for r,n in best.items()) == + sum(n*(r**p) for r,n in bill.items()), 'endpoint tie') + for p in ps: + for i in range(1,m): + left={2*i-1:1,2*i+1:1,2*i:-2} + j=i+1 + right={2*j-1:1,2*j+1:1,2*j:-2} + strict_less(left,right,p) + first,second=invoice(2,{1}),invoice(2,{2}) + diff=difference(first,second) + require(sum(n*min(r,2) for r,n in diff.items())==-1,'hinge 2') + require(sum(n*min(r,4) for r,n in diff.items())==1,'hinge 4') + strict_less(second,first,F(3,2)) + reject(lambda: strict_less(first,second,F(3,2))) + changed_target=dict(first) + changed_target[12]=0 + reject(lambda: strict_less(changed_target,second,F(1,2))) + extra_fee=dict(first) + extra_fee[1]=extra_fee.get(1,0)+1 + reject(lambda: strict_less(extra_fee,second,F(1,2))) + reject(lambda: invoice(0,())) + reject(lambda: invoice(2,{3})) + reject(lambda: strict_less(second,first,F(1,2))) + require(len(list(combinations(range(1,11),5)))==252,'m10 layer') + require(len(list(combinations(range(1,12),5)))==462,'m11 layer') + print(json.dumps({'status':'PASS_POWER_LAYER_COLLAPSE','rational_powers':len(ps), + 'strict_comparisons':compared,'m10_survivors':1,'m11_survivors':1, + 'scope':'written all-p proof with finite exact corroboration; no new kappa'},sort_keys=True)) + + +if __name__=='__main__': + main()