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/reversible-stochastic-shears/README.md b/research/reversible-stochastic-shears/README.md new file mode 100644 index 0000000000..829b3ebf4b --- /dev/null +++ b/research/reversible-stochastic-shears/README.md @@ -0,0 +1,203 @@ +# Stochastic scalar prefixes can restore dirty inputs with a parity log + +A grid-valued stochastic ADD is an exactly invertible shear when its inverse +uses the complemented coin. A rounded signed halving instead needs one parity +bit; keeping that bit suffices, and recomputing it during reversal clears it. +Together these give a compute–accumulate–uncompute interface for the exact +9,589-event scalar prefix studied by +[Nick Petalas](https://github.com/petalas)'s +[PR #6026](https://github.com/CrocSwap/integer-mult-bounds/pull/6026). + +The source has 84 signed halvings. The protocol uses **84 clean residue bits +and 11,713 read-only random bits per real stream sample**, restores all 748 +arbitrary dirty working values, returns the residue log to zero, and leaves +the random tape unchanged. Its forward arithmetic law is exactly the source's +fresh stochastic rounding law. Thus its source-relative forward error bound +is retained under the source's assumptions; that concentration result is cited, +not independently replayed or strengthened here. + +This is a logical scalar-grid ABI, not a native rounded supplier, physically +reversible bit-level implementation, complete caller invoice or new κ. Physical +random-bit preparation/access, guard widths, integer arithmetic, temporary +cleanup and the later native MOVE remain payable and unimplemented. + +## Exact stochastic rounding and an inverse shear + +Normalize the grid spacing to one. For an integer numerator $n$, dyadic +denominator $d=2^q$, and a fixed coin integer $0\leq U0 and d&(d-1)==0 and 0<=u1 for _,_,_,_,d in events) + need(ops=={'ADD':9358,'SCALE':231} and bits==11713 and h==84 and rounded==7421,'source ledger') + rng=Random(6026) + fixtures=[[0]*748,[((i*73)%251)-125 for i in range(748)], + [(-1 if i%2 else 1)*((1<<30)+104729*i) for i in range(748)], + [rng.randrange(-10**6,10**6) for _ in range(748)]] + full=peak=0 + for initial in fixtures: + target=[i*17-12345 for i in range(748)] + for mode in range(4): + tape=tuple(0 if mode==0 else d-1 if mode==1 else i%d if mode==2 + else hashlib.sha256(str(i).encode()).digest()[0]%d + for i,(_,_,_,_,d) in enumerate(events)) + _,size=protocol(initial,target,events,tape);peak=max(peak,size);full+=1 + # Same uncomplemented coin is an actual failing inverse, not a guarantee. + y=sr(1,2,0);bad=y+sr(-1,2,0) + need(bad!=0,'uncomplemented-coin counterexample') + reused=sum(sr(sr(1,2,u),2,u) for u in (0,1)) + fresh=sum(sr(sr(1,2,u),2,v) for u,v in product((0,1),repeat=2)) + need(Q(reused,2)==Q(1,2) and Q(fresh,4)==Q(1,4), + 'restored tape is not fresh for an adaptive second shear') + need(sr(0,2,1)==sr(1,2,1),'one side bit necessary for local halving') + rejected(lambda:need(2*sr(1,2,0)==1,'discarded half residue')) + es=[('SCALE',0,None,1,2)];y,log=forward([1],es,(0,));log[0]=0 + rejected(lambda:need(backward(y,es,(0,),log)[0]==[1],'corrupt residue')) + rejected(lambda:sr(1,3,0)) + rejected(lambda:sr(1,2,2)) + rejected(lambda:forward([1],[],(0,))) + print(json.dumps(dict(status='PASS_REVERSIBLE_STOCHASTIC_PREFIX',local_coin_identities=identities, + signed_halves=halves,tiny_protocols=tiny_cases,full_prefix_protocols=full, + events=9589,random_bits=bits,clean_residue_bits=h, + forward_reverse_and_copy_macros=2*len(events)+748, + peak_fixture_value_bits=peak, + scope='logical scalar-grid ABI; physical sampler/native costs open; no new kappa'),sort_keys=True)) + + +if __name__=='__main__':main()