== RQ-B MAIN_RESULT.tex e4193842
PASS  C_3 = g((3-1) s_3) = g(3 s_3) and s_3 = s(q_3)  
PASS  C_4 = g((4-1) s_4) = g(4 s_4) and s_4 = s(q_4)  
PASS  C_5 = g((5-1) s_5) = g(5 s_5) and s_5 = s(q_5)  
PASS  C_6 = g((6-1) s_6) = g(6 s_6) and s_6 = s(q_6)  
PASS  text line 149: located "$r_1=2(3/2)^{3/2}e^{-3/2}=0.819833$"  
PASS  r_1 = 0.819833 (round)  0.819832557884
PASS  text line 185: located "$\gamma_4=0.8235571>r_1=0.8198326$ (margin"  
PASS  text line 186: located "$0.0037$; $\gamma_5=0.83179$, $\gamma_6=0.83684$)"  
PASS  gamma_4 = 0.8235571 (trunc; a lower bound, A.27 remark)  0.823557158515
PASS  r_1 = 0.8198326 (round)  
PASS  gamma_4 > r_1, margin 0.0037 (round)  0.0037246
PASS  gamma_5 = 0.83179, gamma_6 = 0.83684 (round)  0.8317944 0.8368419
PASS  text line 191: located "(there $\sqrt{1-q}\,M(q)=0.8077<r_1$)"  
PASS  C(q3) = g(2 s3) = g(3 s3) is the max over k <= 80 (k > 80: k s3 > 16, g < 1e-5)  
PASS  sqrt(1-q3) M(q3) = sqrt(q3/s3) C(q3) = 0.8077 (round) < r_1  0.80774786
PASS  text line 263: located "$r_1=2(3/2)^{3/2}e^{-3/2}=0.819833<0.82$"  
PASS  text line 264: located "exceeds $0.82$ at $\lambda=0.32$ ($0.82154$) and $\lambda=0.74$ ($0.82086$)"  
PASS  r_1 < 0.82 < g(0.32), g(0.74); g(0.32) = 0.82154, g(0.74) = 0.82086 (round)  0.8215438532 0.8208578181
PASS  text line 268: located "(an interval of length $0.42$)"  
PASS  0.74 - 0.32 = 0.42 exactly  
PASS  text line 270: located "$q\le1-e^{-0.42}=0.34295$"  
PASS  text line 271: located "for every $q\le0.3429$"  
PASS  1 - e^-0.42 = 0.34295 (round) and 0.3429 <= it  0.3429531802
PASS  text line 303: located "$C_4=0.85334356\ldots$, $C_5=0.85510045\ldots$, $C_6=0.85598448\ldots$"  
PASS  text line 304: located "$\sqrt{2/e}-C_K=0.0044203$, $0.0026634$, $0.0017794$"  
PASS  text line 305: located "(e.g.\ $0.8533435$, $0.855100$, $0.855984$)"  
PASS  C_4 = 0.85334356... (trunc), sqrt(2/e) - C_4 = 0.0044203 (round), example 0.8533435 <= C_4  0.85334356849605
PASS  C_5 = 0.85510045... (trunc), sqrt(2/e) - C_5 = 0.0026634 (round), example 0.855100 <= C_5  0.85510045547082
PASS  C_6 = 0.85598448... (trunc), sqrt(2/e) - C_6 = 0.0017794 (round), example 0.855984 <= C_6  0.85598448917382
PASS  text line 350: located "[3s(q_4),4s(q_4)]=[0.4315,0.5754]$"  
PASS  text line 351: located "[1/\sqrt{4s(q_4)},1/\sqrt{3s(q_4)}]=[1.3183436,1.5222920]$"  
PASS  text line 352: located "$\theta\le a_4=1/\sqrt{4s(q_4)}=1.3183436$"  
PASS  3 s(q4) = 0.4315, 4 s(q4) = 0.5754 (round)  0.431523109 0.575364145
PASS  a_4 = 1.3183436, b_4 = 1.5222920 (round)  1.3183435624 1.5222920212
PASS  text line 895: located "target $\frac{171}{200}<C_5=0.85510045547$"  
PASS  171/200 < C_5 = 0.85510045547 (trunc and round)  
== RQ-B Section 13 table, re-counted from the certificate files
PASS  text table: located "1 (near splits) & 7956 & 8481 (5) & 2 & 14 & 0.85499698"  
PASS  nsplit_D14: own copy 0883b5d9 is byte-identical to the store copy  
PASS  nsplit_D14: 8481 certificates (5 without phi), max depth 2, D = [14], roots 7956 (A.39 coverage)  depths {0: 7922, 1: 539, 2: 20}
PASS  nsplit_D14: largest bound (A.39) 0.854996980551545 at N/k35/i0j6 rounds to 0.85499698  
PASS  text table: located "2 (chord boxes) & 60 & 1212 (166) & 5 & 14 & 0.85495525"  
PASS  chord_D14: own copy 3d7366f9 is byte-identical to the store copy  
PASS  chord_D14: 1212 certificates (166 without phi), max depth 5, D = [14], roots 60 (A.39 coverage)  depths {0: 26, 1: 385, 2: 588, 3: 187, 4: 18, 5: 8}
PASS  chord_D14: largest bound (A.39) 0.8549552502410571 at C/i1j3/q32 rounds to 0.85495525  
PASS  text table: located "3 (light set) & 537 & 1273 (60) & 4 & 18 & 0.85497432"  
PASS  light_vl025_D18: own copy 2bbb7484 is byte-identical to the store copy  
PASS  light_vl025_D18: 1273 certificates (60 without phi), max depth 4, D = [18], roots 537 (A.39 coverage)  depths {0: 468, 1: 207, 2: 195, 3: 207, 4: 196}
PASS  light_vl025_D18: largest bound (A.39) 0.8549743150463496 at L/s15t15 rounds to 0.85497432  
PASS  text line 1048: located "$\frac{171}{200}-U=3.02\cdot10^{-6}$"  
PASS  text line 1048: located "In case 1, $7922$ boxes are certified at depth $0$ and the other $34$ by $539$"  
PASS  text line 1049: located "rest cells at depth $1$ and $20$ at depth $2$"  
PASS  case 1: 171/200 - U = 3.02e-6 (3 digits)  3.019448e-06
PASS  case 1: 7922 leaves at depth 0, 539 at depth 1, 20 at depth 2; 7956 - 7922 = 34 roots split, 34 x 16 = 539 + 5 and the 5 depth-1 cells split into 5 x 4 = 20  roots split 34, depth-1 parents 5
== RQ-C CLAIMS.md 4b1e22a4, C15(g)
PASS  C15 below its header line is byte-identical to the 15:53 text audited in A.28  a2709071
PASS  text C15(g): located "A'(0.05) = 1.46976, A'(q_6) = 1.51455, A'(0.1) = 1.53085, A'(q_5) = 1.53804, A'(q_4) = 1.5"  
PASS  A'(0.05), A'(q6), A'(0.1), A'(q5), A'(q4) (round, 5 places); the points increase  1.46975890 1.51454838 1.53085319 1.53804439 1.57599267
PASS  text C15(g): located "e.g. a = 1.49690 for k = 4 against A'(q_5) = 1.53804"  
PASS  a(4) = 1/sqrt(4 s(q5)) = sqrt(2/(4 ln(5/4))) = 1.49690 (round) < A'(q5)  1.496900150
PASS  a(k) = sqrt2 (1 + 1/(4k) + O(k^-2)): k^2 (a/sqrt2 - 1 - 1/(4k)) -> -7/96  -0.072878 -0.072913 -0.072916
PASS  text C15(g): located "A = 99/70 = 1.41429"  
PASS  99/70 = 1.41429 (round); sqrt2 < 99/70 < a(4)  99/70 - sqrt2 = 7.215e-05
PASS  text C15(g): located "A ≥ 1.538 for q ≤ q_5, A ≥ 1.576 for q ≤ q_4"  
PASS  1.538 and 1.576 are A'(q5) and A'(q4) to 3 places (1.538 < A'(q5); 1.576 rounds A'(q4) up)  
PASS  the chain's A = 77/50 exceeds A'(q5)  
== RQ-A CLAIMS.md ac1b39c0, U.1-U.3
PASS  U.1-U.3 are byte-identical to the 16:47 text (CLAIMS 3a8a0c64, the text of a26d)  71c5186b
PASS  K=4: C(q_K) = 0.8533435684... and eta_K = 0.0044203164... (trunc); margin 0.00443 >= eta_K  
PASS  K=5: C(q_K) = 0.8551004554... and eta_K = 0.0026634294... (trunc); margin 0.00267 >= eta_K  
PASS  K=6: C(q_K) = 0.8559844891... and eta_K = 0.0017793957... (trunc); margin 0.00178 >= eta_K  
PASS  text U.3: located "decimal C <= 0.8533435"  
PASS  text U.3: located "0.853344, which is C(q_4) rounded up and leaves q in (0.13397376, q_4) uncovered"  
PASS  text U.3: located "(e.g. C = 0.855100)"  
PASS  text U.3: located "(e.g. C = 0.855984)"  
PASS  0.8533435 <= C(q4) < 0.853344; 0.855100 <= C(q5); 0.855984 <= C(q6)  
PASS  bracket: g(4/8) > 0.853344 > g(4 s4)  
PASS  root s* of g(4s) = 0.853344 enclosed  
PASS  q* = 1 - e^(-s*) = 0.13397376 (trunc), q4 - q* = 8.36e-7  q* = 0.133973760383006, q4 - q* = 8.3583e-07
PASS  tie g(3 s4) = g(4 s4); at s*: g(3s), g(5s) < g(4s) (with the monotonicity in the docstring, C = g(4s) on the gap)  
PASS  text U.2: located "eta_K ~ sqrt(2/e)/(16 K^2) as K -> oo"  
PASS  eta_K 16 K^2 / sqrt(2/e) -> 1 (K = 1e3, 1e4, 1e5)  1.0010009 1.0001000 1.0000100
A40F_PASS
