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/paired-residue-sampler/README.md b/research/paired-residue-sampler/README.md new file mode 100644 index 0000000000..615c4890ec --- /dev/null +++ b/research/paired-residue-sampler/README.md @@ -0,0 +1,188 @@ +# Joint denominator-13 decisions use fewer expected fair bits + +For every fixed pair of nonzero residue probabilities $a/13,b/13$, an explicit +finite-state sampler produces **two independent** Bernoulli decisions with +optimal expected fair-bit count strictly below $7/2$. Two separate exact +standalone samplers require expected count at least four. When both probabilities +are $1/13$, the joint expected count is below $9/4$, saving more than 43.75% of +the standalone expected draws. + +Each parameter pair has exactly 312 internal control states and 624 binary +transitions. Including its four output labels, every target fits nine bits; +a packed transition table uses 5,616 bits, or 702 bytes, per parameter pair. +The implementation generates one table at a time rather than storing all 144. + +This is a finite exact sampling construction and an expected-bit optimum, +not a physical inverse, worst-case latency bound, reversible cleanup protocol, +supplier or new κ. It deliberately changes the **standalone-call** hypothesis +of [PR #6068](https://github.com/CrocSwap/integer-mult-bounds/pull/6068). +The underlying dyadic decision-graph method is classical; the contribution is +this small complete denominator-13 catalogue, exact means and resource ledger. + +## Contract and source relevance + +The denominator-13 inverse in +[PR #5069](https://github.com/CrocSwap/integer-mult-bounds/pull/5069) motivates +rounding probabilities with this denominator. Both probabilities must be known +**before** this sampler consumes any bits. Their intended decisions are +independent. A second probability that depends on the first rounded result +cannot be substituted into this batch without a new contract. + +No actual native caller is asserted to provide the required residue pair or +batching window. The retained deterministic inverse is not alleged defective. +The stochastic prefix of +[Nick Petalas](https://github.com/petalas)'s +[PR #6026](https://github.com/CrocSwap/integer-mult-bounds/pull/6026) supplies a +related arithmetic context, but its adaptive updates are not automatically +batchable, and its native/caller error analysis is not extended here. + +## Exact joint decision graph + +In output order 00, 01, 10, 11, set the integer weights + +$$ +(w_0,w_1,w_2,w_3) +=((13-a)(13-b),(13-a)b,a(13-b),ab). +$$ + +Their sum is 169. Dividing by 169 gives exactly the product law, hence the +required independent marginals. Write the binary digits of each probability +as $d_{i,k}$ at depth $k\geq1$. Define + +$$ +n_k=2^k-\sum_{i=0}^3\lfloor2^k w_i/169\rfloor. +$$ + +This is the number of unfinished binary prefixes after depth $k$. At the root, +$n_0=1$. At the next depth, double every unfinished node, label the first +$d_{i,k}$ available children with output $i$, and retain the rest as unfinished. +Each digit is zero or one, and + +$$ +n_k=2n_{k-1}-\sum_i d_{i,k}. +$$ + +Thus this rule never overfills a level. An executable version stores the +unfinished-node index $j$: after drawing one bit $u$, set $j\leftarrow2j+u$, +then subtract the four probability digits in output order. The first subtraction +making $j$ negative returns that output; otherwise the remaining $j$ is the +next unfinished-node index. All four digits come from exact residue doubling +modulo 169. + +By induction, the completed output-$i$ prefixes at depth $k$ number exactly +$\lfloor2^k w_i/169\rfloor$. Since $1\leq n_k\leq3$, unfinished probability +is at most $3/2^k$, tending to zero. The resulting output law is therefore +exactly $w_i/169$, not an approximation from finite samples. + +## Finite periodic controller and exact expected cost + +The order of two modulo 169 is 156; replay checks this with exact integer +powers. Every weight is coprime to 13, so its residue sequence is periodic +with that period. The digits and unfinished-node counts repeat. There are +exactly 312 internal phase/node pairs for every one of the 144 residue pairs; +this finite count is checked exhaustively. Two transitions per state give the +624-entry table. No growing arithmetic precision is needed to represent the +sampler's logical control state, although its random tape and stopping length +have no finite worst-case bound. + +The exact expected draw count is + +$$ +E[T]=\frac{\sum_{k=0}^{155} n_k2^{-k}}{1-2^{-156}}. +$$ + +For $(a,b)=(1,1)$ this is + +$$ +E[T]=\frac{9960277917013927549978}{4649714690825496825793}<\frac94. +$$ + +The exact finite catalogue certifies $2=312:done[target-312]+=n + else:nxt[target]=nxt.get(target,0)+n + active=nxt + need(done==[w*(1<=312:return target-312,used + state=target + return None,len(bits) + + +def rejected(fn): + try:fn() + except ValueError:return + raise ValueError('negative control accepted') + + +def main(): + pins=json.loads((HERE/'SOURCES.json').read_text()) + for row in pins['files']: + if row['usage']=='input': + need(hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'],'source bytes') + need(pow(2,PERIOD,DEN)==1 and all(pow(2,k,DEN)!=1 for k in range(1,PERIOD)),'exact binary period') + maximum=Q(0);minimum=Q(4);cases=literal=0 + for a,b in product(range(1,13),repeat=2): + weights,counts,table,mean=make(a,b) + census(table,weights,2*PERIOD) + need(2=4,'false additivity of standalone lower bounds')) + rejected(lambda:need(mean<=2,'understated joint mean')) + rejected(lambda:need(census(table,weights,PERIOD)[1]==0,'false finite draw cap')) + need(Q(1,13)!=Q(1,169),'reused single flag violates independent joint law') + print(json.dumps(dict(status='PASS_PAIRED_RESIDUE_SAMPLER',residue_pairs=cases, + internal_states=312,transitions_per_pair=624,depths_checked_per_pair=312, + literal_tapes=literal,mean_one_one=str(mean),maximum_mean=str(maximum), + minimum_mean=str(minimum), + scope='optimal expected fair-bit count for a fixed nonadaptive pair; physical costs open; no new kappa'),sort_keys=True)) + + +if __name__=='__main__':main()