From 9465f263a673d2d86e7262523cbeb0e796f486cf Mon Sep 17 00:00:00 2001 From: Figo Lam Date: Wed, 28 Oct 2026 11:27:32 +0000 Subject: [PATCH 1/7] Prove fixed direct-flow leaf deficit saturation --- research/direct-flow-leaf-saturation/PROOF.md | 105 +++++++++ .../direct-flow-leaf-saturation/README.md | 50 ++++ .../direct-flow-leaf-saturation/RESULT.json | 48 ++++ .../direct-flow-leaf-saturation/REVIEW.md | 43 ++++ .../direct-flow-leaf-saturation/SOURCES.json | 48 ++++ .../direct-flow-leaf-saturation/TASK.json | 105 +++++++++ .../direct-flow-leaf-saturation/VALIDATION.md | 38 +++ .../direct-flow-leaf-saturation/VERIFY.json | 44 ++++ .../independent_source.py | 32 +++ .../logs/independent-optimized.log | 65 +++++ .../logs/independent.log | 65 +++++ .../logs/metadata-final.log | 1 + .../logs/metadata.log | 1 + .../logs/mutations-optimized.log | 1 + .../logs/mutations.log | 1 + .../logs/optimized.log | 48 ++++ .../logs/primary.log | 48 ++++ .../logs/registered.log | 118 +++++++++ .../logs/validation.json | 117 +++++++++ .../test_controls.py | 59 +++++ .../direct-flow-leaf-saturation/verify.py | 223 ++++++++++++++++++ 21 files changed, 1260 insertions(+) create mode 100644 research/direct-flow-leaf-saturation/PROOF.md create mode 100644 research/direct-flow-leaf-saturation/README.md create mode 100644 research/direct-flow-leaf-saturation/RESULT.json create mode 100644 research/direct-flow-leaf-saturation/REVIEW.md create mode 100644 research/direct-flow-leaf-saturation/SOURCES.json create mode 100644 research/direct-flow-leaf-saturation/TASK.json create mode 100644 research/direct-flow-leaf-saturation/VALIDATION.md create mode 100644 research/direct-flow-leaf-saturation/VERIFY.json create mode 100644 research/direct-flow-leaf-saturation/independent_source.py create mode 100644 research/direct-flow-leaf-saturation/logs/independent-optimized.log create mode 100644 research/direct-flow-leaf-saturation/logs/independent.log create mode 100644 research/direct-flow-leaf-saturation/logs/metadata-final.log create mode 100644 research/direct-flow-leaf-saturation/logs/metadata.log create mode 100644 research/direct-flow-leaf-saturation/logs/mutations-optimized.log create mode 100644 research/direct-flow-leaf-saturation/logs/mutations.log create mode 100644 research/direct-flow-leaf-saturation/logs/optimized.log create mode 100644 research/direct-flow-leaf-saturation/logs/primary.log create mode 100644 research/direct-flow-leaf-saturation/logs/registered.log create mode 100644 research/direct-flow-leaf-saturation/logs/validation.json create mode 100644 research/direct-flow-leaf-saturation/test_controls.py create mode 100644 research/direct-flow-leaf-saturation/verify.py diff --git a/research/direct-flow-leaf-saturation/PROOF.md b/research/direct-flow-leaf-saturation/PROOF.md new file mode 100644 index 0000000000..0d7d4c4a8b --- /dev/null +++ b/research/direct-flow-leaf-saturation/PROOF.md @@ -0,0 +1,105 @@ +# A nonlattice saturation theorem for the fixed #4467 leaf law + +This is a scoped mathematical proof using the classical nonlattice interval local-limit theorem stated below. The Python certificate verifies its source-specific numerical hypotheses and finite source-law controls; it is not a proof-kernel verification of this argument. No finite-depth error rate is claimed. + +## 1. Source law and statement + +Use the fixed raw-p7 inventories in Ryanson Jonathan / pinterbanget's #4467 (`research/direct-flow-leaf-walk/verify.py`): + +``` +P = {1:37305, 2:10695, 3:3360, 4:1530, 5:300, + 8:1464, 16:448, 32:448, 48:448} +W = {5:420, 6:270, 7:840, 8:1395, 9:3195, + 25:448, 41:448, 57:448, 121:224} +m = 121 +``` + +Let `Z(s) = Σ_r P_r r^s`, `μ(s) = Z'(s)/Z(s)`, and let `t` be the unique root of `Σ_k W_k k^t = Z(t)` in the certified interval `[0.99731351095114, 0.99731351095116]`. Put `a = log 5`. Let `α` be the unique solution of `μ(α)=a` and set `λ=t−α`. + +The certificate also bounds the invoice derivative strictly above 211661 on the predecessor’s entire bisection interval `[0.99,1]`, so the isolated root is its unique root there. The certificate proves `μ(t)>a`, `α∈[0.98981438244597, 0.98981438244599]`, and thus `λ∈[0.00749912850515, 0.00749912850519]`. All intervals here are outward bounds, not floating-point root guesses. Uniqueness of α follows from `μ'(s)=Var_s(log r)>0`, its limits 0 and log48 at the two infinities, and `00`. + +**Actual leaf consequence.** For every integer rank `N≥121`, set `G=floor(log_5(N/121))` and `δ=log(N/121)−G log5∈[0,a)`. The potential-weighted mean leaf log-depth in the pinned flow satisfies + +`D_leaf(N) → log121 − μ(t) + 1/λ ∈ [136.51870330,136.51870331]` + +as `N→∞`, including sequences approaching either end of a lockstep level. There is no restriction to the level starts `N=121·5^G`. + +## 2. Why this is the source's measure + +The pinned `diagnostics/overlap_flow.py` constructs `F[d][ρ]` by multiplying `d` paid ranks and retaining a new product precisely when `121·ρ≤N`. All paid ranks are positive integers, so their logarithms are nonnegative: the final product constraint implies every earlier constraint. Consequently `F[G][ρ]` is exactly the sum of `Π_i P_{r_i}` over ordered G-tuples with product ρ and `ρ≤N/121`. + +In its `d==G` branch, the flow issues *every* final rank `r` with multiplicity `F[G][ρ] P_r` at exit rank `rρ`. This final rank is **not conditioned** by `121·rρ≤N`. Weighting by `(rρ)^t` factorizes into the conditioned G-step law above and an independent terminal `R` with law `p_t`. + +Thus, exactly at every finite N, + +`E[log(N/(Rρ))] = log121 − μ(t) + E[Y_G | S_G≤B_G]`. + +This G-versus-G+1 distinction matters. The checker independently enumerates ordered words through G=3 and compares all leaf multiplicities with the whole-flow `X−BX`; an extra-terminal-truncation mutant fails. The source audit also checks the original #4436 flow. These are finite controls for the source derivation, not evidence for the asymptotic theorem. + +## 3. The classical input and its hypotheses + +We use the nonlattice interval local-limit theorem in the following standard form. If iid real `V_i` have mean zero, finite positive variance `σ²`, and a nonlattice law, then for each fixed `h>0`, + +`sup_x | sqrt(G) P(Σ V_i∈[x,x+h)) − h/(σ sqrt(2π)) exp(−x²/(2Gσ²)) | → 0`. + +Reference: C. Stone, “A local limit theorem for nonlattice multi-dimensional distribution functions,” *The Annals of Mathematical Statistics* 36(2) (1965), 546–551, [DOI 10.1214/aoms/1177700165](https://doi.org/10.1214/aoms/1177700165), one-dimensional specialization. This theorem is an external mathematical dependency; it is stated here rather than silently replacing a discrete distribution by a density. Its asymptotic form supplies no explicit error constant or onset G. + +Apply it to the tilted law `q(r)=P_r r^α/Z(α)`, with `V=log r−a`. Its mean is zero by definition, and its variance is positive and finite because the support is finite and contains distinct points of positive mass. The support is nonlattice: it contains `0,log2,log3` before centering. If all belonged to a translate of `hZ`, their differences would imply `log2/log3` rational. An integer relation `u log2=v log3` with nonzero integers would imply `2^u=3^v`, contradicting unique factorization. Centering and tilting do not alter this property. + +Two consequences are used: + +- For fixed finite intervals in y, `sqrt(G) Q(B_G−S_G∈I) → |I|/(σ sqrt(2π))`, uniformly over bounded δ. +- There is a constant C such that for all `G≥1` and all real x, `sqrt(G) Q(S_G∈[x,x+1))≤C`. + +The second follows from the theorem for h=1 for sufficiently large G, and enlarging C for finitely many smaller G. It is an existence bound, not a computable convergence rate. Either convention for half-open intervals works: the maximum atom is `o(G^(-1/2))`, by bounding it with an interval of arbitrary fixed h and then taking h down to zero. This also handles an atom at the exact truncation boundary. + +## 4. Weighted local limits and integrable tails + +Write `c=1/(σ sqrt(2π))`. For the nonnegative functions + +`f_0(y)=exp(−λy)`, `f_1(y)=y exp(−λy)`, and `f_x(y)=1_{y≥x} exp(−λy)`, + +we claim, uniformly in δ, + +`sqrt(G) E_q[f(B_G−S_G) 1_{S_G≤B_G}] → c ∫_0^∞ f(y)dy`. + +On a fixed compact interval this follows by upper and lower step-function approximations and the interval local limit. The functions are bounded and Riemann integrable there, including the single jump of `f_x`; the possible boundary atom is negligible by §3. + +For an integer `J≥0` and the tail partition into intervals `[j,j+1)`, the concentration bound in §3 gives, uniformly over G and δ, + +`sqrt(G) E_q[f_0(Y_G) 1_{Y_G≥J}] ≤ C Σ_{j≥J} exp(−λj)`, + +and + +`sqrt(G) E_q[f_1(Y_G) 1_{Y_G≥J}] ≤ C Σ_{j≥J} (j+1) exp(−λj)`. + +Here Y_G denotes the unconditioned difference `B_G−S_G` inside the indicated nonnegative event. Both series tend to zero as `J→∞` because λ>0; `f_x≤f_0` has the same domination. This proves the weighted local limits and supplies the missing uniform-integrability argument for the mean. Weak convergence alone would not suffice. + +## 5. Undoing the tilt + +For an ordered G-tuple, + +`p_t(tuple)/q(tuple) = (Z(α)/Z(t))^G exp(λ S_G)`. + +On writing `S_G=B_G−y`, the common factor `(Z(α)/Z(t))^G exp(λ B_G)` cancels in every conditional ratio. Hence + +`P_t(Y_G≥x | S_G≤B_G) = E_q[f_x(B_G−S_G) 1_{S_G≤B_G}] / E_q[f_0(B_G−S_G) 1_{S_G≤B_G}]`, + +and the analogous numerator with `f_1` gives the conditional expectation. By §4, the three scaled integrals converge to `c exp(−λx)/λ`, `c/λ²`, and `c/λ`. The denominator limit is strictly positive, so their ratios converge uniformly over δ to `exp(−λx)` and `1/λ`. Section 2 then gives the claimed leaf-depth limit. + +## 6. Scope, controls, and remaining decisions + +This proves the saturation that #4467 explicitly labelled heuristic. It does **not** prove its suggested total log-gap `g∞≈122`, stable source/boundary/leaf shares, any numerical refined-induction ceiling, or the quoted astronomical ranks required to achieve a saving. Those require separate control of other flow components and a finite-depth estimate. The raw-p7 inventory is historical and is not the selected #6030 invoice. + +Nonlattice support is essential for this limit law. For `X∈{0,log2}` with probabilities `(1/3,2/3)` and even G, conditioned at `B_G=G log2/2`, λ=1 but the limiting deficit is `log2` times a geometric variable with probabilities `2^(-j-1)`, j≥0. Its mean is `log2`, not 1. Indeed the successive binomial mass ratio below G/2 tends to 1/2 and is bounded by 1/2, which proves both the geometric limit and mean convergence by domination. The verifier includes this failure control. Zero or negative relative drift likewise lies outside the theorem's λ>0 hypothesis. + +Credit: the flow is zxv's #4436, the refined induction is Cinna Davis / 1337isnot1337's #4405, the lockstep construction is Jacob Alan Sussman's Theorem 1G, and the source law, saturation conjecture and diagnostics are Ryanson Jonathan / pinterbanget's #4467 (following #4465). This proof and certificate were prepared for DLamdata with substantial OpenAI Codex assistance. Apache-2.0. Internal AI checks are not independent human review or formal verification. diff --git a/research/direct-flow-leaf-saturation/README.md b/research/direct-flow-leaf-saturation/README.md new file mode 100644 index 0000000000..ec6a503ba6 --- /dev/null +++ b/research/direct-flow-leaf-saturation/README.md @@ -0,0 +1,50 @@ +# The fixed #4467 leaf deficit saturates, uniformly across lockstep levels + +This package proves the saturation predicted by Ryanson Jonathan / pinterbanget's [#4467](https://github.com/CrocSwap/integer-mult-bounds/pull/4467). For its fixed raw-p7 paid-rank law, the conditional deficit `B_G−S_G` converges to `Exp(λ)`, **including convergence of the mean**, uniformly for `B_G=G log5+δ`, `0≤δN:continue + multiplicity=math.prod(walk.P[r] for r in ranks) + for r,pr in walk.P.items():exact[r*rho]+=multiplicity*pr + leaf=collections.Counter(f['X']);leaf.subtract(f['BX']);leaf=+leaf + need(exact==leaf,(N,'leaf histogram')) + actual=native.Flow(walk.W,walk.P,N).merged() + other=actual['exits'].copy();other.subtract(actual['boundary_exits']);other=+other + need(other==exact,(N,'original Flow class')) + # Incorrectly truncating the last unconditioned rank must change the leaf law. + wrong=collections.Counter({r:c for r,c in exact.items() if 121*r<=N}) + need(wrong!=exact,(N,'terminal truncation failure control')) + rows.append({'N':N,'G':G,'leaf_ranks':len(exact),'terminal_truncation_rejected':True}) +print(json.dumps({'status':'PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION','fixtures':rows},indent=2)) diff --git a/research/direct-flow-leaf-saturation/logs/independent-optimized.log b/research/direct-flow-leaf-saturation/logs/independent-optimized.log new file mode 100644 index 0000000000..f50d39a3e3 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/independent-optimized.log @@ -0,0 +1,65 @@ +{ + "status": "PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION", + "fixtures": [ + { + "N": 121, + "G": 0, + "leaf_ranks": 9, + "terminal_truncation_rejected": true + }, + { + "N": 604, + "G": 0, + "leaf_ranks": 9, + "terminal_truncation_rejected": true + }, + { + "N": 605, + "G": 1, + "leaf_ranks": 26, + "terminal_truncation_rejected": true + }, + { + "N": 606, + "G": 1, + "leaf_ranks": 26, + "terminal_truncation_rejected": true + }, + { + "N": 3024, + "G": 1, + "leaf_ranks": 30, + "terminal_truncation_rejected": true + }, + { + "N": 3025, + "G": 2, + "leaf_ranks": 55, + "terminal_truncation_rejected": true + }, + { + "N": 3026, + "G": 2, + "leaf_ranks": 55, + "terminal_truncation_rejected": true + }, + { + "N": 15124, + "G": 2, + "leaf_ranks": 65, + "terminal_truncation_rejected": true + }, + { + "N": 15125, + "G": 3, + "leaf_ranks": 98, + "terminal_truncation_rejected": true + }, + { + "N": 15126, + "G": 3, + "leaf_ranks": 98, + "terminal_truncation_rejected": true + } + ] +} diff --git a/research/direct-flow-leaf-saturation/logs/independent.log b/research/direct-flow-leaf-saturation/logs/independent.log new file mode 100644 index 0000000000..f50d39a3e3 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/independent.log @@ -0,0 +1,65 @@ +{ + "status": "PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION", + "fixtures": [ + { + "N": 121, + "G": 0, + "leaf_ranks": 9, + "terminal_truncation_rejected": true + }, + { + "N": 604, + "G": 0, + "leaf_ranks": 9, + "terminal_truncation_rejected": true + }, + { + "N": 605, + "G": 1, + "leaf_ranks": 26, + "terminal_truncation_rejected": true + }, + { + "N": 606, + "G": 1, + "leaf_ranks": 26, + "terminal_truncation_rejected": true + }, + { + "N": 3024, + "G": 1, + "leaf_ranks": 30, + "terminal_truncation_rejected": true + }, + { + "N": 3025, + "G": 2, + "leaf_ranks": 55, + "terminal_truncation_rejected": true + }, + { + "N": 3026, + "G": 2, + "leaf_ranks": 55, + "terminal_truncation_rejected": true + }, + { + "N": 15124, + "G": 2, + "leaf_ranks": 65, + "terminal_truncation_rejected": true + }, + { + "N": 15125, + "G": 3, + "leaf_ranks": 98, + "terminal_truncation_rejected": true + }, + { + "N": 15126, + "G": 3, + "leaf_ranks": 98, + "terminal_truncation_rejected": true + } + ] +} diff --git a/research/direct-flow-leaf-saturation/logs/metadata-final.log b/research/direct-flow-leaf-saturation/logs/metadata-final.log new file mode 100644 index 0000000000..a6c9fb298a --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/metadata-final.log @@ -0,0 +1 @@ +PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check) diff --git a/research/direct-flow-leaf-saturation/logs/metadata.log b/research/direct-flow-leaf-saturation/logs/metadata.log new file mode 100644 index 0000000000..a6c9fb298a --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/metadata.log @@ -0,0 +1 @@ +PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check) diff --git a/research/direct-flow-leaf-saturation/logs/mutations-optimized.log b/research/direct-flow-leaf-saturation/logs/mutations-optimized.log new file mode 100644 index 0000000000..ba3e3e0348 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/mutations-optimized.log @@ -0,0 +1 @@ +PASS_MUTATION_CONTROLS source_bytes_normal_and_optimized corrupted_receipt paid_and_target_count_plus_one diff --git a/research/direct-flow-leaf-saturation/logs/mutations.log b/research/direct-flow-leaf-saturation/logs/mutations.log new file mode 100644 index 0000000000..ba3e3e0348 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/mutations.log @@ -0,0 +1 @@ +PASS_MUTATION_CONTROLS source_bytes_normal_and_optimized corrupted_receipt paid_and_target_count_plus_one diff --git a/research/direct-flow-leaf-saturation/logs/optimized.log b/research/direct-flow-leaf-saturation/logs/optimized.log new file mode 100644 index 0000000000..33db553260 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/optimized.log @@ -0,0 +1,48 @@ +{ + "controls": { + "interval_domain_rejections": 3, + "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1" + }, + "finite_law": { + "extra_terminal_truncation": "rejected", + "ordered_word_max_depth": 3, + "whole_flow_fixtures": 8 + }, + "parameters": { + "alpha": [ + "0.98981438244597", + "0.98981438244599" + ], + "drift_above_log5": [ + "0.016477707041", + "0.016477707042" + ], + "invoice_derivative_lower_bound_interval_0_99_to_1": [ + "211661.930309", + "211661.930310" + ], + "lambda": [ + "0.00749912850515", + "0.00749912850519" + ], + "mean_deficit_limit": [ + "133.34882837", + "133.34882838" + ], + "mean_leaf_depth_limit": [ + "136.51870330", + "136.51870331" + ], + "mean_log_rank": [ + "1.625915619475", + "1.625915619476" + ], + "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds", + "t_star": [ + "0.99731351095114", + "0.99731351095116" + ] + }, + "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.", + "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS" +} diff --git a/research/direct-flow-leaf-saturation/logs/primary.log b/research/direct-flow-leaf-saturation/logs/primary.log new file mode 100644 index 0000000000..33db553260 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/primary.log @@ -0,0 +1,48 @@ +{ + "controls": { + "interval_domain_rejections": 3, + "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1" + }, + "finite_law": { + "extra_terminal_truncation": "rejected", + "ordered_word_max_depth": 3, + "whole_flow_fixtures": 8 + }, + "parameters": { + "alpha": [ + "0.98981438244597", + "0.98981438244599" + ], + "drift_above_log5": [ + "0.016477707041", + "0.016477707042" + ], + "invoice_derivative_lower_bound_interval_0_99_to_1": [ + "211661.930309", + "211661.930310" + ], + "lambda": [ + "0.00749912850515", + "0.00749912850519" + ], + "mean_deficit_limit": [ + "133.34882837", + "133.34882838" + ], + "mean_leaf_depth_limit": [ + "136.51870330", + "136.51870331" + ], + "mean_log_rank": [ + "1.625915619475", + "1.625915619476" + ], + "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds", + "t_star": [ + "0.99731351095114", + "0.99731351095116" + ] + }, + "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.", + "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS" +} diff --git a/research/direct-flow-leaf-saturation/logs/registered.log b/research/direct-flow-leaf-saturation/logs/registered.log new file mode 100644 index 0000000000..b4772c2b4a --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/registered.log @@ -0,0 +1,118 @@ +CHECK Exact rational root/drift/tilt/limit enclosures, eight whole-flow fixtures, lattice and domain failure controls; classical LLT proof is written, not machine-checked. +{ + "controls": { + "interval_domain_rejections": 3, + "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1" + }, + "finite_law": { + "extra_terminal_truncation": "rejected", + "ordered_word_max_depth": 3, + "whole_flow_fixtures": 8 + }, + "parameters": { + "alpha": [ + "0.98981438244597", + "0.98981438244599" + ], + "drift_above_log5": [ + "0.016477707041", + "0.016477707042" + ], + "invoice_derivative_lower_bound_interval_0_99_to_1": [ + "211661.930309", + "211661.930310" + ], + "lambda": [ + "0.00749912850515", + "0.00749912850519" + ], + "mean_deficit_limit": [ + "133.34882837", + "133.34882838" + ], + "mean_leaf_depth_limit": [ + "136.51870330", + "136.51870331" + ], + "mean_log_rank": [ + "1.625915619475", + "1.625915619476" + ], + "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds", + "t_star": [ + "0.99731351095114", + "0.99731351095116" + ] + }, + "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.", + "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS" +} +CHECK Ten independent ordered-word fixtures agree with PR4436 and PR4467 leaf histograms; wrong final truncation rejected. +{ + "status": "PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION", + "fixtures": [ + { + "N": 121, + "G": 0, + "leaf_ranks": 9, + "terminal_truncation_rejected": true + }, + { + "N": 604, + "G": 0, + "leaf_ranks": 9, + "terminal_truncation_rejected": true + }, + { + "N": 605, + "G": 1, + "leaf_ranks": 26, + "terminal_truncation_rejected": true + }, + { + "N": 606, + "G": 1, + "leaf_ranks": 26, + "terminal_truncation_rejected": true + }, + { + "N": 3024, + "G": 1, + "leaf_ranks": 30, + "terminal_truncation_rejected": true + }, + { + "N": 3025, + "G": 2, + "leaf_ranks": 55, + "terminal_truncation_rejected": true + }, + { + "N": 3026, + "G": 2, + "leaf_ranks": 55, + "terminal_truncation_rejected": true + }, + { + "N": 15124, + "G": 2, + "leaf_ranks": 65, + "terminal_truncation_rejected": true + }, + { + "N": 15125, + "G": 3, + "leaf_ranks": 98, + "terminal_truncation_rejected": true + }, + { + "N": 15126, + "G": 3, + "leaf_ranks": 98, + "terminal_truncation_rejected": true + } + ] +} +CHECK Reject changed source bytes, altered histogram bracket, and corrupted expected receipt, including under optimized Python. +PASS_MUTATION_CONTROLS source_bytes_normal_and_optimized corrupted_receipt paid_and_target_count_plus_one +PASS_REGISTERED_RESEARCH_PACKAGE research/direct-flow-leaf-saturation outcome=completed diff --git a/research/direct-flow-leaf-saturation/logs/validation.json b/research/direct-flow-leaf-saturation/logs/validation.json new file mode 100644 index 0000000000..7a3734b6f2 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/validation.json @@ -0,0 +1,117 @@ +{ + "python": "3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]", + "platform": "Linux-6.18.55-x86_64-with-glibc2.41", + "base": "721c03822c421b7f7fcbb2598993b947c4d88419", + "runs": [ + { + "name": "metadata", + "command": [ + "python3", + "-B", + "scripts/research_package.py", + "--package", + "research/direct-flow-leaf-saturation", + "--check-only" + ], + "exit_code": 0, + "seconds": 0.207, + "log": "logs/metadata.log" + }, + { + "name": "primary", + "command": [ + "python3", + "-B", + "research/direct-flow-leaf-saturation/verify.py", + "--expect", + "research/direct-flow-leaf-saturation/RESULT.json" + ], + "exit_code": 0, + "seconds": 15.394, + "log": "logs/primary.log" + }, + { + "name": "optimized", + "command": [ + "python3", + "-B", + "-O", + "research/direct-flow-leaf-saturation/verify.py", + "--expect", + "research/direct-flow-leaf-saturation/RESULT.json" + ], + "exit_code": 0, + "seconds": 16.419, + "log": "logs/optimized.log" + }, + { + "name": "independent", + "command": [ + "python3", + "-B", + "research/direct-flow-leaf-saturation/independent_source.py" + ], + "exit_code": 0, + "seconds": 0.098, + "log": "logs/independent.log" + }, + { + "name": "independent-optimized", + "command": [ + "python3", + "-B", + "-O", + "research/direct-flow-leaf-saturation/independent_source.py" + ], + "exit_code": 0, + "seconds": 0.169, + "log": "logs/independent-optimized.log" + }, + { + "name": "mutations", + "command": [ + "python3", + "-B", + "research/direct-flow-leaf-saturation/test_controls.py" + ], + "exit_code": 0, + "seconds": 30.049, + "log": "logs/mutations.log" + }, + { + "name": "mutations-optimized", + "command": [ + "python3", + "-B", + "-O", + "research/direct-flow-leaf-saturation/test_controls.py" + ], + "exit_code": 0, + "seconds": 30.11, + "log": "logs/mutations-optimized.log" + }, + { + "name": "registered", + "command": [ + "python3", + "-B", + "scripts/research_package.py", + "--package", + "research/direct-flow-leaf-saturation" + ], + "exit_code": 0, + "seconds": 43.277, + "log": "logs/registered.log" + } + ], + "scientific_files_sha256": { + "PROOF.md": "b6edd825bc5a3a48fc2860533040faa111c7f239f8724bb3b50cc8a3bdfdc6e7", + "verify.py": "9a6ed8de94eab4a643685eba3697d34503bae9dd4c6097b6b8a6f230c29dd3b8", + "RESULT.json": "7c0b9019941b2178c58c846a1077748669eab39c39128b4ca9e5f6455f736aef", + "independent_source.py": "4aef5b1d0c61a9af68d27c4fdda924e188363a9b7444c75e6d1c6b666db834b0", + "test_controls.py": "04410e43354ebb70ad52dc18ecd3d54e3369b2c41161558555dc12c37bb9ac61", + "SOURCES.json": "90997ec1be8cd8c3e588d71a349783b2f1696a224dc082749f3886bebd8c2c4a", + "VERIFY.json": "b7e76cf715a9d4bcbf0482f64856852ccf410d1c5fecbb7fed04283550e72e54" + }, + "post_run_prose_edit": "Normalized PR-number references to #NUMBER and linked the verified canonical claim; no mathematical or computational change." +} diff --git a/research/direct-flow-leaf-saturation/test_controls.py b/research/direct-flow-leaf-saturation/test_controls.py new file mode 100644 index 0000000000..c9ecee0465 --- /dev/null +++ b/research/direct-flow-leaf-saturation/test_controls.py @@ -0,0 +1,59 @@ +#!/usr/bin/env python3 +"""Mutation controls for the certificate boundary. DLamdata/Codex, Apache-2.0.""" +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +spec = importlib.util.spec_from_file_location('certificate', HERE / 'verify.py') +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) + + +def require_rejection(argv, cwd, needle): + run = subprocess.run(argv, cwd=cwd, text=True, capture_output=True, timeout=60) + if run.returncode == 0 or needle not in run.stderr: + raise ValueError(f'control did not reject with {needle!r}: {run.returncode}, {run.stderr[-400:]}') + + +with tempfile.TemporaryDirectory(prefix='leaf-saturation-controls-') as directory: + root = Path(directory) + package = root / 'research/direct-flow-leaf-saturation' + package.mkdir(parents=True) + for name in ('verify.py', 'SOURCES.json', 'RESULT.json'): + shutil.copy2(HERE / name, package / name) + sources = json.loads((HERE / 'SOURCES.json').read_text()) + for row in sources['files']: + if row['usage'] == 'input': + target = root / row['path'] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(ROOT / row['path'], target) + source = root / 'research/direct-flow-leaf-walk/verify.py' + original = source.read_bytes() + source.write_bytes(original + b'\n# corrupt-source control\n') + for mode in ([], ['-O']): + require_rejection([sys.executable, *mode, '-B', str(package / 'verify.py')], root, 'source mismatch') + source.write_bytes(original) + expected = json.loads((package / 'RESULT.json').read_text()) + expected['parameters']['lambda'][0] = '0.0' + receipt = package / 'corrupt-result.json' + receipt.write_text(json.dumps(expected)) + require_rejection([sys.executable, '-O', '-B', str(package / 'verify.py'), '--expect', str(receipt)], root, 'expected receipt mismatch') + +for name in ('paid', 'target'): + P, W, M = v.bindings() + histogram = P if name == 'paid' else W + histogram[min(histogram)] += 1 + try: + v.parameters(P, W, M) + except ValueError as error: + if 'invoice root bracket' not in str(error): + raise + else: + raise ValueError('changed histogram passed fixed root certificate: ' + name) +print('PASS_MUTATION_CONTROLS source_bytes_normal_and_optimized corrupted_receipt paid_and_target_count_plus_one') diff --git a/research/direct-flow-leaf-saturation/verify.py b/research/direct-flow-leaf-saturation/verify.py new file mode 100644 index 0000000000..b5007aadb8 --- /dev/null +++ b/research/direct-flow-leaf-saturation/verify.py @@ -0,0 +1,223 @@ +#!/usr/bin/env python3 +"""Exact source/parameter/finite-law checks; does not mechanically prove the LLT. +DLamdata with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from functools import lru_cache +from pathlib import Path +import argparse +import ast +import hashlib +import itertools +import json +import math +import runpy + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +# Rational intervals. No machine floating-point arithmetic in certification. +def add(a, b): + return a[0] + b[0], a[1] + b[1] + + +def neg(a): + return -a[1], -a[0] + + +def mul(a, b): + v = [x * y for x in a for y in b] + return min(v), max(v) + + +def div(a, b): + need(b[0] > 0, 'positive denominator required') + return mul(a, (1 / b[1], 1 / b[0])) + + +def pt(x): + return Q(x), Q(x) + + +@lru_cache(None) +def log_bounds(n): + """log(n) via 2 atanh(z), |z|<=1/3, with geometric tail.""" + need(isinstance(n, int) and n >= 1, 'positive integer log input') + if n == 1: + return pt(0) + e = n.bit_length() - 1 + u = Q(n, 2 ** e) + + def series(z): + total = sum((2 * z ** (2 * k + 1) / (2 * k + 1) for k in range(48)), Q(0)) + tail = 2 * z ** 97 / (97 * (1 - z * z)) + return total, total + tail + + return add(mul(pt(e), series(Q(1, 3))), series((u - 1) / (u + 1))) + + +@lru_cache(None) +def exp_point(x): + """Taylor enclosure for 0<=x<=5; exp(x)<=3^5 bounds remainder.""" + need(0 <= x <= 5, 'exp domain [0,5]') + term = total = Q(1) + for k in range(1, 81): + term = term * x / k + total += term + tail = Q(3 ** 5) * term * x / 81 + return total, total + tail + + +def exp_bounds(x): + return exp_point(x[0])[0], exp_point(x[1])[1] + + +def power(n, t): + return exp_bounds(mul(log_bounds(n), pt(t))) + + +def moment(hist, t, derivative=False): + out = pt(0) + for rank, count in hist.items(): + term = mul(pt(count), power(rank, t)) + if derivative: + term = mul(term, log_bounds(rank)) + out = add(out, term) + return out + + +def mean(hist, t): + return div(moment(hist, t, True), moment(hist, t)) + + +def rounded(a, places=12): + scale = 10 ** places + lo = a[0].numerator * scale // a[0].denominator + hi = -((-a[1].numerator * scale) // a[1].denominator) + def fmt(k): + sign = '-' if k < 0 else '' + k = abs(k) + return f'{sign}{k // scale}.{k % scale:0{places}d}' + return [fmt(lo), fmt(hi)] + + +def bindings(): + source = json.loads((HERE / 'SOURCES.json').read_text()) + for row in source['files']: + if row['usage'] == 'input': + need(hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'], + 'source mismatch: ' + row['path']) + path = ROOT / 'research/direct-flow-leaf-walk/verify.py' + constants = {} + for node in ast.parse(path.read_text()).body: + if isinstance(node, ast.Assign) and len(node.targets) == 1 and isinstance(node.targets[0], ast.Name): + if node.targets[0].id in ('P', 'W', 'M'): + constants[node.targets[0].id] = ast.literal_eval(node.value) + need(set(constants) == {'P', 'W', 'M'}, 'source constants missing') + return constants['P'], constants['W'], constants['M'] + + +def parameters(P, W, M): + t = (Q('0.99731351095114'), Q('0.99731351095116')) + alpha = (Q('0.98981438244597'), Q('0.98981438244599')) + # Positive derivative on the full source bisection interval identifies its root. + f_lo = add(moment(W, t[0]), neg(moment(P, t[0]))) + f_hi = add(moment(W, t[1]), neg(moment(P, t[1]))) + derivative = add(moment(W, Q('0.99'), True), neg(moment(P, Q(1), True))) + need(f_lo[1] < 0 < f_hi[0] and derivative[0] > 0, 'invoice root bracket') + a = log_bounds(5) + need(mean(P, alpha[0])[1] < a[0] and mean(P, alpha[1])[0] > a[1], 'tilt mean bracket') + mu = mean(P, t[0])[0], mean(P, t[1])[1] # mean strictly increases: derivative=variance>0. + drift = add(mu, neg(a)) + need(drift[0] > 0, 'positive drift') + need(all(P.get(k, 0) > 0 for k in (1, 2, 3)), 'nonlattice support witness 1,2,3') + lam = add(t, neg(alpha)) + inverse = div(pt(1), lam) + depth = add(add(log_bounds(M), neg(mu)), inverse) + return {'t_star': rounded(t, 14), 'alpha': rounded(alpha, 14), + 'lambda': rounded(lam, 14), 'mean_log_rank': rounded(mu), + 'invoice_derivative_lower_bound_interval_0_99_to_1': rounded(derivative, 6), + 'drift_above_log5': rounded(drift), 'mean_deficit_limit': rounded(inverse, 8), + 'mean_leaf_depth_limit': rounded(depth, 8), + 'method': 'exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds'} + + +def finite_law(P, W, M): + # Independent ordered-word enumeration vs the predecessor's whole-flow X-BX. + flow = runpy.run_path(str(ROOT / 'research/direct-flow-leaf-walk/diagnostics/overlap_flow.py'))['flow'] + count = 0 + extra_truncation_detected = False + for G in range(4): + for N in (M * 5 ** G, M * 5 ** G + M * 5 ** G // 2): + got = flow(N, W, P) + need(got['G'] == G, 'flow depth') + prefixes = {} + for word in itertools.product(P, repeat=G): + rho = math.prod(word) + if M * rho <= N: + prefixes[rho] = prefixes.get(rho, 0) + math.prod(P[r] for r in word) + leaves, wrong = {}, {} + for rho, multiplicity in prefixes.items(): + for r, pr in P.items(): + e = rho * r + leaves[e] = leaves.get(e, 0) + multiplicity * pr + if M * e <= N: + wrong[e] = wrong.get(e, 0) + multiplicity * pr + actual = {e: c - got['BX'].get(e, 0) for e, c in got['X'].items() if c != got['BX'].get(e, 0)} + need(actual == leaves, 'ordered words disagree with actual leaf exits') + # At t=1, the weighted final-r distribution factorizes exactly. + leaf_mass = sum(e * c for e, c in leaves.items()) + need(leaf_mass == sum(rho * c for rho, c in prefixes.items()) * sum(r * c for r, c in P.items()), 'independent terminal rank') + extra_truncation_detected |= wrong != actual + count += 1 + need(extra_truncation_detected, 'extra-terminal-truncation control did not discriminate') + return {'whole_flow_fixtures': count, 'ordered_word_max_depth': 3, + 'extra_terminal_truncation': 'rejected'} + + +def controls(): + # Lattice countermodel: X in {0,log2}, p(X=log2)=2/3, barrier n log2/2. + # At even n the limiting gap/log2 is geometric with mean 1, whereas + # the nonlattice formula would give mean gap=1 (lambda=1). + means = [] + for n in (40, 400): + denominator = sum(math.comb(n, k) * 2 ** k for k in range(n // 2 + 1)) + numerator = sum((n // 2 - k) * math.comb(n, k) * 2 ** k for k in range(n // 2 + 1)) + means.append(Q(numerator, denominator)) + need(0 < means[0] < means[1] < 1, 'lattice geometric control') + need(mul(pt(means[1]), log_bounds(2))[1] < Q(7, 10), 'lattice mean must differ from exponential mean 1') + rejected = 0 + for f in (lambda: div(pt(1), (-Q(1), Q(1))), lambda: exp_point(Q(-1)), lambda: log_bounds(0)): + try: + f() + except ValueError: + rejected += 1 + need(rejected == 3, 'interval domain controls') + # Elementary exact enclosure controls include endpoint exp0/log1 identities. + need(log_bounds(1) == pt(0) and exp_point(Q(0)) == pt(1), 'identity fixtures') + need(log_bounds(2)[0] > Q(69, 100) and log_bounds(2)[1] < Q(7, 10), 'log2 fixture') + return {'lattice_countermodel': 'geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1', + 'interval_domain_rejections': rejected} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--expect', type=Path) + args = parser.parse_args() + P, W, M = bindings() + result = {'status': 'PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS', 'parameters': parameters(P, W, M), + 'finite_law': finite_law(P, W, M), 'controls': controls(), + 'scope': 'Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.'} + if args.expect: + need(result == json.loads(args.expect.read_text()), 'expected receipt mismatch') + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() From ff365dba6911ce615bec76e8d1f149faf1fe16ca Mon Sep 17 00:00:00 2001 From: Figo Lam Date: Wed, 28 Oct 2026 11:29:21 +0000 Subject: [PATCH 2/7] Record committed export and Git-free replay evidence --- .../direct-flow-leaf-saturation/VALIDATION.md | 14 +++- .../logs/portable-0.log | 48 ++++++++++++++ .../logs/portable-1.log | 65 +++++++++++++++++++ .../logs/portable-2.log | 1 + .../logs/portable-results.json | 40 ++++++++++++ 5 files changed, 167 insertions(+), 1 deletion(-) create mode 100644 research/direct-flow-leaf-saturation/logs/portable-0.log create mode 100644 research/direct-flow-leaf-saturation/logs/portable-1.log create mode 100644 research/direct-flow-leaf-saturation/logs/portable-2.log create mode 100644 research/direct-flow-leaf-saturation/logs/portable-results.json diff --git a/research/direct-flow-leaf-saturation/VALIDATION.md b/research/direct-flow-leaf-saturation/VALIDATION.md index 2db84d4a5e..9afb1c1bfc 100644 --- a/research/direct-flow-leaf-saturation/VALIDATION.md +++ b/research/direct-flow-leaf-saturation/VALIDATION.md @@ -35,4 +35,16 @@ No selected-construction replay, `make verify`, historical heavy suite, Lean, or ## Committed bytes and portable replay -The publication preflight, official export integrity check and Git-free replay are recorded below after execution. They check transport and reproducibility, not the analytic theorem. +At scientific commit `9465f263a673d2d86e7262523cbeb0e796f486cf`, the following commands passed on all 26 package/input files: + +```sh +python3 -B scripts/check_research_commit.py --package research/direct-flow-leaf-saturation --check-source-history +python3 -B scripts/export_research_package.py export --package research/direct-flow-leaf-saturation --ref 9465f263a673d2d86e7262523cbeb0e796f486cf --output /tmp/leaf-saturation.tar +python3 -B scripts/export_research_package.py check /tmp/leaf-saturation.tar +``` + +The actual temporary archive path was outside the repository; `/tmp/leaf-saturation.tar` above is the portable equivalent. Both exporter commands reported `PASS_RESEARCH_EXPORT`. Committed-byte comparison reported `PASS_RESEARCH_COMMIT_BYTES`, with source-history commit `721c03822c421b7f7fcbb2598993b947c4d88419`. + +After extraction into a fresh directory, with PATH pointing to an empty directory and no Git available, all three direct package commands passed: main verifier 14.383 s, independent source checker 0.094 s, mutation controls 28.189 s. [logs/portable-results.json](logs/portable-results.json) records the actual commands, exits and logs. Their source bytes are exactly the scientific commit above; subsequent packaging adds these logs and this record without changing the proof or checker. + +These checks establish committed-source availability, transport integrity and portable replay. They do not prove the analytic theorem. Final publication-byte preflight is repeated after recording this evidence; the PR pins the final contribution SHA. diff --git a/research/direct-flow-leaf-saturation/logs/portable-0.log b/research/direct-flow-leaf-saturation/logs/portable-0.log new file mode 100644 index 0000000000..33db553260 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/portable-0.log @@ -0,0 +1,48 @@ +{ + "controls": { + "interval_domain_rejections": 3, + "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1" + }, + "finite_law": { + "extra_terminal_truncation": "rejected", + "ordered_word_max_depth": 3, + "whole_flow_fixtures": 8 + }, + "parameters": { + "alpha": [ + "0.98981438244597", + "0.98981438244599" + ], + "drift_above_log5": [ + "0.016477707041", + "0.016477707042" + ], + "invoice_derivative_lower_bound_interval_0_99_to_1": [ + "211661.930309", + "211661.930310" + ], + "lambda": [ + "0.00749912850515", + "0.00749912850519" + ], + "mean_deficit_limit": [ + "133.34882837", + "133.34882838" + ], + "mean_leaf_depth_limit": [ + "136.51870330", + "136.51870331" + ], + "mean_log_rank": [ + "1.625915619475", + "1.625915619476" + ], + "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds", + "t_star": [ + "0.99731351095114", + "0.99731351095116" + ] + }, + "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.", + "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS" +} diff --git a/research/direct-flow-leaf-saturation/logs/portable-1.log b/research/direct-flow-leaf-saturation/logs/portable-1.log new file mode 100644 index 0000000000..f50d39a3e3 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/portable-1.log @@ -0,0 +1,65 @@ +{ + "status": "PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION", + "fixtures": [ + { + "N": 121, + "G": 0, + "leaf_ranks": 9, + "terminal_truncation_rejected": true + }, + { + "N": 604, + "G": 0, + "leaf_ranks": 9, + "terminal_truncation_rejected": true + }, + { + "N": 605, + "G": 1, + "leaf_ranks": 26, + "terminal_truncation_rejected": true + }, + { + "N": 606, + "G": 1, + "leaf_ranks": 26, + "terminal_truncation_rejected": true + }, + { + "N": 3024, + "G": 1, + "leaf_ranks": 30, + "terminal_truncation_rejected": true + }, + { + "N": 3025, + "G": 2, + "leaf_ranks": 55, + "terminal_truncation_rejected": true + }, + { + "N": 3026, + "G": 2, + "leaf_ranks": 55, + "terminal_truncation_rejected": true + }, + { + "N": 15124, + "G": 2, + "leaf_ranks": 65, + "terminal_truncation_rejected": true + }, + { + "N": 15125, + "G": 3, + "leaf_ranks": 98, + "terminal_truncation_rejected": true + }, + { + "N": 15126, + "G": 3, + "leaf_ranks": 98, + "terminal_truncation_rejected": true + } + ] +} diff --git a/research/direct-flow-leaf-saturation/logs/portable-2.log b/research/direct-flow-leaf-saturation/logs/portable-2.log new file mode 100644 index 0000000000..ba3e3e0348 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/portable-2.log @@ -0,0 +1 @@ +PASS_MUTATION_CONTROLS source_bytes_normal_and_optimized corrupted_receipt paid_and_target_count_plus_one diff --git a/research/direct-flow-leaf-saturation/logs/portable-results.json b/research/direct-flow-leaf-saturation/logs/portable-results.json new file mode 100644 index 0000000000..1855fd7914 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/portable-results.json @@ -0,0 +1,40 @@ +{ + "export_commit": "9465f263a673d2d86e7262523cbeb0e796f486cf", + "export_files": 26, + "git_available": false, + "path": "empty directory", + "runs": [ + { + "command": [ + "python3", + "-B", + "research/direct-flow-leaf-saturation/verify.py", + "--expect", + "research/direct-flow-leaf-saturation/RESULT.json" + ], + "exit_code": 0, + "seconds": 14.383, + "log": "logs/portable-0.log" + }, + { + "command": [ + "python3", + "-B", + "research/direct-flow-leaf-saturation/independent_source.py" + ], + "exit_code": 0, + "seconds": 0.094, + "log": "logs/portable-1.log" + }, + { + "command": [ + "python3", + "-B", + "research/direct-flow-leaf-saturation/test_controls.py" + ], + "exit_code": 0, + "seconds": 28.189, + "log": "logs/portable-2.log" + } + ] +} From 553198839618962e07519b51cb3bbe808ca6f1dc Mon Sep 17 00:00:00 2001 From: Figo Lam Date: Wed, 28 Oct 2026 12:30:51 +0000 Subject: [PATCH 3/7] Address Claude review of leaf-saturation proof and checks --- .../CLAUDE-RESPONSE.md | 32 ++++ research/direct-flow-leaf-saturation/PROOF.md | 24 ++- .../direct-flow-leaf-saturation/README.md | 21 +-- .../direct-flow-leaf-saturation/RESULT.json | 3 +- .../direct-flow-leaf-saturation/REVIEW.md | 16 +- .../direct-flow-leaf-saturation/TASK.json | 2 +- .../direct-flow-leaf-saturation/VALIDATION.md | 30 +++- .../direct-flow-leaf-saturation/VERIFY.json | 13 +- .../independent_source.py | 14 +- .../logs/claude-enclosures-normal.json | 33 ++++ .../logs/claude-enclosures-optimized.json | 33 ++++ .../logs/claude-enclosures-timing.json | 14 ++ .../logs/claude-independent-optimized.log | 65 +++++++ .../logs/claude-metadata.log | 1 + .../logs/claude-mutations-optimized.log | 1 + .../logs/claude-optimized.log | 49 +++++ .../logs/claude-registered.log | 153 ++++++++++++++++ .../logs/claude-validation.json | 84 +++++++++ .../test_controls.py | 53 +++++- .../test_enclosures.py | 170 ++++++++++++++++++ .../direct-flow-leaf-saturation/verify.py | 14 +- 21 files changed, 784 insertions(+), 41 deletions(-) create mode 100644 research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md create mode 100644 research/direct-flow-leaf-saturation/logs/claude-enclosures-normal.json create mode 100644 research/direct-flow-leaf-saturation/logs/claude-enclosures-optimized.json create mode 100644 research/direct-flow-leaf-saturation/logs/claude-enclosures-timing.json create mode 100644 research/direct-flow-leaf-saturation/logs/claude-independent-optimized.log create mode 100644 research/direct-flow-leaf-saturation/logs/claude-metadata.log create mode 100644 research/direct-flow-leaf-saturation/logs/claude-mutations-optimized.log create mode 100644 research/direct-flow-leaf-saturation/logs/claude-optimized.log create mode 100644 research/direct-flow-leaf-saturation/logs/claude-registered.log create mode 100644 research/direct-flow-leaf-saturation/logs/claude-validation.json create mode 100644 research/direct-flow-leaf-saturation/test_enclosures.py diff --git a/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md b/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md new file mode 100644 index 0000000000..0a550225ae --- /dev/null +++ b/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md @@ -0,0 +1,32 @@ +# Response to the Claude Code review of ff365dba + +The review examined `ff365dba6911ce615bec76e8d1f149faf1fe16ca` and confirmed the scoped theorem and numerical enclosures. This response preserves that theorem, its fixed raw-p7 scope and all parameter values. Claude Code and the follow-up Codex reviewers are AI reviewers, not independent human or formal verification. + +| Finding | Resolution | Evidence and limit | +| --- | --- | --- | +| 1. Stone statement and uniformity need precise citation | PROOF.md §3 now names Corollary 1 (7), Theorem (5) and footnote 2; gives the normalization/rescaling and characteristic-function/support equivalence. | Fixed-x (12) is explicitly not the source of uniform concentration. The review reports checking the primary paper; the follow-up internal proof review corroborated the uniform form from Stone's later text but did not retrieve the original afresh. Stronger nonlattice rate hypotheses fail for finite support; this does not exclude quantitative rates by other methods. | +| 2. Terminal-rank flags overstate coverage | Removed the redundant self-factorization assertion; renamed flags as fixture sensitivity. The source identity is the complete histogram comparison. | `test_controls.py` actually empties or truncates the source leaf branch in a temporary tree, re-pins the mutant bytes, and requires semantic rejection by both source-law entry points, normally and under `-O`. A checksum failure cannot count as this semantic rejection. | +| 3. Remainder bounds lack discriminating controls | Added `test_enclosures.py`, an exact-rational independent enclosure oracle. | It checks every successful log/exp argument captured from current `parameters()` and `controls()`. Logarithms use a different series; exponentials use a positive-series geometric tail rather than the primary Lagrange bound. Zero logarithm/exponential tails and the invalid majorant 1 are rejected at explicit fixtures even though the old rounded receipt did not distinguish them. | +| 4. Standalone independent source checker lacks byte binding | `independent_source.py` authenticates every declared live input before any predecessor import. | Comment-only mutations to both predecessor verifier and original flow are rejected by both standalone entry points in normal and optimized modes. No Git is needed. | +| 5. Executable source domain ends at G≤3 | Retained and explicitly scoped; no unnecessary search expansion. | The source proof is for every G, while the local primary/independent fixtures remain eight/ten checks through G=3. Claude reported further G=4–5 corroboration; this package does not present that as a newly executed local check. | +| 6. Leaf observable lacks an explicit formula | PROOF.md §1 now defines the normalized potential-weighted sum over `X−BX`, and its equivalent sum with weights `F[G][ρ] P_r (rρ)^t`. | The final rank uses the full paid inventory and both denominators are positive. The limit is unchanged. | + +## What the new controls do not prove + +The remainder oracle certifies containment on the captured finite argument domain. Both implementations still share Python's exact rational arithmetic and the exponential series; the logarithm series and exponential remainder arguments differ. This is not formal verification or a proof of the routines for arbitrary future inputs. Its domain digest and loaded verifier SHA identify the checked inputs and code. + +The +1 histogram mutations are regressions for the fixed narrow root bracket, not general tests of interval arithmetic. The derivative-bound endpoint ordering is justified by the written monotonicity argument and code review; a changed printed derivative is also caught by the expected receipt. The new enclosure tests do not claim to independently prove that derivative formula. + +The source mutation controls exercise the complete histogram equality checks. A flag saying that a fixture has an exit above N/121 only describes its ability to distinguish truncation; it does not independently authenticate or validate a source implementation. + +The registered runner still declares Python 3.12. README commands now explicitly select `python3.12` to avoid a default `python3` selecting 3.13 and failing that version gate. No dependency or runner policy is changed. + +## Reproduce the response + +```sh +python3.12 -B scripts/research_package.py --package research/direct-flow-leaf-saturation +python3.12 -O -B research/direct-flow-leaf-saturation/test_controls.py +python3.12 -O -B research/direct-flow-leaf-saturation/test_enclosures.py +``` + +[VALIDATION.md](VALIDATION.md) records the actual runs, source hashes and portable replay. The full-flow ceiling, finite-depth rates, stable shares, and supplier admission remain open. The selected #6030 record is unchanged. diff --git a/research/direct-flow-leaf-saturation/PROOF.md b/research/direct-flow-leaf-saturation/PROOF.md index 0d7d4c4a8b..9e0a493dcc 100644 --- a/research/direct-flow-leaf-saturation/PROOF.md +++ b/research/direct-flow-leaf-saturation/PROOF.md @@ -27,7 +27,14 @@ Under `p_t(r)=P_r r^t/Z(t)`, take independent `X_i=log R_i` and write `S_G=Σ_{i The condition has positive probability because `P_1>0`. -**Actual leaf consequence.** For every integer rank `N≥121`, set `G=floor(log_5(N/121))` and `δ=log(N/121)−G log5∈[0,a)`. The potential-weighted mean leaf log-depth in the pinned flow satisfies +**Actual leaf consequence.** For every integer rank `N≥121`, set `G=floor(log_5(N/121))` and `δ=log(N/121)−G log5∈[0,a)`. Write `L_N(ℓ)=X_N(ℓ)−BX_N(ℓ)` for the pinned flow's leaf-exit multiplicity at rank `ℓ`, subtracting its boundary-exit histogram from its complete exit histogram and interpreting missing entries as zero. Define its potential-weighted mean leaf log-depth by + +``` +D_leaf(N) = [Σ_ℓ L_N(ℓ) ℓ^t log(N/ℓ)] / [Σ_ℓ L_N(ℓ) ℓ^t] + = [Σ_ρ Σ_r F[G][ρ] P_r (rρ)^t log(N/(rρ))] / [Σ_ρ Σ_r F[G][ρ] P_r (rρ)^t]. +``` + +Here `F[G]` is the prefix-count table described in §2, and both sums over `r` use the entire paid inventory. The denominators are positive because the all-ones prefix and terminal rank are present. Then `D_leaf(N) → log121 − μ(t) + 1/λ ∈ [136.51870330,136.51870331]` @@ -51,9 +58,20 @@ We use the nonlattice interval local-limit theorem in the following standard for `sup_x | sqrt(G) P(Σ V_i∈[x,x+h)) − h/(σ sqrt(2π)) exp(−x²/(2Gσ²)) | → 0`. -Reference: C. Stone, “A local limit theorem for nonlattice multi-dimensional distribution functions,” *The Annals of Mathematical Statistics* 36(2) (1965), 546–551, [DOI 10.1214/aoms/1177700165](https://doi.org/10.1214/aoms/1177700165), one-dimensional specialization. This theorem is an external mathematical dependency; it is stated here rather than silently replacing a discrete distribution by a density. Its asymptotic form supplies no explicit error constant or onset G. +Reference: C. Stone, “A local limit theorem for nonlattice multi-dimensional distribution functions,” *The Annals of Mathematical Statistics* 36(2) (1965), 546–551, [DOI 10.1214/aoms/1177700165](https://doi.org/10.1214/aoms/1177700165), **Corollary 1, equation (7), derived from the Theorem, equation (5), with footnote 2's uniformity convention**. The displayed form is a specialization, not a verbatim quotation. Use `d=1`, `A_G=0`, `B_G=√G` in Stone's normalization (his `B_G` is unrelated to our barrier `Ga+δ`), and normal limiting density `φ_σ(u)=exp(−u²/(2σ²))/(σ√(2π))`. For `T_G=Σ V_i` and any fixed width `H>0`, substitute `x=X/√G` and `h=H/√G` in his half-open boxes. This gives, uniformly over `X∈R`, + +``` +P(T_G∈[X,X+H)) = ∫_[X/√G,(X+H)/√G) φ_σ(u) du + o(G^(−1/2)) + = (H/√G) φ_σ(X/√G) + o(G^(−1/2)). +``` + +The second equality uses uniform continuity of the Gaussian density. Multiplying by `√G` gives the required supremum statement; footnote 2 makes the remainder uniform in the unlisted variable `x`, hence also in `X`. The paper's Corollary 4, equation (12), is only a fixed-`x` statement and is not the input used for our uniform concentration bound. Stone's theorem is an external mathematical dependency; no discrete law is replaced by a density without this interval argument. + +Apply it to the tilted law `q(r)=P_r r^α/Z(α)`, with `V=log r−a`. Its mean is zero by definition, and its variance is positive and finite because the support is finite and contains distinct points of positive mass. The ordinary central limit theorem supplies Stone's normal domain-of-attraction hypothesis with this normalization. The support is nonlattice: it contains `0,log2,log3` before centering. If all belonged to a translate of `hZ`, their differences would imply `log2/log3` rational. An integer relation `u log2=v log3` with nonzero integers would imply `2^u=3^v`, contradicting unique factorization. Centering and tilting do not alter this property. + +This support argument verifies Stone's characteristic-function condition (2). Indeed, for `θ≠0`, equality `|E exp(iθV)|=1` holds exactly when the unit complex variable `exp(iθV)` is almost surely constant, equivalently when the support lies in `c/θ+(2π/θ)Z` for some real `c`. Thus nonlattice support gives strict inequality for every nonzero `θ`. -Apply it to the tilted law `q(r)=P_r r^α/Z(α)`, with `V=log r−a`. Its mean is zero by definition, and its variance is positive and finite because the support is finite and contains distinct points of positive mass. The support is nonlattice: it contains `0,log2,log3` before centering. If all belonged to a translate of `hZ`, their differences would imply `log2/log3` rational. An integer relation `u log2=v log3` with nonzero integers would imply `2^u=3^v`, contradicting unique factorization. Centering and tilting do not alter this property. +The finite support does **not** satisfy Stone's stronger condition (3): simultaneous approximation of its finitely many phases gives arbitrarily large `|θ|` for which the characteristic-function modulus approaches one. Stone's stronger rate conclusion requiring that condition is therefore inapplicable here. The asymptotic theorem used in this proof supplies no explicit error constant or onset `G`; this does not rule out quantitative bounds from other methods. Two consequences are used: diff --git a/research/direct-flow-leaf-saturation/README.md b/research/direct-flow-leaf-saturation/README.md index ec6a503ba6..1fe9048298 100644 --- a/research/direct-flow-leaf-saturation/README.md +++ b/research/direct-flow-leaf-saturation/README.md @@ -8,7 +8,7 @@ The [proof](PROOF.md) uses the classical nonlattice interval local-limit theorem - limiting mean deficit in `[133.34882837,133.34882838]`; - limiting actual leaf log-depth in `[136.51870330,136.51870331]`. -The source has **G conditioned paid ranks plus one unconditioned terminal rank**. Ten independent exact fixtures bind this interpretation to both the original #4436 flow and #4467's diagnostic; an incorrectly truncated terminal rank is rejected. The main certificate adds eight fixtures and a lattice countermodel showing why discrete support alone does not justify an exponential limit. +The source has **G conditioned paid ranks plus one unconditioned terminal rank**. Ten independent exact fixtures compare the complete leaf histograms of both the original #4436 flow and #4467's diagnostic. Both standalone entry points authenticate all declared inputs before executing them. Separate mutation tests re-pin empty or terminal-truncated source branches and confirm that the actual histogram comparisons reject them; fixture-sensitivity flags are not counted as extra source checks. The main certificate checks eight fixtures and a lattice countermodel showing why discrete support alone does not justify an exponential limit. This resolves the qualitative saturation part of #4467's open question. It supplies **no explicit finite-depth error rate**, stable-share theorem, full-flow log-gap limit, numerical refined-induction ceiling, new κ, or supplier admission. The raw-p7 profile is historical; the selected #6030 record and its five assumptions are unchanged. In particular, the predecessor's estimated `.0025–.0026` ceiling and enormous finite-rank thresholds remain unproved here. @@ -23,22 +23,23 @@ The original direct flow is zxv's #4436 (`56003680aee2871773de408e5f01cc5dd46b14 Python 3.12, standard library only, assertions not needed. From the repository root: ```sh -python3 -B scripts/research_package.py --package research/direct-flow-leaf-saturation --check-only -python3 -B scripts/research_package.py --package research/direct-flow-leaf-saturation -python3 -O -B research/direct-flow-leaf-saturation/verify.py --expect research/direct-flow-leaf-saturation/RESULT.json +python3.12 -B scripts/research_package.py --package research/direct-flow-leaf-saturation --check-only +python3.12 -B scripts/research_package.py --package research/direct-flow-leaf-saturation +python3.12 -O -B research/direct-flow-leaf-saturation/verify.py --expect research/direct-flow-leaf-saturation/RESULT.json ``` -Direct commands also work from a package export without Git: +The registered runner requires Python 3.12; using a default `python3` that selects 3.13 fails its declared version gate. Direct commands also work from a package export without Git: ```sh -python3 -B research/direct-flow-leaf-saturation/verify.py --expect research/direct-flow-leaf-saturation/RESULT.json -python3 -B research/direct-flow-leaf-saturation/independent_source.py -python3 -B research/direct-flow-leaf-saturation/test_controls.py +python3.12 -B research/direct-flow-leaf-saturation/verify.py --expect research/direct-flow-leaf-saturation/RESULT.json +python3.12 -B research/direct-flow-leaf-saturation/independent_source.py +python3.12 -B research/direct-flow-leaf-saturation/test_controls.py +python3.12 -B research/direct-flow-leaf-saturation/test_enclosures.py ``` -The main certificate uses `Fraction` intervals throughout: a 48-term `2 atanh(z)` series with a geometric tail bounds logarithms after power-of-two reduction; an 80-term exponential Taylor series uses `e^x≤3^5` on `[0,5]` to bound the remainder. Strict endpoint signs and a derivative lower bound isolate the invoice root. Strict monotonicity of the tilted mean (its derivative is a positive variance) isolates the tilt. Output decimals are rounded outward. The certificate does not execute the predecessor's floating-point root finder or fit its data. +The main certificate uses `Fraction` intervals throughout: a 48-term `2 atanh(z)` series with a geometric tail bounds logarithms after power-of-two reduction; an 80-term exponential Taylor series uses `e^x≤3^5` on `[0,5]` to bound the remainder. Strict endpoint signs and a derivative lower bound isolate the invoice root. Strict monotonicity of the tilted mean (its derivative is a positive variance) isolates the tilt. Output decimals are rounded outward. The certificate does not execute the predecessor's floating-point root finder or fit its data. `test_enclosures.py` independently encloses every executed logarithm/exponential argument using a different logarithm series and a geometric-tail exponential bound. It detects zero tails and an invalid exponential majorant even when the rounded parameter receipt stays unchanged. These are finite-domain controls, not an all-input proof of the routines; both engines share exact rational arithmetic and the exponential series. -[VALIDATION.md](VALIDATION.md) records actual commands, environments and logs. [REVIEW.md](REVIEW.md) records the independent derivation, source check, skeptical review and shared dependencies. The proof's local-limit theorem remains an external mathematical input, rather than an assertion tested by finite examples. +[VALIDATION.md](VALIDATION.md) records actual commands, environments and logs, including the response to the user-provided Claude Code review of `ff365dba6911ce615bec76e8d1f149faf1fe16ca`. [REVIEW.md](REVIEW.md) records the independent derivation, source check, skeptical review and shared dependencies. The proof's local-limit theorem remains an external mathematical input, rather than an assertion tested by finite examples. ## Open next questions diff --git a/research/direct-flow-leaf-saturation/RESULT.json b/research/direct-flow-leaf-saturation/RESULT.json index 33db553260..a799a944c4 100644 --- a/research/direct-flow-leaf-saturation/RESULT.json +++ b/research/direct-flow-leaf-saturation/RESULT.json @@ -4,8 +4,9 @@ "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1" }, "finite_law": { - "extra_terminal_truncation": "rejected", "ordered_word_max_depth": 3, + "source_check": "complete actual X-BX histogram equals ordered-word enumeration", + "terminal_cut_distinguishing_fixtures": 8, "whole_flow_fixtures": 8 }, "parameters": { diff --git a/research/direct-flow-leaf-saturation/REVIEW.md b/research/direct-flow-leaf-saturation/REVIEW.md index 490d9bdcba..a1772d4b6f 100644 --- a/research/direct-flow-leaf-saturation/REVIEW.md +++ b/research/direct-flow-leaf-saturation/REVIEW.md @@ -1,6 +1,6 @@ -# Internal review and source independence +# Review history and source independence -Two separate OpenAI Codex agents examined pinned source inputs before seeing the lead's proof. These are internal AI checks, not independent human review, proof-kernel verification, or maintainer acceptance. +The sections below through “Initial integration review” record the initial `ff365dba6911ce615bec76e8d1f149faf1fe16ca` snapshot; their hashes and logs are historical after the later review response. Two separate OpenAI Codex agents examined pinned source inputs before seeing the lead's proof. These are internal AI checks, not independent human review, proof-kernel verification, or maintainer acceptance. ## Independent mathematical derivation @@ -32,7 +32,7 @@ The second reviewer then inspected the frozen proof and verifier (verifier SHA25 No blocking issue was found. The reviewer recommended strengthening monotonicity from the tiny root enclosure to the predecessor's full `[0.99,1]` bisection interval. The final checker implements that stronger bound, exceeding 211661, and includes both +1 histogram controls. The lead reran all affected evidence after this change; the original review hashes do not pretend to identify the final bytes. -## Final integration review +## Initial integration review The skeptical reviewer read the integrated stronger derivative bound, both +1 histogram controls, portable two-source fixture and package claims. No blocker remained. Final reviewed proof SHA256 `b6edd825bc5a3a48fc2860533040faa111c7f239f8724bb3b50cc8a3bdfdc6e7`; verifier SHA256 `9a6ed8de94eab4a643685eba3697d34503bae9dd4c6097b6b8a6f230c29dd3b8`. The reviewer checked that the last proof change was only PR-reference spelling. The confirmed canonical claim link was added to README. Registered evidence and publication checks are reported separately. @@ -41,3 +41,13 @@ The skeptical reviewer read the integrated stronger derivative bound, both +1 hi Orientation coverage was complete for 375 open PRs, 5,222 closed/merged PRs, 5,771 Discussion records and 8,348 local notes at base `721c03822c421b7f7fcbb2598993b947c4d88419` (2026-10-28 11:09–11:11 UTC). Broader body searches also found #4477's disposition, the later finite-share diagnostic, and the author's explicit request for a saturation proof; these still left the proof open. The final refresh is recorded in VALIDATION.md. No body search establishes novelty or covers every code diff. Remaining obligations are an effective finite-depth rate and the other full-flow components/exact induction ratio. Finite tests do not prove the asymptotic result; the asymptotic result does not certify finite-depth extrapolations, a supplier, or the multiplication theorem. + +## Claude review and follow-up + +A user-provided Claude Code AI review independently examined `ff365dba6911ce615bec76e8d1f149faf1fe16ca`. It confirmed the scoped theorem and certified parameter values, reported inspection of Stone's primary text, and identified citation precision and checker-coverage gaps. It is not human or formal verification. The earlier internal reviews' primary-text limitation above remains an accurate description of their work; the later review supplies the equation/footnote mapping now in PROOF.md. + +[CLAUDE-RESPONSE.md](CLAUDE-RESPONSE.md) maps all six findings to the changes and their remaining limits. The theorem and every numerical parameter interval are unchanged. The standalone source checker now authenticates inputs, coverage labels distinguish fixture sensitivity from actual source comparisons, and exact independent log/exp bounds discriminate the reported remainder faults. An additional internal reviewer checked the integrated fixes; current checks and source hashes are in the follow-up section of VALIDATION.md. + +### Final review of the response + +A separate internal reviewer checked the integrated changes without running a competing replay. It verified the alternative logarithm series, the degree 82 exponential geometric tail, full interval containment, meaningful remainder fixtures, re-pinned source mutations and pre-import hashes. No blocking defect was found. Current reviewed verifier SHA256 `3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d`; oracle SHA256 `b92a75601ef676ab0b412395eb2ccaa52c8e802f89fe1fb2f3820cafa173aea4`; proof SHA256 `09dc0d6fd22b5e502b812543ddf78395ab7deacc894cd52430709475acfb2978`. The final oracle metadata addition was checked against the earlier reviewed bytes. These are internal AI reviews with the shared arithmetic/series dependencies disclosed in CLAUDE-RESPONSE.md, not formal verification. diff --git a/research/direct-flow-leaf-saturation/TASK.json b/research/direct-flow-leaf-saturation/TASK.json index 1fd9ee475d..fcc181cdfb 100644 --- a/research/direct-flow-leaf-saturation/TASK.json +++ b/research/direct-flow-leaf-saturation/TASK.json @@ -85,7 +85,7 @@ "budget_minutes": 90, "stop_rule": "Stop after a source-bound saturation proof and certified hypotheses. No stable-share theorem, finite-G rate, whole-flow ceiling, supplier admission or construction search.", "outcome": "completed", - "evidence": "PROOF.md, RESULT.json, independent_source.py, REVIEW.md and VALIDATION.md.", + "evidence": "PROOF.md, RESULT.json, independent_source.py, test_enclosures.py, REVIEW.md, CLAUDE-RESPONSE.md and VALIDATION.md.", "author": "DLamdata", "ai_assistance": "Substantial OpenAI Codex assistance, including two separate native AI agents for independent derivation/source checks and skeptical review. No human or proof-kernel verification.", "open_questions": [ diff --git a/research/direct-flow-leaf-saturation/VALIDATION.md b/research/direct-flow-leaf-saturation/VALIDATION.md index 9afb1c1bfc..926c9bb3af 100644 --- a/research/direct-flow-leaf-saturation/VALIDATION.md +++ b/research/direct-flow-leaf-saturation/VALIDATION.md @@ -1,8 +1,10 @@ # Validation and reproducibility +The initial evidence below is pinned to `ff365dba6911ce615bec76e8d1f149faf1fe16ca`. Its receipt schema and source hashes are historical after the Claude-review response. Follow-up evidence is recorded at the end; numerical parameter intervals are unchanged. + Base and last upstream refresh: `721c03822c421b7f7fcbb2598993b947c4d88419`, 2026-10-28. Priority revision 8. The branch adds only `research/direct-flow-leaf-saturation/`; frozen predecessors and the selected record are unchanged. -## Local evidence actually run +## Initial local evidence actually run Environment: 3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]; Linux-6.18.55-x86_64-with-glibc2.41. Standard library only. The retained environment was activated in the isolated contribution worktree. No dependencies were installed. @@ -33,7 +35,7 @@ The finite verifier certifies source bindings, rational numerical hypotheses, an No selected-construction replay, `make verify`, historical heavy suite, Lean, or Docker run is applicable to this isolated package. Explicit finite-depth bounds, stable whole-flow shares, the exact refined-induction ceiling, supplier admission, and all five selected framework assumptions remain unrun/unresolved here. Hosted CI is separate; consult the contribution PR for its actual status. -## Committed bytes and portable replay +## Initial committed bytes and portable replay At scientific commit `9465f263a673d2d86e7262523cbeb0e796f486cf`, the following commands passed on all 26 package/input files: @@ -48,3 +50,27 @@ The actual temporary archive path was outside the repository; `/tmp/leaf-saturat After extraction into a fresh directory, with PATH pointing to an empty directory and no Git available, all three direct package commands passed: main verifier 14.383 s, independent source checker 0.094 s, mutation controls 28.189 s. [logs/portable-results.json](logs/portable-results.json) records the actual commands, exits and logs. Their source bytes are exactly the scientific commit above; subsequent packaging adds these logs and this record without changing the proof or checker. These checks establish committed-source availability, transport integrity and portable replay. They do not prove the analytic theorem. Final publication-byte preflight is repeated after recording this evidence; the PR pins the final contribution SHA. + +## Claude-review response: current local validation + +The response addresses all six findings on `ff365dba6911ce615bec76e8d1f149faf1fe16ca`; [CLAUDE-RESPONSE.md](CLAUDE-RESPONSE.md) maps scope and evidence. All `RESULT.json.parameters` values compare exactly equal to that snapshot. The receipt's source-check labels changed to report histogram equality and fixture sensitivity accurately. The finite source domains remain G≤3. + +The following Python 3.12 runs all exited 0. Commands, environment and final scientific-source hashes are in [logs/claude-validation.json](logs/claude-validation.json): + +| Check | Seconds | Output | +| --- | --- | --- | +| metadata | 0.282 | [log](logs/claude-metadata.log) | +| registered | 75.068 | [log](logs/claude-registered.log) | +| optimized | 14.372 | [log](logs/claude-optimized.log) | +| independent-optimized | 0.155 | [log](logs/claude-independent-optimized.log) | +| mutations-optimized | 30.389 | [log](logs/claude-mutations-optimized.log) | + +The registered replay now runs four commands, including the independent rational enclosure test. Normal and optimized oracle checks additionally passed in 28.674 s and 27.920 s with identical receipts; [timings](logs/claude-enclosures-timing.json), [normal receipt](logs/claude-enclosures-normal.json), [optimized receipt](logs/claude-enclosures-optimized.json). They cover 16 integer logarithm arguments and 127 distinct rational exponential arguments, and reject all three reported remainder faults. Their receipts identify the loaded verifier SHA and exact argument-domain digest. This independently certifies finite-domain enclosure containment, not all-input correctness or the asymptotic theorem. + +Both standalone source checkers now reject altered source bytes. Re-pinned empty and terminal-truncated source branches are rejected by the actual histogram comparisons, in normal and optimized modes. This separates source semantics from checksum failures and from fixture sensitivity. Fixed-root-bracket and corrupted-receipt controls remain separately labelled. + +The final internal review found no blocking issue in the updated proof, source binding, mutation tests or oracle mathematics. Primary numerical functions were compared by AST against the reviewed snapshot and are unchanged; only `finite_law` changed in verify.py. The oracle's last change adds the loaded source SHA to its receipt and was separately reviewed. README's final “adds eight”→“checks eight” wording avoids implying eighteen distinct source ranks; this prose-only change affects no evidence. + +The previously opened draft #6118's hosted run at `ff365dba` had a failed planning job and skipped replay. Its [actual job log](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40681403297/job/122792722146) reports two failures in `test_research_current_status`: the old selected-family CI text and an exact bold-value match. The shared files involved are unchanged from base. This is separate from the passing package replay; no unrelated suite or shared documentation repair was added here. Check the PR for the latest head's CI status. + +The current committed-byte/export/Git-free follow-up is recorded after execution below. diff --git a/research/direct-flow-leaf-saturation/VERIFY.json b/research/direct-flow-leaf-saturation/VERIFY.json index da746ca01f..a4ca4629cc 100644 --- a/research/direct-flow-leaf-saturation/VERIFY.json +++ b/research/direct-flow-leaf-saturation/VERIFY.json @@ -29,7 +29,7 @@ "{package}/independent_source.py" ], "timeout_seconds": 60, - "checks": "Ten independent ordered-word fixtures agree with PR4436 and PR4467 leaf histograms; wrong final truncation rejected." + "checks": "Ten independent ordered-word fixtures compare complete #4436 and #4467 leaf histograms after authenticating every input; terminal-cut fields describe fixture sensitivity." }, { "argv": [ @@ -38,7 +38,16 @@ "{package}/test_controls.py" ], "timeout_seconds": 120, - "checks": "Reject changed source bytes, altered histogram bracket, and corrupted expected receipt, including under optimized Python." + "checks": "Reject altered bytes in both standalone entry points; re-pinned empty/truncated source branches rejected semantically in normal and optimized modes; fixed-bracket and receipt regressions." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_enclosures.py" + ], + "timeout_seconds": 120, + "checks": "Independent exact rational bounds at every executed log/exp argument; reject zero logarithm/exponential tails and invalid exponential remainder majorant." } ] } diff --git a/research/direct-flow-leaf-saturation/independent_source.py b/research/direct-flow-leaf-saturation/independent_source.py index dca25cdad6..14c045c668 100644 --- a/research/direct-flow-leaf-saturation/independent_source.py +++ b/research/direct-flow-leaf-saturation/independent_source.py @@ -1,8 +1,14 @@ """Independent source audit. DLamdata with OpenAI Codex assistance; Apache-2.0.""" -import importlib.util, pathlib, collections, itertools, math, json +import importlib.util, pathlib, collections, itertools, math, json, hashlib ROOT=pathlib.Path(__file__).resolve().parents[2] def need(ok, message): if not ok: raise ValueError(message) +# Authenticate every declared live input before executing either predecessor. +# This is independent of the primary verifier and also works without Git. +manifest=json.loads((pathlib.Path(__file__).resolve().parent/'SOURCES.json').read_text()) +for row in manifest['files']: + if row['usage']=='input': + need(hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'], 'source mismatch: '+row['path']) def load(relative,name): s=importlib.util.spec_from_file_location(name,ROOT/relative);m=importlib.util.module_from_spec(s);s.loader.exec_module(m);return m old=load('research/direct-flow-leaf-walk/diagnostics/overlap_flow.py','audit_flow') @@ -25,8 +31,8 @@ def load(relative,name): actual=native.Flow(walk.W,walk.P,N).merged() other=actual['exits'].copy();other.subtract(actual['boundary_exits']);other=+other need(other==exact,(N,'original Flow class')) - # Incorrectly truncating the last unconditioned rank must change the leaf law. + # Fixture sensitivity only; the source checks are exact==leaf and other==exact above. wrong=collections.Counter({r:c for r,c in exact.items() if 121*r<=N}) - need(wrong!=exact,(N,'terminal truncation failure control')) - rows.append({'N':N,'G':G,'leaf_ranks':len(exact),'terminal_truncation_rejected':True}) + need(wrong!=exact,(N,'fixture does not distinguish terminal truncation')) + rows.append({'N':N,'G':G,'leaf_ranks':len(exact),'terminal_cut_distinguished':True}) print(json.dumps({'status':'PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION','fixtures':rows},indent=2)) diff --git a/research/direct-flow-leaf-saturation/logs/claude-enclosures-normal.json b/research/direct-flow-leaf-saturation/logs/claude-enclosures-normal.json new file mode 100644 index 0000000000..22b2ef62f1 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/claude-enclosures-normal.json @@ -0,0 +1,33 @@ +{ + "all_exp_arguments_below": "479/100", + "distinct_exp_rational_arguments": 127, + "domain_sha256": "5e27ec5fc8e5fe372d5511730fd47d3d9acac76ae707221b11bfa99b963c58e4", + "exp_oracle": "degree-82 positive series; exact ratio-bounded geometric tail", + "log_integer_arguments": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 16, + 25, + 32, + 41, + 48, + 57, + 121 + ], + "log_oracle": "256-term -log(1-q) series; exact positive geometric tail", + "mutations_rejected": [ + "zero_log_tail_at_log2", + "zero_exp_tail_at_exp1", + "invalid_exp_majorant_one_at_exp1" + ], + "production_source_sha256": "3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d", + "scope": "Exact containment at every argument captured from current parameters and controls; finite mutation discrimination, not a formal verifier or an all-input enclosure proof.", + "status": "PASS_INDEPENDENT_RATIONAL_ENCLOSURES" +} diff --git a/research/direct-flow-leaf-saturation/logs/claude-enclosures-optimized.json b/research/direct-flow-leaf-saturation/logs/claude-enclosures-optimized.json new file mode 100644 index 0000000000..22b2ef62f1 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/claude-enclosures-optimized.json @@ -0,0 +1,33 @@ +{ + "all_exp_arguments_below": "479/100", + "distinct_exp_rational_arguments": 127, + "domain_sha256": "5e27ec5fc8e5fe372d5511730fd47d3d9acac76ae707221b11bfa99b963c58e4", + "exp_oracle": "degree-82 positive series; exact ratio-bounded geometric tail", + "log_integer_arguments": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 16, + 25, + 32, + 41, + 48, + 57, + 121 + ], + "log_oracle": "256-term -log(1-q) series; exact positive geometric tail", + "mutations_rejected": [ + "zero_log_tail_at_log2", + "zero_exp_tail_at_exp1", + "invalid_exp_majorant_one_at_exp1" + ], + "production_source_sha256": "3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d", + "scope": "Exact containment at every argument captured from current parameters and controls; finite mutation discrimination, not a formal verifier or an all-input enclosure proof.", + "status": "PASS_INDEPENDENT_RATIONAL_ENCLOSURES" +} diff --git a/research/direct-flow-leaf-saturation/logs/claude-enclosures-timing.json b/research/direct-flow-leaf-saturation/logs/claude-enclosures-timing.json new file mode 100644 index 0000000000..0035686976 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/claude-enclosures-timing.json @@ -0,0 +1,14 @@ +[ + { + "mode": "normal", + "returncode": 0, + "elapsed_seconds": 28.674, + "max_rss_kib": 18612 + }, + { + "mode": "optimized", + "returncode": 0, + "elapsed_seconds": 27.92, + "max_rss_kib": 19620 + } +] diff --git a/research/direct-flow-leaf-saturation/logs/claude-independent-optimized.log b/research/direct-flow-leaf-saturation/logs/claude-independent-optimized.log new file mode 100644 index 0000000000..5f7f01fadc --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/claude-independent-optimized.log @@ -0,0 +1,65 @@ +{ + "status": "PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION", + "fixtures": [ + { + "N": 121, + "G": 0, + "leaf_ranks": 9, + "terminal_cut_distinguished": true + }, + { + "N": 604, + "G": 0, + "leaf_ranks": 9, + "terminal_cut_distinguished": true + }, + { + "N": 605, + "G": 1, + "leaf_ranks": 26, + "terminal_cut_distinguished": true + }, + { + "N": 606, + "G": 1, + "leaf_ranks": 26, + "terminal_cut_distinguished": true + }, + { + "N": 3024, + "G": 1, + "leaf_ranks": 30, + "terminal_cut_distinguished": true + }, + { + "N": 3025, + "G": 2, + "leaf_ranks": 55, + "terminal_cut_distinguished": true + }, + { + "N": 3026, + "G": 2, + "leaf_ranks": 55, + "terminal_cut_distinguished": true + }, + { + "N": 15124, + "G": 2, + "leaf_ranks": 65, + "terminal_cut_distinguished": true + }, + { + "N": 15125, + "G": 3, + "leaf_ranks": 98, + "terminal_cut_distinguished": true + }, + { + "N": 15126, + "G": 3, + "leaf_ranks": 98, + "terminal_cut_distinguished": true + } + ] +} diff --git a/research/direct-flow-leaf-saturation/logs/claude-metadata.log b/research/direct-flow-leaf-saturation/logs/claude-metadata.log new file mode 100644 index 0000000000..a6c9fb298a --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/claude-metadata.log @@ -0,0 +1 @@ +PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check) diff --git a/research/direct-flow-leaf-saturation/logs/claude-mutations-optimized.log b/research/direct-flow-leaf-saturation/logs/claude-mutations-optimized.log new file mode 100644 index 0000000000..4a287e277c --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/claude-mutations-optimized.log @@ -0,0 +1 @@ +PASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions diff --git a/research/direct-flow-leaf-saturation/logs/claude-optimized.log b/research/direct-flow-leaf-saturation/logs/claude-optimized.log new file mode 100644 index 0000000000..a799a944c4 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/claude-optimized.log @@ -0,0 +1,49 @@ +{ + "controls": { + "interval_domain_rejections": 3, + "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1" + }, + "finite_law": { + "ordered_word_max_depth": 3, + "source_check": "complete actual X-BX histogram equals ordered-word enumeration", + "terminal_cut_distinguishing_fixtures": 8, + "whole_flow_fixtures": 8 + }, + "parameters": { + "alpha": [ + "0.98981438244597", + "0.98981438244599" + ], + "drift_above_log5": [ + "0.016477707041", + "0.016477707042" + ], + "invoice_derivative_lower_bound_interval_0_99_to_1": [ + "211661.930309", + "211661.930310" + ], + "lambda": [ + "0.00749912850515", + "0.00749912850519" + ], + "mean_deficit_limit": [ + "133.34882837", + "133.34882838" + ], + "mean_leaf_depth_limit": [ + "136.51870330", + "136.51870331" + ], + "mean_log_rank": [ + "1.625915619475", + "1.625915619476" + ], + "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds", + "t_star": [ + "0.99731351095114", + "0.99731351095116" + ] + }, + "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.", + "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS" +} diff --git a/research/direct-flow-leaf-saturation/logs/claude-registered.log b/research/direct-flow-leaf-saturation/logs/claude-registered.log new file mode 100644 index 0000000000..0aeabff141 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/claude-registered.log @@ -0,0 +1,153 @@ +CHECK Exact rational root/drift/tilt/limit enclosures, eight whole-flow fixtures, lattice and domain failure controls; classical LLT proof is written, not machine-checked. +{ + "controls": { + "interval_domain_rejections": 3, + "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1" + }, + "finite_law": { + "ordered_word_max_depth": 3, + "source_check": "complete actual X-BX histogram equals ordered-word enumeration", + "terminal_cut_distinguishing_fixtures": 8, + "whole_flow_fixtures": 8 + }, + "parameters": { + "alpha": [ + "0.98981438244597", + "0.98981438244599" + ], + "drift_above_log5": [ + "0.016477707041", + "0.016477707042" + ], + "invoice_derivative_lower_bound_interval_0_99_to_1": [ + "211661.930309", + "211661.930310" + ], + "lambda": [ + "0.00749912850515", + "0.00749912850519" + ], + "mean_deficit_limit": [ + "133.34882837", + "133.34882838" + ], + "mean_leaf_depth_limit": [ + "136.51870330", + "136.51870331" + ], + "mean_log_rank": [ + "1.625915619475", + "1.625915619476" + ], + "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds", + "t_star": [ + "0.99731351095114", + "0.99731351095116" + ] + }, + "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.", + "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS" +} +CHECK Ten independent ordered-word fixtures compare complete #4436 and #4467 leaf histograms after authenticating every input; terminal-cut fields describe fixture sensitivity. +{ + "status": "PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION", + "fixtures": [ + { + "N": 121, + "G": 0, + "leaf_ranks": 9, + "terminal_cut_distinguished": true + }, + { + "N": 604, + "G": 0, + "leaf_ranks": 9, + "terminal_cut_distinguished": true + }, + { + "N": 605, + "G": 1, + "leaf_ranks": 26, + "terminal_cut_distinguished": true + }, + { + "N": 606, + "G": 1, + "leaf_ranks": 26, + "terminal_cut_distinguished": true + }, + { + "N": 3024, + "G": 1, + "leaf_ranks": 30, + "terminal_cut_distinguished": true + }, + { + "N": 3025, + "G": 2, + "leaf_ranks": 55, + "terminal_cut_distinguished": true + }, + { + "N": 3026, + "G": 2, + "leaf_ranks": 55, + "terminal_cut_distinguished": true + }, + { + "N": 15124, + "G": 2, + "leaf_ranks": 65, + "terminal_cut_distinguished": true + }, + { + "N": 15125, + "G": 3, + "leaf_ranks": 98, + "terminal_cut_distinguished": true + }, + { + "N": 15126, + "G": 3, + "leaf_ranks": 98, + "terminal_cut_distinguished": true + } + ] +} +CHECK Reject altered bytes in both standalone entry points; re-pinned empty/truncated source branches rejected semantically in normal and optimized modes; fixed-bracket and receipt regressions. +PASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions +CHECK Independent exact rational bounds at every executed log/exp argument; reject zero logarithm/exponential tails and invalid exponential remainder majorant. +{ + "all_exp_arguments_below": "479/100", + "distinct_exp_rational_arguments": 127, + "domain_sha256": "5e27ec5fc8e5fe372d5511730fd47d3d9acac76ae707221b11bfa99b963c58e4", + "exp_oracle": "degree-82 positive series; exact ratio-bounded geometric tail", + "log_integer_arguments": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 16, + 25, + 32, + 41, + 48, + 57, + 121 + ], + "log_oracle": "256-term -log(1-q) series; exact positive geometric tail", + "mutations_rejected": [ + "zero_log_tail_at_log2", + "zero_exp_tail_at_exp1", + "invalid_exp_majorant_one_at_exp1" + ], + "production_source_sha256": "3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d", + "scope": "Exact containment at every argument captured from current parameters and controls; finite mutation discrimination, not a formal verifier or an all-input enclosure proof.", + "status": "PASS_INDEPENDENT_RATIONAL_ENCLOSURES" +} +PASS_REGISTERED_RESEARCH_PACKAGE research/direct-flow-leaf-saturation outcome=completed diff --git a/research/direct-flow-leaf-saturation/logs/claude-validation.json b/research/direct-flow-leaf-saturation/logs/claude-validation.json new file mode 100644 index 0000000000..a83289ceb0 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/claude-validation.json @@ -0,0 +1,84 @@ +{ + "python": "3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]", + "platform": "Linux-6.18.55-x86_64-with-glibc2.41", + "reviewed_predecessor": "ff365dba6911ce615bec76e8d1f149faf1fe16ca", + "upstream": "721c03822c421b7f7fcbb2598993b947c4d88419", + "runs": [ + { + "name": "metadata", + "command": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/direct-flow-leaf-saturation", + "--check-only" + ], + "exit_code": 0, + "seconds": 0.282, + "log": "logs/claude-metadata.log" + }, + { + "name": "registered", + "command": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/direct-flow-leaf-saturation" + ], + "exit_code": 0, + "seconds": 75.068, + "log": "logs/claude-registered.log" + }, + { + "name": "optimized", + "command": [ + "python3.12", + "-B", + "-O", + "research/direct-flow-leaf-saturation/verify.py", + "--expect", + "research/direct-flow-leaf-saturation/RESULT.json" + ], + "exit_code": 0, + "seconds": 14.372, + "log": "logs/claude-optimized.log" + }, + { + "name": "independent-optimized", + "command": [ + "python3.12", + "-B", + "-O", + "research/direct-flow-leaf-saturation/independent_source.py" + ], + "exit_code": 0, + "seconds": 0.155, + "log": "logs/claude-independent-optimized.log" + }, + { + "name": "mutations-optimized", + "command": [ + "python3.12", + "-B", + "-O", + "research/direct-flow-leaf-saturation/test_controls.py" + ], + "exit_code": 0, + "seconds": 30.389, + "log": "logs/claude-mutations-optimized.log" + } + ], + "enclosure_agent_runs": "logs/claude-enclosures-timing.json", + "scientific_files_sha256": { + "PROOF.md": "09dc0d6fd22b5e502b812543ddf78395ab7deacc894cd52430709475acfb2978", + "verify.py": "3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d", + "RESULT.json": "d195c3fd5620bf2e64dc7d677c79ad52e780aefde9534d4e6a02a5ff1b9c9bdd", + "independent_source.py": "abe248ffc0012fdcb7a941c399cba0f5f943c006d86368553c1c3317442f5773", + "test_controls.py": "ff4e4b8b8a34416b6e93a32ab2afbdd3733ce6e730a0df51a946d47b4a3836a5", + "test_enclosures.py": "b92a75601ef676ab0b412395eb2ccaa52c8e802f89fe1fb2f3820cafa173aea4", + "SOURCES.json": "90997ec1be8cd8c3e588d71a349783b2f1696a224dc082749f3886bebd8c2c4a", + "VERIFY.json": "07b8cf8da544a3049f817664381b3d26b3c5e35454ce2e308cfa41a6f3e76663" + } +} diff --git a/research/direct-flow-leaf-saturation/test_controls.py b/research/direct-flow-leaf-saturation/test_controls.py index c9ecee0465..6b8c5a77ed 100644 --- a/research/direct-flow-leaf-saturation/test_controls.py +++ b/research/direct-flow-leaf-saturation/test_controls.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 """Mutation controls for the certificate boundary. DLamdata/Codex, Apache-2.0.""" +import hashlib import importlib.util import json from pathlib import Path @@ -21,11 +22,19 @@ def require_rejection(argv, cwd, needle): raise ValueError(f'control did not reject with {needle!r}: {run.returncode}, {run.stderr[-400:]}') +def repin(package, root, relative): + manifest = json.loads((package / 'SOURCES.json').read_text()) + for row in manifest['files']: + if row['path'] == relative: + row['sha256'] = hashlib.sha256((root / relative).read_bytes()).hexdigest() + (package / 'SOURCES.json').write_text(json.dumps(manifest)) + + with tempfile.TemporaryDirectory(prefix='leaf-saturation-controls-') as directory: root = Path(directory) package = root / 'research/direct-flow-leaf-saturation' package.mkdir(parents=True) - for name in ('verify.py', 'SOURCES.json', 'RESULT.json'): + for name in ('verify.py', 'independent_source.py', 'SOURCES.json', 'RESULT.json'): shutil.copy2(HERE / name, package / name) sources = json.loads((HERE / 'SOURCES.json').read_text()) for row in sources['files']: @@ -33,18 +42,46 @@ def require_rejection(argv, cwd, needle): target = root / row['path'] target.parent.mkdir(parents=True, exist_ok=True) shutil.copy2(ROOT / row['path'], target) - source = root / 'research/direct-flow-leaf-walk/verify.py' - original = source.read_bytes() - source.write_bytes(original + b'\n# corrupt-source control\n') - for mode in ([], ['-O']): - require_rejection([sys.executable, *mode, '-B', str(package / 'verify.py')], root, 'source mismatch') - source.write_bytes(original) + # Both standalone entry points must bind bytes before executing inputs. + for relative in ('research/direct-flow-leaf-walk/verify.py', 'research/direct-mixed-flow/flow.py'): + source = root / relative + original = source.read_bytes() + source.write_bytes(original + b'\n# corrupt-source control\n') + for script in ('verify.py', 'independent_source.py'): + for mode in ([], ['-O']): + require_rejection([sys.executable, *mode, '-B', str(package / script)], root, 'source mismatch: ' + relative) + source.write_bytes(original) + + # Exercise the actual source-histogram assertions. Re-pin mutant bytes so + # a checksum failure cannot masquerade as a semantic rejection. + relative = 'research/direct-flow-leaf-walk/diagnostics/overlap_flow.py' + source = root / relative + original = source.read_text() + branch = ' if d == G:\n add(X, rank, issued); continue' + if original.count(branch) != 1: + raise ValueError('source mutation anchor drift') + mutations = { + 'empty_leaf': ' if d == G:\n continue', + 'truncated_terminal': ' if d == G:\n if m * rank <= N: add(X, rank, issued)\n continue', + } + probe = "import runpy,sys; v=runpy.run_path(sys.argv[1]); v['finite_law'](*v['bindings']())" + for replacement in mutations.values(): + source.write_text(original.replace(branch, replacement)) + repin(package, root, relative) + for mode in ([], ['-O']): + require_rejection([sys.executable, *mode, '-B', '-c', probe, str(package / 'verify.py')], root, 'ordered words disagree with actual leaf exits') + require_rejection([sys.executable, *mode, '-B', str(package / 'independent_source.py')], root, 'leaf histogram') + source.write_text(original) + shutil.copy2(HERE / 'SOURCES.json', package / 'SOURCES.json') + expected = json.loads((package / 'RESULT.json').read_text()) expected['parameters']['lambda'][0] = '0.0' receipt = package / 'corrupt-result.json' receipt.write_text(json.dumps(expected)) require_rejection([sys.executable, '-O', '-B', str(package / 'verify.py'), '--expect', str(receipt)], root, 'expected receipt mismatch') +# These are regressions for this narrow pinned root bracket, not general +# coverage of enclosure arithmetic; test_enclosures.py checks that separately. for name in ('paid', 'target'): P, W, M = v.bindings() histogram = P if name == 'paid' else W @@ -56,4 +93,4 @@ def require_rejection(argv, cwd, needle): raise else: raise ValueError('changed histogram passed fixed root certificate: ' + name) -print('PASS_MUTATION_CONTROLS source_bytes_normal_and_optimized corrupted_receipt paid_and_target_count_plus_one') +print('PASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions') diff --git a/research/direct-flow-leaf-saturation/test_enclosures.py b/research/direct-flow-leaf-saturation/test_enclosures.py new file mode 100644 index 0000000000..61c01cdddf --- /dev/null +++ b/research/direct-flow-leaf-saturation/test_enclosures.py @@ -0,0 +1,170 @@ +#!/usr/bin/env python3 +"""Exact independent enclosure checks and discriminating remainder mutations. + +The logarithm oracle uses -log(1-q)=sum(q**k/k), rather than the primary +atanh series. After n=2**e*u, 1<=u<2, both log(2) and log(u) have q<=1/2. +For K=256 the positive remainder is at most +q**(K+1)/((K+1)*(1-q)). + +The exponential oracle sums through degree 82. Its first omitted term is +x**83/83!, and every subsequent term ratio is at most x/84<=5/84, so a +geometric series bounds its tail. This does not use the primary Lagrange +bound exp(x)<3**5. Both implementations still share the ordinary exponential +series and Python's exact Fraction arithmetic; these finite checks are not a +formal proof of either series or of all future inputs. + +Every successful log/exp argument in the primary parameters and controls is +checked. The domain is collected from that execution, not independently +inferred. Three mutations use smaller, explicitly named discriminating +fixtures; they do not rerun a mutated scientific certificate. + +Prepared for DLamdata with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction +from functools import lru_cache +from pathlib import Path +import hashlib +import json + +HERE = Path(__file__).resolve().parent +PRODUCTION = HERE / 'verify.py' +Q = Fraction + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load(source): + """Compile the actual source bytes, with no import bytecode-cache reuse.""" + namespace = {'__name__': 'enclosure_test_subject', '__file__': str(PRODUCTION)} + exec(compile(source, str(PRODUCTION), 'exec'), namespace) + return namespace + + +@lru_cache(None) +def log_oracle(n): + need(isinstance(n, int) and n >= 1, 'oracle positive integer log input') + e = n.bit_length() - 1 + u = Q(n, 1 << e) + + def minus_log_one_minus(q): + need(0 <= q <= Q(1, 2), 'oracle log range reduction') + term = Q(1) + lower = Q(0) + for k in range(1, 257): + term *= q + lower += term / k + remainder = term * q / (257 * (1 - q)) + return lower, lower + remainder + + lo2, hi2 = minus_log_one_minus(Q(1, 2)) + lou, hiu = minus_log_one_minus(1 - 1 / u) + return e * lo2 + lou, e * hi2 + hiu + + +@lru_cache(None) +def exp_oracle(x): + need(isinstance(x, Q) and 0 <= x <= 5, 'oracle rational exp domain [0,5]') + term = lower = Q(1) + for k in range(1, 83): + term *= x / k + lower += term + first_omitted = term * x / 83 + upper = lower + first_omitted / (1 - x / 84) + return lower, upper + + +def check_enclosure(kind, argument, production_interval, oracle_interval): + lo, hi = production_interval + oracle_lo, oracle_hi = oracle_interval + need(all(isinstance(x, Q) for x in (lo, hi, oracle_lo, oracle_hi)), + kind + ' arithmetic must remain exact Fraction') + need(lo <= oracle_lo <= oracle_hi <= hi, + kind + ' enclosure fails exact independent containment') + + +def actual_arguments(subject): + logs, exponentials = set(), set() + original_log, original_exp = subject['log_bounds'], subject['exp_point'] + + def track_log(n): + value = original_log(n) + logs.add(n) + return value + + def track_exp(x): + value = original_exp(x) + exponentials.add(x) + return value + + subject['log_bounds'], subject['exp_point'] = track_log, track_exp + P, W, M = subject['bindings']() + subject['parameters'](P, W, M) + subject['controls']() + # The full verifier's remaining finite_law function uses integer products + # and counts only; it makes no log_bounds or exp_point calls. + need(logs and exponentials, 'empty production argument coverage') + return logs, exponentials, original_log, original_exp + + +def reject_mutation(source, name, old, new, kind, argument): + need(source.count(old) == 1, 'mutation source anchor changed: ' + name) + mutated = load(source.replace(old, new)) + function = mutated['log_bounds' if kind == 'log' else 'exp_point'] + oracle = log_oracle if kind == 'log' else exp_oracle + try: + check_enclosure(kind, argument, function(argument), oracle(argument)) + except ValueError as error: + need(str(error) == kind + ' enclosure fails exact independent containment', + 'mutation rejected for an unrelated reason: ' + name) + return name + raise ValueError('remainder mutation escaped independent check: ' + name) + + +def main(): + source = PRODUCTION.read_text(encoding='utf-8') + subject = load(source) + logs, exponentials, production_log, production_exp = actual_arguments(subject) + for n in sorted(logs): + check_enclosure('log', n, production_log(n), log_oracle(n)) + for x in sorted(exponentials): + check_enclosure('exp', x, production_exp(x), exp_oracle(x)) + # Known exact endpoints also guard the oracle's zero cases. + need(log_oracle(1) == (Q(0), Q(0)) and exp_oracle(Q(0)) == (Q(1), Q(1)), + 'independent oracle identity fixtures') + mutations = [ + reject_mutation(source, 'zero_log_tail_at_log2', + ' return total, total + tail', + ' return total, total', 'log', 2), + reject_mutation(source, 'zero_exp_tail_at_exp1', + 'tail = Q(3 ** 5) * term * x / 81', + 'tail = Q(0)', 'exp', Q(1)), + reject_mutation(source, 'invalid_exp_majorant_one_at_exp1', + 'tail = Q(3 ** 5) * term * x / 81', + 'tail = Q(1) * term * x / 81', 'exp', Q(1)), + ] + need(max(exponentials) < Q(479, 100), 'actual exp argument ceiling changed') + # A deterministic domain digest records exact argument coverage without + # printing the large rational numerators/denominators. + domain = json.dumps({'log': sorted(logs), + 'exp': [[str(x.numerator), str(x.denominator)] + for x in sorted(exponentials)]}, + sort_keys=True, separators=(',', ':')).encode() + print(json.dumps({ + 'status': 'PASS_INDEPENDENT_RATIONAL_ENCLOSURES', + 'production_source_sha256': hashlib.sha256(source.encode('utf-8')).hexdigest(), + 'log_integer_arguments': sorted(logs), + 'distinct_exp_rational_arguments': len(exponentials), + 'all_exp_arguments_below': '479/100', + 'domain_sha256': hashlib.sha256(domain).hexdigest(), + 'log_oracle': '256-term -log(1-q) series; exact positive geometric tail', + 'exp_oracle': 'degree-82 positive series; exact ratio-bounded geometric tail', + 'mutations_rejected': mutations, + 'scope': 'Exact containment at every argument captured from current parameters and controls; finite mutation discrimination, not a formal verifier or an all-input enclosure proof.' + }, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/direct-flow-leaf-saturation/verify.py b/research/direct-flow-leaf-saturation/verify.py index b5007aadb8..83d2cd9276 100644 --- a/research/direct-flow-leaf-saturation/verify.py +++ b/research/direct-flow-leaf-saturation/verify.py @@ -152,7 +152,7 @@ def finite_law(P, W, M): # Independent ordered-word enumeration vs the predecessor's whole-flow X-BX. flow = runpy.run_path(str(ROOT / 'research/direct-flow-leaf-walk/diagnostics/overlap_flow.py'))['flow'] count = 0 - extra_truncation_detected = False + terminal_cut_distinguishing_fixtures = 0 for G in range(4): for N in (M * 5 ** G, M * 5 ** G + M * 5 ** G // 2): got = flow(N, W, P) @@ -171,14 +171,14 @@ def finite_law(P, W, M): wrong[e] = wrong.get(e, 0) + multiplicity * pr actual = {e: c - got['BX'].get(e, 0) for e, c in got['X'].items() if c != got['BX'].get(e, 0)} need(actual == leaves, 'ordered words disagree with actual leaf exits') - # At t=1, the weighted final-r distribution factorizes exactly. - leaf_mass = sum(e * c for e, c in leaves.items()) - need(leaf_mass == sum(rho * c for rho, c in prefixes.items()) * sum(r * c for r, c in P.items()), 'independent terminal rank') - extra_truncation_detected |= wrong != actual + # This checks fixture sensitivity, not an additional source identity. + # Source coverage is the complete actual==leaves comparison above. + terminal_cut_distinguishing_fixtures += wrong != leaves count += 1 - need(extra_truncation_detected, 'extra-terminal-truncation control did not discriminate') + need(terminal_cut_distinguishing_fixtures > 0, 'no fixture distinguishes terminal truncation') return {'whole_flow_fixtures': count, 'ordered_word_max_depth': 3, - 'extra_terminal_truncation': 'rejected'} + 'terminal_cut_distinguishing_fixtures': terminal_cut_distinguishing_fixtures, + 'source_check': 'complete actual X-BX histogram equals ordered-word enumeration'} def controls(): From 6310550e932de70243fc2aaab6f4885688b6fe21 Mon Sep 17 00:00:00 2001 From: Figo Lam Date: Wed, 28 Oct 2026 12:35:26 +0000 Subject: [PATCH 4/7] Record reviewed export replay and model attribution --- .../CLAUDE-RESPONSE.md | 2 +- .../direct-flow-leaf-saturation/README.md | 2 +- .../direct-flow-leaf-saturation/VALIDATION.md | 15 ++++- .../logs/claude-portable-0.log | 49 ++++++++++++++ .../logs/claude-portable-1.log | 65 +++++++++++++++++++ .../logs/claude-portable-2.log | 1 + .../logs/claude-portable-3.log | 33 ++++++++++ .../logs/claude-portable-results.json | 49 ++++++++++++++ 8 files changed, 213 insertions(+), 3 deletions(-) create mode 100644 research/direct-flow-leaf-saturation/logs/claude-portable-0.log create mode 100644 research/direct-flow-leaf-saturation/logs/claude-portable-1.log create mode 100644 research/direct-flow-leaf-saturation/logs/claude-portable-2.log create mode 100644 research/direct-flow-leaf-saturation/logs/claude-portable-3.log create mode 100644 research/direct-flow-leaf-saturation/logs/claude-portable-results.json diff --git a/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md b/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md index 0a550225ae..428760199c 100644 --- a/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md +++ b/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md @@ -1,6 +1,6 @@ # Response to the Claude Code review of ff365dba -The review examined `ff365dba6911ce615bec76e8d1f149faf1fe16ca` and confirmed the scoped theorem and numerical enclosures. This response preserves that theorem, its fixed raw-p7 scope and all parameter values. Claude Code and the follow-up Codex reviewers are AI reviewers, not independent human or formal verification. +The review examined `ff365dba6911ce615bec76e8d1f149faf1fe16ca` and confirmed the scoped theorem and numerical enclosures. This response preserves that theorem, its fixed raw-p7 scope and all parameter values. Claude Code (Opus 5.5) and the follow-up OpenAI Codex (GPT-6 Astra) reviewers are AI reviewers, not independent human or formal verification. | Finding | Resolution | Evidence and limit | | --- | --- | --- | diff --git a/research/direct-flow-leaf-saturation/README.md b/research/direct-flow-leaf-saturation/README.md index 1fe9048298..81d1d51daa 100644 --- a/research/direct-flow-leaf-saturation/README.md +++ b/research/direct-flow-leaf-saturation/README.md @@ -48,4 +48,4 @@ The main certificate uses `Fraction` intervals throughout: a 48-term `2 atanh(z) Structured questions are in [TASK.json](TASK.json). No wider construction search is justified by this package alone. -Prepared for DLamdata with substantial OpenAI Codex assistance, including two separate AI agents for independent mathematical/source checks and skeptical review. This is not independent human review, formal verification, or maintainer acceptance. Predecessor credit and Apache-2.0 licensing are retained. +Prepared for DLamdata with substantial OpenAI Codex (GPT-6 Astra) assistance, including two separate AI agents for independent mathematical/source checks and skeptical review. Claude Code (Opus 5.5) reviewed the initial published snapshot; its findings and the response are recorded in CLAUDE-RESPONSE.md. This is not independent human review, formal verification, or maintainer acceptance. Predecessor credit and Apache-2.0 licensing are retained. diff --git a/research/direct-flow-leaf-saturation/VALIDATION.md b/research/direct-flow-leaf-saturation/VALIDATION.md index 926c9bb3af..7e41da759a 100644 --- a/research/direct-flow-leaf-saturation/VALIDATION.md +++ b/research/direct-flow-leaf-saturation/VALIDATION.md @@ -73,4 +73,17 @@ The final internal review found no blocking issue in the updated proof, source b The previously opened draft #6118's hosted run at `ff365dba` had a failed planning job and skipped replay. Its [actual job log](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40681403297/job/122792722146) reports two failures in `test_research_current_status`: the old selected-family CI text and an exact bold-value match. The shared files involved are unchanged from base. This is separate from the passing package replay; no unrelated suite or shared documentation repair was added here. Check the PR for the latest head's CI status. -The current committed-byte/export/Git-free follow-up is recorded after execution below. +## Claude-review response: committed export and Git-free replay + +Scientific follow-up commit: `553198839618962e07519b51cb3bbe808ca6f1dc`. Committed-byte comparison with `--check-source-history` passed for all 41 package/input files, with the original base as the source-history ancestor. The official exporter and archive check both reported `PASS_RESEARCH_EXPORT` for those 41 files: + +```sh +python3.12 -B scripts/check_research_commit.py --package research/direct-flow-leaf-saturation --check-source-history +python3.12 -B scripts/export_research_package.py export --package research/direct-flow-leaf-saturation --ref 553198839618962e07519b51cb3bbe808ca6f1dc --output /tmp/leaf-saturation-reviewed.tar +python3.12 -B scripts/export_research_package.py check /tmp/leaf-saturation-reviewed.tar +``` + +The archive was extracted into a fresh directory, using an absolute Python 3.12 executable with PATH set to an empty directory and no Git available. All four direct commands passed: primary certificate 15.962 s, independent source checker 0.090 s, mutation controls 31.220 s, and independent enclosure checks 28.117 s. [logs/claude-portable-results.json](logs/claude-portable-results.json) records exact commands, exit codes and links to their logs. The scientific bytes are exactly the commit above; the subsequent evidence commit adds only these logs, this validation record and model attribution. Final publication-byte and export checks are repeated after that evidence commit. + + +Pre-publication refresh at 2026-10-28T12:34:31Z found canonical main unchanged at `721c03822c421b7f7fcbb2598993b947c4d88419` and no guidance/priority change. A bounded live check of the 100 most recently updated PRs (all states) and 100 Discussions reached back to October 28 00:24Z and October 25 03:58Z respectively, overlapping the earlier complete body snapshots. Exact predecessor and saturation-term checks found no new competing saturation result; this is body-level coverage, not a claim to have reviewed every diff or reply. Existing #6118 was confirmed open and draft before the update. diff --git a/research/direct-flow-leaf-saturation/logs/claude-portable-0.log b/research/direct-flow-leaf-saturation/logs/claude-portable-0.log new file mode 100644 index 0000000000..a799a944c4 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/claude-portable-0.log @@ -0,0 +1,49 @@ +{ + "controls": { + "interval_domain_rejections": 3, + "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1" + }, + "finite_law": { + "ordered_word_max_depth": 3, + "source_check": "complete actual X-BX histogram equals ordered-word enumeration", + "terminal_cut_distinguishing_fixtures": 8, + "whole_flow_fixtures": 8 + }, + "parameters": { + "alpha": [ + "0.98981438244597", + "0.98981438244599" + ], + "drift_above_log5": [ + "0.016477707041", + "0.016477707042" + ], + "invoice_derivative_lower_bound_interval_0_99_to_1": [ + "211661.930309", + "211661.930310" + ], + "lambda": [ + "0.00749912850515", + "0.00749912850519" + ], + "mean_deficit_limit": [ + "133.34882837", + "133.34882838" + ], + "mean_leaf_depth_limit": [ + "136.51870330", + "136.51870331" + ], + "mean_log_rank": [ + "1.625915619475", + "1.625915619476" + ], + "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds", + "t_star": [ + "0.99731351095114", + "0.99731351095116" + ] + }, + "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.", + "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS" +} diff --git a/research/direct-flow-leaf-saturation/logs/claude-portable-1.log b/research/direct-flow-leaf-saturation/logs/claude-portable-1.log new file mode 100644 index 0000000000..5f7f01fadc --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/claude-portable-1.log @@ -0,0 +1,65 @@ +{ + "status": "PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION", + "fixtures": [ + { + "N": 121, + "G": 0, + "leaf_ranks": 9, + "terminal_cut_distinguished": true + }, + { + "N": 604, + "G": 0, + "leaf_ranks": 9, + "terminal_cut_distinguished": true + }, + { + "N": 605, + "G": 1, + "leaf_ranks": 26, + "terminal_cut_distinguished": true + }, + { + "N": 606, + "G": 1, + "leaf_ranks": 26, + "terminal_cut_distinguished": true + }, + { + "N": 3024, + "G": 1, + "leaf_ranks": 30, + "terminal_cut_distinguished": true + }, + { + "N": 3025, + "G": 2, + "leaf_ranks": 55, + "terminal_cut_distinguished": true + }, + { + "N": 3026, + "G": 2, + "leaf_ranks": 55, + "terminal_cut_distinguished": true + }, + { + "N": 15124, + "G": 2, + "leaf_ranks": 65, + "terminal_cut_distinguished": true + }, + { + "N": 15125, + "G": 3, + "leaf_ranks": 98, + "terminal_cut_distinguished": true + }, + { + "N": 15126, + "G": 3, + "leaf_ranks": 98, + "terminal_cut_distinguished": true + } + ] +} diff --git a/research/direct-flow-leaf-saturation/logs/claude-portable-2.log b/research/direct-flow-leaf-saturation/logs/claude-portable-2.log new file mode 100644 index 0000000000..4a287e277c --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/claude-portable-2.log @@ -0,0 +1 @@ +PASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions diff --git a/research/direct-flow-leaf-saturation/logs/claude-portable-3.log b/research/direct-flow-leaf-saturation/logs/claude-portable-3.log new file mode 100644 index 0000000000..22b2ef62f1 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/claude-portable-3.log @@ -0,0 +1,33 @@ +{ + "all_exp_arguments_below": "479/100", + "distinct_exp_rational_arguments": 127, + "domain_sha256": "5e27ec5fc8e5fe372d5511730fd47d3d9acac76ae707221b11bfa99b963c58e4", + "exp_oracle": "degree-82 positive series; exact ratio-bounded geometric tail", + "log_integer_arguments": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 16, + 25, + 32, + 41, + 48, + 57, + 121 + ], + "log_oracle": "256-term -log(1-q) series; exact positive geometric tail", + "mutations_rejected": [ + "zero_log_tail_at_log2", + "zero_exp_tail_at_exp1", + "invalid_exp_majorant_one_at_exp1" + ], + "production_source_sha256": "3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d", + "scope": "Exact containment at every argument captured from current parameters and controls; finite mutation discrimination, not a formal verifier or an all-input enclosure proof.", + "status": "PASS_INDEPENDENT_RATIONAL_ENCLOSURES" +} diff --git a/research/direct-flow-leaf-saturation/logs/claude-portable-results.json b/research/direct-flow-leaf-saturation/logs/claude-portable-results.json new file mode 100644 index 0000000000..4575d9dc68 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/claude-portable-results.json @@ -0,0 +1,49 @@ +{ + "export_commit": "553198839618962e07519b51cb3bbe808ca6f1dc", + "git_available": false, + "path": "empty directory", + "runs": [ + { + "command": [ + "python3.12", + "-B", + "research/direct-flow-leaf-saturation/verify.py", + "--expect", + "research/direct-flow-leaf-saturation/RESULT.json" + ], + "exit_code": 0, + "seconds": 15.962, + "log": "logs/claude-portable-0.log" + }, + { + "command": [ + "python3.12", + "-B", + "research/direct-flow-leaf-saturation/independent_source.py" + ], + "exit_code": 0, + "seconds": 0.09, + "log": "logs/claude-portable-1.log" + }, + { + "command": [ + "python3.12", + "-B", + "research/direct-flow-leaf-saturation/test_controls.py" + ], + "exit_code": 0, + "seconds": 31.22, + "log": "logs/claude-portable-2.log" + }, + { + "command": [ + "python3.12", + "-B", + "research/direct-flow-leaf-saturation/test_enclosures.py" + ], + "exit_code": 0, + "seconds": 28.117, + "log": "logs/claude-portable-3.log" + } + ] +} From 9946b1c42466ada889c10cd0cea7522d6360a63b Mon Sep 17 00:00:00 2001 From: Figo Lam Date: Wed, 28 Oct 2026 12:57:05 +0000 Subject: [PATCH 5/7] Clarify leaf-saturation reading path and current evidence --- .../CLAUDE-RESPONSE.md | 33 +---- .../direct-flow-leaf-saturation/README.md | 63 ++++---- .../direct-flow-leaf-saturation/REVIEW.md | 61 +++++--- .../direct-flow-leaf-saturation/VALIDATION.md | 134 ++++++++++++------ 4 files changed, 171 insertions(+), 120 deletions(-) diff --git a/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md b/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md index 428760199c..9d75e0da62 100644 --- a/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md +++ b/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md @@ -1,32 +1,5 @@ -# Response to the Claude Code review of ff365dba +# Claude Code review response -The review examined `ff365dba6911ce615bec76e8d1f149faf1fe16ca` and confirmed the scoped theorem and numerical enclosures. This response preserves that theorem, its fixed raw-p7 scope and all parameter values. Claude Code (Opus 5.5) and the follow-up OpenAI Codex (GPT-6 Astra) reviewers are AI reviewers, not independent human or formal verification. +The six findings from Claude Code (Opus 5.5)'s review of `ff365dba6911ce615bec76e8d1f149faf1fe16ca`, their resolutions, and the follow-up OpenAI Codex (GPT-6 Astra) review are consolidated in [REVIEW.md](REVIEW.md#claude-review-findings). -| Finding | Resolution | Evidence and limit | -| --- | --- | --- | -| 1. Stone statement and uniformity need precise citation | PROOF.md §3 now names Corollary 1 (7), Theorem (5) and footnote 2; gives the normalization/rescaling and characteristic-function/support equivalence. | Fixed-x (12) is explicitly not the source of uniform concentration. The review reports checking the primary paper; the follow-up internal proof review corroborated the uniform form from Stone's later text but did not retrieve the original afresh. Stronger nonlattice rate hypotheses fail for finite support; this does not exclude quantitative rates by other methods. | -| 2. Terminal-rank flags overstate coverage | Removed the redundant self-factorization assertion; renamed flags as fixture sensitivity. The source identity is the complete histogram comparison. | `test_controls.py` actually empties or truncates the source leaf branch in a temporary tree, re-pins the mutant bytes, and requires semantic rejection by both source-law entry points, normally and under `-O`. A checksum failure cannot count as this semantic rejection. | -| 3. Remainder bounds lack discriminating controls | Added `test_enclosures.py`, an exact-rational independent enclosure oracle. | It checks every successful log/exp argument captured from current `parameters()` and `controls()`. Logarithms use a different series; exponentials use a positive-series geometric tail rather than the primary Lagrange bound. Zero logarithm/exponential tails and the invalid majorant 1 are rejected at explicit fixtures even though the old rounded receipt did not distinguish them. | -| 4. Standalone independent source checker lacks byte binding | `independent_source.py` authenticates every declared live input before any predecessor import. | Comment-only mutations to both predecessor verifier and original flow are rejected by both standalone entry points in normal and optimized modes. No Git is needed. | -| 5. Executable source domain ends at G≤3 | Retained and explicitly scoped; no unnecessary search expansion. | The source proof is for every G, while the local primary/independent fixtures remain eight/ten checks through G=3. Claude reported further G=4–5 corroboration; this package does not present that as a newly executed local check. | -| 6. Leaf observable lacks an explicit formula | PROOF.md §1 now defines the normalized potential-weighted sum over `X−BX`, and its equivalent sum with weights `F[G][ρ] P_r (rρ)^t`. | The final rank uses the full paid inventory and both denominators are positive. The limit is unchanged. | - -## What the new controls do not prove - -The remainder oracle certifies containment on the captured finite argument domain. Both implementations still share Python's exact rational arithmetic and the exponential series; the logarithm series and exponential remainder arguments differ. This is not formal verification or a proof of the routines for arbitrary future inputs. Its domain digest and loaded verifier SHA identify the checked inputs and code. - -The +1 histogram mutations are regressions for the fixed narrow root bracket, not general tests of interval arithmetic. The derivative-bound endpoint ordering is justified by the written monotonicity argument and code review; a changed printed derivative is also caught by the expected receipt. The new enclosure tests do not claim to independently prove that derivative formula. - -The source mutation controls exercise the complete histogram equality checks. A flag saying that a fixture has an exit above N/121 only describes its ability to distinguish truncation; it does not independently authenticate or validate a source implementation. - -The registered runner still declares Python 3.12. README commands now explicitly select `python3.12` to avoid a default `python3` selecting 3.13 and failing that version gate. No dependency or runner policy is changed. - -## Reproduce the response - -```sh -python3.12 -B scripts/research_package.py --package research/direct-flow-leaf-saturation -python3.12 -O -B research/direct-flow-leaf-saturation/test_controls.py -python3.12 -O -B research/direct-flow-leaf-saturation/test_enclosures.py -``` - -[VALIDATION.md](VALIDATION.md) records the actual runs, source hashes and portable replay. The full-flow ceiling, finite-depth rates, stable shares, and supplier admission remain open. The selected #6030 record is unchanged. +Use [the current evidence index](VALIDATION.md#current-evidence-index) for checked source hashes, commands and receipts. The theorem and numerical bounds are unchanged. This file preserves existing links; REVIEW.md is the authoritative review record. All reviews are AI reviews, not human or formal verification. diff --git a/research/direct-flow-leaf-saturation/README.md b/research/direct-flow-leaf-saturation/README.md index 81d1d51daa..af9afeb32c 100644 --- a/research/direct-flow-leaf-saturation/README.md +++ b/research/direct-flow-leaf-saturation/README.md @@ -1,51 +1,52 @@ # The fixed #4467 leaf deficit saturates, uniformly across lockstep levels -This package proves the saturation predicted by Ryanson Jonathan / pinterbanget's [#4467](https://github.com/CrocSwap/integer-mult-bounds/pull/4467). For its fixed raw-p7 paid-rank law, the conditional deficit `B_G−S_G` converges to `Exp(λ)`, **including convergence of the mean**, uniformly for `B_G=G log5+δ`, `0≤δ Date: Wed, 28 Oct 2026 13:43:08 +0000 Subject: [PATCH 6/7] Correct Stone refinement wording and guard original-flow comparison --- .../CLAUDE-RESPONSE.md | 2 +- research/direct-flow-leaf-saturation/PROOF.md | 2 +- .../direct-flow-leaf-saturation/README.md | 6 +- .../direct-flow-leaf-saturation/REVIEW.md | 27 ++- .../direct-flow-leaf-saturation/VALIDATION.md | 35 ++-- .../direct-flow-leaf-saturation/VERIFY.json | 2 +- .../logs/followup-validation.json | 159 ++++++++++++++++++ .../test_controls.py | 19 ++- 8 files changed, 223 insertions(+), 29 deletions(-) create mode 100644 research/direct-flow-leaf-saturation/logs/followup-validation.json diff --git a/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md b/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md index 9d75e0da62..814323fd93 100644 --- a/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md +++ b/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md @@ -1,5 +1,5 @@ # Claude Code review response -The six findings from Claude Code (Opus 5.5)'s review of `ff365dba6911ce615bec76e8d1f149faf1fe16ca`, their resolutions, and the follow-up OpenAI Codex (GPT-6 Astra) review are consolidated in [REVIEW.md](REVIEW.md#claude-review-findings). +The initial Claude Code (Opus 5.5) review of `ff365dba6911ce615bec76e8d1f149faf1fe16ca`, its follow-up at `6310550e932de70243fc2aaab6f4885688b6fe21`, and the OpenAI Codex (GPT-6 Astra) responses are consolidated in [REVIEW.md](REVIEW.md). Use [the current evidence index](VALIDATION.md#current-evidence-index) for checked source hashes, commands and receipts. The theorem and numerical bounds are unchanged. This file preserves existing links; REVIEW.md is the authoritative review record. All reviews are AI reviews, not human or formal verification. diff --git a/research/direct-flow-leaf-saturation/PROOF.md b/research/direct-flow-leaf-saturation/PROOF.md index 9e0a493dcc..6d8ed0c657 100644 --- a/research/direct-flow-leaf-saturation/PROOF.md +++ b/research/direct-flow-leaf-saturation/PROOF.md @@ -71,7 +71,7 @@ Apply it to the tilted law `q(r)=P_r r^α/Z(α)`, with `V=log r−a`. Its mean i This support argument verifies Stone's characteristic-function condition (2). Indeed, for `θ≠0`, equality `|E exp(iθV)|=1` holds exactly when the unit complex variable `exp(iθV)` is almost surely constant, equivalently when the support lies in `c/θ+(2π/θ)Z` for some real `c`. Thus nonlattice support gives strict inequality for every nonzero `θ`. -The finite support does **not** satisfy Stone's stronger condition (3): simultaneous approximation of its finitely many phases gives arbitrarily large `|θ|` for which the characteristic-function modulus approaches one. Stone's stronger rate conclusion requiring that condition is therefore inapplicable here. The asymptotic theorem used in this proof supplies no explicit error constant or onset `G`; this does not rule out quantitative bounds from other methods. +The finite support does **not** satisfy Stone's stronger condition (3): simultaneous approximation of its finitely many phases gives arbitrarily large `|θ|` for which the characteristic-function modulus approaches one. Under that condition, Stone's equations (6) and (8) extend the local-limit statement to boxes as small as `exp(−cn)` for a suitable `c>0`; their remainder is still an unquantified `o(1)`. Neither equation is used here. Our proof uses equations (5) and (7) for fixed unnormalized windows. Neither cited version supplies an explicit quantitative convergence rate, error constant or onset `G`; failure of condition (3) is not the explanation for this missing quantitative information. Such bounds require additional work and are not ruled out by this argument. Two consequences are used: diff --git a/research/direct-flow-leaf-saturation/README.md b/research/direct-flow-leaf-saturation/README.md index af9afeb32c..bf1ce2a4c5 100644 --- a/research/direct-flow-leaf-saturation/README.md +++ b/research/direct-flow-leaf-saturation/README.md @@ -31,7 +31,7 @@ This runs all four registered checks serially; the recorded run took about **75 | Conditional distribution and mean converge uniformly over offsets | [Written proof](PROOF.md), using Stone's interval local-limit theorem and a uniform expectation-tail bound | Classical theorem is an external dependency; no effective finite-G rate. | | Root, tilt and limiting mean lie in the stated intervals | [verify.py](verify.py) and [RESULT.json](RESULT.json), using exact rational enclosures | Certifies this fixed source law, not a new supplier or multiplication bound. | | The source emits G conditioned ranks and an unconditioned terminal rank | All-G source reading in [PROOF.md §2](PROOF.md#2-why-this-is-the-sources-measure); eight primary and ten independent complete-histogram fixtures against #4467 and #4436 | Fixtures overlap and stop at G=3; they corroborate the derivation rather than exhaust all G. | -| Specified source faults are rejected | [test_controls.py](test_controls.py): changed-byte checks plus re-pinned empty/truncated source branches, normal and optimized | Semantic rejection comes from the actual histogram comparisons; terminal-cut flags describe fixture sensitivity only. | +| Specified source faults are rejected | [test_controls.py](test_controls.py): changed-byte checks plus re-pinned empty/truncated #4467 branches and an altered #4436 returned histogram, normal and optimized | Semantic rejection comes from the actual histogram comparisons; terminal-cut flags describe fixture sensitivity only. | | Numerical enclosures contain independent bounds on the executed domain | [test_enclosures.py](test_enclosures.py): 16 log and 127 exp arguments; three targeted remainder faults rejected | Finite captured domain; shared exact arithmetic and exponential series, not all-input formal verification. | The numerical certificate uses a 48-term `2 atanh(z)` series with a geometric tail for logarithms, and an 80-term exponential series with the Lagrange majorant `3^5` on `[0,5]`. The independent checker uses a different logarithm series and a geometric exponential-tail bound. Root isolation uses endpoint signs and a derivative lower bound; tilt uniqueness uses positive variance. Decimals are rounded outward; no predecessor floating-point root finder or data fit supplies the certificate. A lattice countermodel demonstrates the need for nonlattice support; the certificate also checks positive drift and rejects invalid interval-operation inputs. @@ -44,9 +44,11 @@ The original direct flow is zxv's #4436 (`56003680aee2871773de408e5f01cc5dd46b14 ## Open next questions -1. **Give a certified finite-G error bound.** Start by obtaining an effective interval local-limit estimate for this fixed tilted log-rank law, then combine it with the weighted-tail decomposition in PROOF.md §4. A useful result would give explicit constants and an onset for the conditional mean error, uniformly over the level offset. The present proof's concentration constant and onset are existential; Stone's stronger rate hypothesis fails for this finite support, so it cannot simply be substituted. Reuse the pinned law, tilt enclosure and tail decomposition, but review and certify any new quantitative estimates. +1. **Give a certified finite-G error bound.** Start by obtaining an effective interval local-limit estimate for this fixed tilted log-rank law, then combine it with the weighted-tail decomposition in PROOF.md §4. A useful result would give explicit constants and an onset for the conditional mean error, uniformly over the level offset. The present proof's concentration constant and onset are existential. Stone's stronger nonlattice refinements extend the allowed box sizes, but still provide no quantified remainder; their failure for finite support does not explain the missing error rate. Reuse the pinned law, tilt enclosure and tail decomposition, but review and certify any new quantitative estimates. 2. **Analyze the other flow components and the exact induction ratio.** Start from #4436's source and boundary sums at the same bounded level offset, retaining all terms. A useful first result would be a source-bound formula or bound for one component's normalized potential contribution, with any offset dependence explicit. Stable shares and the exact-ratio asymptotic remain blockers to a whole-flow ceiling; the leaf limit alone supplies neither. Reuse the source pins and leaf identity, not the predecessor's heuristic total ceiling. +Related pending work by Nick Petalas: [#6125](https://github.com/CrocSwap/integer-mult-bounds/pull/6125) (`f58e29052a0bbb4e123ea777b5e03321fde6f31f`) extends this framework to three power-tariff regimes; [#6128](https://github.com/CrocSwap/integer-mult-bounds/pull/6128) (`9be0bd96279cd66098a9d536ffd0092fd771550a`) reports an explicit finite-depth tail envelope and clipping bound. Both cite our `6310550e` scientific snapshot. These descriptions were checked, but their proofs and certificates were not audited here. A continuation should assess that work before duplicating it; a decreasing convergence-error estimate remains open in both descriptions. + Structured questions are in [TASK.json](TASK.json). A wider construction search needs a separate justification under the repository's family-expansion gate. Prepared for DLamdata with substantial OpenAI Codex (GPT-6 Astra) assistance, including separate agents for independent mathematical/source checks and skeptical review. Claude Code (Opus 5.5) reviewed the initial published snapshot; [REVIEW.md](REVIEW.md) records its findings and the response. These are AI reviews, not human or formal verification or maintainer acceptance. Predecessor credit and Apache-2.0 licensing are retained. diff --git a/research/direct-flow-leaf-saturation/REVIEW.md b/research/direct-flow-leaf-saturation/REVIEW.md index e9a591bb0e..4993b9e5d3 100644 --- a/research/direct-flow-leaf-saturation/REVIEW.md +++ b/research/direct-flow-leaf-saturation/REVIEW.md @@ -2,18 +2,28 @@ ## Current review status -The current scientific files are those at `553198839618962e07519b51cb3bbe808ca6f1dc`, with their hashes and replay receipts indexed in [VALIDATION.md](VALIDATION.md#current-evidence-index). Subsequent changes record evidence, attribution and reading guidance. The scoped theorem and every numerical parameter interval are unchanged from the initial published snapshot `ff365dba6911ce615bec76e8d1f149faf1fe16ca`. +Current source hashes and checks are indexed in [VALIDATION.md](VALIDATION.md#current-evidence-index). The follow-up review of `6310550e932de70243fc2aaab6f4885688b6fe21` was applied to `9946b1c42466ada889c10cd0cea7522d6360a63b`, whose intervening changes were documentation only. This response corrects one Stone paragraph and adds a control for the original #4436 comparison. The theorem, its argument, all numerical results and pinned predecessor inputs are unchanged. -Claude Code (Opus 5.5) reviewed that initial snapshot, confirmed the scoped theorem and numerical enclosures, and reported checking Stone's primary text. The six findings and their resolutions below are the canonical review record. Follow-up OpenAI Codex (GPT-6 Astra) review found no unresolved blocker in the integrated response. These are AI reviews, not independent human review, proof-kernel verification or maintainer acceptance. +Claude Code (Opus 5.5) reviewed both the initial `ff365dba6911ce615bec76e8d1f149faf1fe16ca` snapshot and the response at `6310550e`. Its follow-up confirmed findings 1, 2, 3, 4 and 6 were resolved except for the Stone wording below; finding 5 remains a disclosed coverage limit. The six findings and follow-up resolutions below are the canonical review record. OpenAI Codex (GPT-6 Astra) performed the fixes and internal checks. These are AI reviews, not independent human review, proof-kernel verification or maintainer acceptance. + +### Follow-up findings at 6310550e + +| Finding | Resolution | Evidence and limit | +| --- | --- | --- | +| Stone's stronger condition was incorrectly described as giving a rate | PROOF.md now distinguishes refinements (6)/(8), allowing boxes as small as exp(−cn), from a quantified remainder rate. Their remainder is still unquantified o(1); neither refinement is used. README and the original finding-1 record below are corrected too. | The wording originated in the first Claude review and was corrected by its follow-up primary-text check. Internal review confirms only this explanatory paragraph changed; a fresh primary-PDF retrieval remained unavailable internally. No theorem or argument change. | +| No control guarded the original #4436 Flow comparison | A scratch copy changes the returned boundary histogram by one count, re-pins that source, and requires the specific `(121, 'original Flow class')` rejection in normal and optimized modes. | The mutation is applied after Flow's own telescoping check, so that check cannot mask the comparison. Deleting just the original-Flow comparison must now make the new control fail; positive fixtures remain unchanged. | + +Internal follow-up review independently checked that the returned-boundary mutation changes the N=121 leaf count at rank 1 from 37305 to 37304 after all native invariants, verified re-pinning and restoration, and compared the deleted-guard results. No unresolved blocker remained in the scoped fix. Current proof/control hashes and executed evidence are recorded in VALIDATION.md. + +The follow-up review also independently exercised production remainder faults, deletion of the primary source comparison, and disabled standalone pin checks. Those are reported Claude runs, not additional local runs. Local commands and results for this response are distinguished in VALIDATION.md. -A separate internal reviewer checked the integrated changes without running a competing replay. It verified the alternative logarithm series, the degree 82 exponential geometric tail, full interval containment, meaningful remainder fixtures, re-pinned source mutations and pre-import hashes. No blocking defect was found. Current reviewed verifier SHA256 `3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d`; oracle SHA256 `b92a75601ef676ab0b412395eb2ccaa52c8e802f89fe1fb2f3820cafa173aea4`; proof SHA256 `09dc0d6fd22b5e502b812543ddf78395ab7deacc894cd52430709475acfb2978`. The final oracle metadata addition was checked against the earlier reviewed bytes. These are internal AI reviews with the shared arithmetic/series dependencies disclosed below, not formal verification. ## Claude review findings | Finding | Resolution | Evidence and limit | | --- | --- | --- | -| 1. Stone statement and uniformity need precise citation | PROOF.md §3 now names Corollary 1 (7), Theorem (5) and footnote 2; gives the normalization/rescaling and characteristic-function/support equivalence. | Fixed-x (12) is explicitly not the source of uniform concentration. The review reports checking the primary paper; the follow-up internal proof review corroborated the uniform form from Stone's later text but did not retrieve the original afresh. Stronger nonlattice rate hypotheses fail for finite support; this does not exclude quantitative rates by other methods. | -| 2. Terminal-rank flags overstate coverage | Removed the redundant self-factorization assertion; renamed flags as fixture sensitivity. The source identity is the complete histogram comparison. | `test_controls.py` actually empties or truncates the source leaf branch in a temporary tree, re-pins the mutant bytes, and requires semantic rejection by both source-law entry points, normally and under `-O`. A checksum failure cannot count as this semantic rejection. | +| 1. Stone statement and uniformity need precise citation | PROOF.md §3 now names Corollary 1 (7), Theorem (5) and footnote 2; gives the normalization/rescaling and characteristic-function/support equivalence. | Fixed-x (12) is explicitly not the source of uniform concentration. The review reports checking the primary paper; the follow-up internal proof review corroborated the uniform form from Stone's later text but did not retrieve the original afresh. Stone's stronger nonlattice condition fails for finite support, but (6)/(8) concern shrinking boxes, not quantified remainder rates. Neither refinement is used; quantitative rates by other methods remain possible. | +| 2. Terminal-rank flags overstate coverage | Removed the redundant self-factorization assertion; renamed flags as fixture sensitivity. The source identity is the complete histogram comparison. | `test_controls.py` empties or truncates #4467's leaf branch in a temporary tree, re-pins the mutant bytes, and requires semantic rejection by both source-law entry points, normally and under `-O`. The follow-up adds a distinct control for the original #4436 comparison. A checksum failure cannot count as this semantic rejection. | | 3. Remainder bounds lack discriminating controls | Added `test_enclosures.py`, an exact-rational independent enclosure oracle. | It checks every successful log/exp argument captured from current `parameters()` and `controls()`. Logarithms use a different series; exponentials use a positive-series geometric tail rather than the primary Lagrange bound. Zero logarithm/exponential tails and the invalid majorant 1 are rejected at explicit fixtures even though the old rounded receipt did not distinguish them. | | 4. Standalone independent source checker lacks byte binding | `independent_source.py` authenticates every declared live input before any predecessor import. | Comment-only mutations to both predecessor verifier and original flow are rejected by both standalone entry points in normal and optimized modes. No Git is needed. | | 5. Executable source domain ends at G≤3 | Retained and explicitly scoped; no unnecessary search expansion. | The source proof is for every G, while the local primary/independent fixtures remain eight/ten checks through G=3. Claude reported further G=4–5 corroboration; this package does not present that as a newly executed local check. | @@ -21,7 +31,7 @@ A separate internal reviewer checked the integrated changes without running a co ## Shared dependencies and remaining limits -The remainder oracle certifies containment on the captured finite argument domain. Both implementations still share Python's exact rational arithmetic and the exponential series; the logarithm series and exponential remainder arguments differ. This is not formal verification or a proof of the routines for arbitrary future inputs. Its domain digest and loaded verifier SHA identify the checked inputs and code. +The remainder oracle certifies containment on the captured finite argument domain. Both implementations still share Python's exact rational arithmetic and the exponential series; the logarithm series and exponential remainder arguments differ. This is not formal verification or a proof of the routines for arbitrary future inputs. Its domain digest and loaded verifier SHA identify the checked inputs and code. It independently checks the log/exp building blocks, not the surrounding interval operations, the μ(t) construction or outward rounding; those rely on the pinned receipt, code review and the earlier independent decimal diagnostic. The diagnostic corroborates values but does not itself certify rational bounds. The +1 histogram mutations are regressions for the fixed narrow root bracket, not general tests of interval arithmetic. The derivative-bound endpoint ordering is justified by the written monotonicity argument and code review; a changed printed derivative is also caught by the expected receipt. The new enclosure tests do not claim to independently prove that derivative formula. @@ -37,6 +47,11 @@ For commands and current receipts, use [VALIDATION.md](VALIDATION.md#current-evi ## Historical review record +### Internal review of the first response + +Before the new Claude follow-up, an internal reviewer checked the alternative logarithm series, the degree 82 exponential geometric tail, full containment, targeted remainder fixtures, re-pinned #4467 source mutations and pre-import hashes. It found no blocker at that review's scope. Reviewed verifier SHA256 `3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d`; oracle `b92a75601ef676ab0b412395eb2ccaa52c8e802f89fe1fb2f3820cafa173aea4`; then-current proof `09dc0d6fd22b5e502b812543ddf78395ab7deacc894cd52430709475acfb2978`. The subsequent Claude review identified the Stone wording and missing #4436 guard recorded above. The old proof hash is retained as provenance, not a hash of the corrected current proof. + + The following sections record the initial `ff365dba6911ce615bec76e8d1f149faf1fe16ca` contribution and intermediate reviewed bytes. Their hashes and receipts are historical; use the current evidence index above for present code. Two separate OpenAI Codex agents examined pinned source inputs before seeing the lead's proof. ### Independent mathematical derivation diff --git a/research/direct-flow-leaf-saturation/VALIDATION.md b/research/direct-flow-leaf-saturation/VALIDATION.md index 294a303eef..6c7f5819a9 100644 --- a/research/direct-flow-leaf-saturation/VALIDATION.md +++ b/research/direct-flow-leaf-saturation/VALIDATION.md @@ -2,18 +2,19 @@ ## Current evidence index -**Scientific snapshot: `553198839618962e07519b51cb3bbe808ca6f1dc`.** The proof, four Python checkers, RESULT.json, SOURCES.json and VERIFY.json remain byte-identical to this snapshot. The hashes in [claude-validation.json](logs/claude-validation.json) identify those eight scientific files. Later commits add evidence, attribution and documentation; a newer documentation commit does not mean the numerical experiments were rerun. +The current hashes, exact commands, stdout/stderr and results are in [followup-validation.json](logs/followup-validation.json). This follow-up to `9946b1c42466ada889c10cd0cea7522d6360a63b` corrects one explanatory Stone paragraph, adds a semantic mutation for the original #4436 comparison, and updates its verification description. The numerical certificate, source checker, enclosure oracle, RESULT.json and SOURCES.json are unchanged. The theorem and its argument are unchanged. -| Evidence | Receipt | Actual result and scope | +| Evidence | Receipt | Scope | | --- | --- | --- | -| Registered replay and metadata | [run manifest and source hashes](logs/claude-validation.json), [replay output](logs/claude-registered.log) | All four registered commands passed in 75.068 s; metadata passed separately. | -| Optimized checks | [certificate](logs/claude-optimized.log), [source fixtures](logs/claude-independent-optimized.log), [mutation controls](logs/claude-mutations-optimized.log) | All exited 0; explicit controls remain effective under `-O`. | -| Independent rational enclosures | [normal receipt](logs/claude-enclosures-normal.json), [optimized receipt](logs/claude-enclosures-optimized.json), [timings](logs/claude-enclosures-timing.json) | Identical receipts; 16 log and 127 exp arguments; all three targeted remainder faults rejected. | -| Git-free exported replay | [commands, times and log links](logs/claude-portable-results.json) | Four direct commands passed on exported scientific snapshot `553198839`; no Git or executable PATH entries. | -| Committed bytes and source history | [export record below](#committed-export-and-git-free-replay) | Passed for 41 package/input files at `553198839`; final evidence snapshot `6310550e932de70243fc2aaab6f4885688b6fe21` passed for 46. File counts include five declared predecessor inputs. | -| Written theorem and review | [PROOF.md](PROOF.md), [review findings](REVIEW.md#claude-review-findings) | Scoped analytic argument with Stone's theorem as an external input; no proof-kernel or human verification. | +| Registered replay and metadata | [current run record](logs/followup-validation.json) | All four registered commands, with the new #4436 control; source hashes identify the executed bytes. | +| Optimized mutation controls and deleted-comparison attack | [current run record](logs/followup-validation.json) | A one-count returned-histogram mutation must reach the original-Flow comparison. Removing that comparison makes the control fail; normal and optimized modes are distinguished in the record. | +| Independent rational enclosures | [normal receipt](logs/claude-enclosures-normal.json), [optimized receipt](logs/claude-enclosures-optimized.json) | Unchanged verifier/oracle bytes; 16 log and 127 exp arguments. The current registered run also repeats the normal oracle check. | +| Committed export and Git-free changed-control replay | [current run record](logs/followup-validation.json) | The changed mutation suite is replayed from an exported tree without Git. Earlier full export replays remain evidence for unchanged direct entry points. | +| Written theorem and review | [PROOF.md](PROOF.md), [review findings](REVIEW.md) | Scoped analytic argument with Stone's theorem as an external input; corrected prose makes no quantitative-rate claim. | -Receipts with the `claude-` prefix apply to the current scientific files. Receipts without it are retained historical evidence for `ff365dba`; their schema and source hashes should not be used to certify current code. Historical review hashes likewise identify intermediate snapshots, not the current files. No original receipt was replaced during documentation consolidation. +The registered replay passed in 75.175 s and metadata in 0.300 s. The isolated mutation suite passed in normal/optimized modes in 31.698/31.589 s; deleting only the original-Flow comparison caused the intended control failure in 1.439/1.541 s. Both positive independent-source baselines passed. All five unchanged numerical/source files were compared byte-for-byte with `6310550e`; the proof differs in exactly one explanatory paragraph. Internal review found no unresolved blocker. Exported-tree results are added to the same current record after execution. + +`followup-validation.json` is the current response record. The `claude-` receipts below identify the first response at `553198839618962e07519b51cb3bbe808ca6f1dc`; they do not exercise the new #4436 mutation. Unprefixed receipts identify the initial `ff365dba` evidence. Earlier numerical receipts still apply where their scientific hashes match unchanged files; historical proof/control hashes must not be mistaken for current hashes. No original receipt was replaced. Base and last upstream refresh: `721c03822c421b7f7fcbb2598993b947c4d88419`, 2026-10-28. Priority revision 8. The branch adds only `research/direct-flow-leaf-saturation/`; frozen predecessors and the selected record are unchanged. @@ -38,9 +39,9 @@ The JSON run manifests preserve the additional optimized-mode commands actually Reusing these receipts requires matching the scientific hashes and predecessor pins. Changes to the proof require renewed argument review; changes to code, numerical data or inputs require the affected numerical/source checks and updated receipts. Documentation-only navigation edits require link, claim-consistency and metadata checks plus confirmation that the scientific bytes remain unchanged. Export checks establish availability and integrity; they do not prove the theorem. -## Current local validation +## First review response: historical validation -The response addresses all six findings on `ff365dba6911ce615bec76e8d1f149faf1fe16ca`; [REVIEW.md](REVIEW.md#claude-review-findings) maps scope and evidence. All `RESULT.json.parameters` values compare exactly equal to that snapshot. The receipt's source-check labels changed to report histogram equality and fixture sensitivity accurately. The finite source domains remain G≤3. +The first response addressed the six findings on `ff365dba6911ce615bec76e8d1f149faf1fe16ca`; [REVIEW.md](REVIEW.md#claude-review-findings) maps scope and evidence. All `RESULT.json.parameters` values compare exactly equal to that snapshot. The receipt's source-check labels changed to report histogram equality and fixture sensitivity accurately. The finite source domains remain G≤3. The following Python 3.12 runs all exited 0. Commands, environment and final scientific-source hashes are in [logs/claude-validation.json](logs/claude-validation.json): @@ -52,13 +53,13 @@ The following Python 3.12 runs all exited 0. Commands, environment and final sci | independent-optimized | 0.155 | [log](logs/claude-independent-optimized.log) | | mutations-optimized | 30.389 | [log](logs/claude-mutations-optimized.log) | -The registered replay now runs four commands, including the independent rational enclosure test. Normal and optimized oracle checks additionally passed in 28.674 s and 27.920 s with identical receipts; [timings](logs/claude-enclosures-timing.json), [normal receipt](logs/claude-enclosures-normal.json), [optimized receipt](logs/claude-enclosures-optimized.json). They cover 16 integer logarithm arguments and 127 distinct rational exponential arguments, and reject all three reported remainder faults. Their receipts identify the loaded verifier SHA and exact argument-domain digest. This independently certifies finite-domain enclosure containment, not all-input correctness or the asymptotic theorem. +The first response expanded the registered replay to four commands, including the independent rational enclosure test. Normal and optimized oracle checks additionally passed in 28.674 s and 27.920 s with identical receipts; [timings](logs/claude-enclosures-timing.json), [normal receipt](logs/claude-enclosures-normal.json), [optimized receipt](logs/claude-enclosures-optimized.json). They cover 16 integer logarithm arguments and 127 distinct rational exponential arguments, and reject all three reported remainder faults. Their receipts identify the loaded verifier SHA and exact argument-domain digest. This independently certifies finite-domain enclosure containment, not all-input correctness or the asymptotic theorem. -Both standalone source checkers now reject altered source bytes. Re-pinned empty and terminal-truncated source branches are rejected by the actual histogram comparisons, in normal and optimized modes. This separates source semantics from checksum failures and from fixture sensitivity. Fixed-root-bracket and corrupted-receipt controls remain separately labelled. +Both standalone source checkers reject altered source bytes. In this first response, re-pinned empty and terminal-truncated #4467 branches were rejected by the #4467 histogram comparisons, in normal and optimized modes; this evidence did not guard the original #4436 comparison. This separates source semantics from checksum failures and from fixture sensitivity. Fixed-root-bracket and corrupted-receipt controls remain separately labelled. The final internal review found no blocking issue in the updated proof, source binding, mutation tests or oracle mathematics. Primary numerical functions were compared by AST against the reviewed snapshot and are unchanged; only `finite_law` changed in verify.py. The oracle's last change adds the loaded source SHA to its receipt and was separately reviewed. The earlier README's “adds eight”→“checks eight” wording avoids implying eighteen distinct source ranks; this prose-only change affects no evidence. -## Committed export and Git-free replay +## First response: committed export and Git-free replay Scientific follow-up commit: `553198839618962e07519b51cb3bbe808ca6f1dc`. Committed-byte comparison with `--check-source-history` passed for all 41 package/input files, with the original base as the source-history ancestor. The official exporter and archive check both reported `PASS_RESEARCH_EXPORT` for those 41 files: @@ -72,11 +73,11 @@ The archive was extracted into a fresh directory, using an absolute Python 3.12 Pre-publication refresh at 2026-10-28T12:34:31Z found canonical main unchanged at `721c03822c421b7f7fcbb2598993b947c4d88419` and no guidance/priority change. A bounded live check of the 100 most recently updated PRs (all states) and 100 Discussions reached back to October 28 00:24Z and October 25 03:58Z respectively, overlapping the earlier complete body snapshots. Exact predecessor and saturation-term checks found no new competing saturation result; this is body-level coverage, not a claim to have reviewed every diff or reply. Existing #6118 was confirmed open and draft before the update. -## Documentation consolidation checks +## Historical documentation consolidation checks -The documentation follow-up to `6310550e932de70243fc2aaab6f4885688b6fe21` changes only README.md, REVIEW.md, CLAUDE-RESPONSE.md and this file. A Python 3.12 link/anchor scan passed all 56 relative links in those documents. SHA256 checks matched all eight scientific files to `logs/claude-validation.json` and `553198839618962e07519b51cb3bbe808ca6f1dc`; byte comparisons confirmed all 28 logs unchanged from `6310550e`. Package metadata/source pins and `git diff --check` passed. Independent AI documentation review preserved the original limitations and corrected wording that had overstated the executed drift controls. Positive drift is certified; no nonpositive-drift test is claimed. +The documentation commit `9946b1c42466ada889c10cd0cea7522d6360a63b`, following `6310550e932de70243fc2aaab6f4885688b6fe21`, changed only README.md, REVIEW.md, CLAUDE-RESPONSE.md and this file. A Python 3.12 link/anchor scan passed all 56 relative links in those documents. SHA256 checks matched all eight scientific files to `logs/claude-validation.json` and `553198839618962e07519b51cb3bbe808ca6f1dc`; byte comparisons confirmed all 28 logs unchanged from `6310550e`. Package metadata/source pins and `git diff --check` passed. Independent AI documentation review preserved the original limitations and corrected wording that had overstated the executed drift controls. Positive drift is certified; no nonpositive-drift test is claimed. -No scientific replay was rerun for this documentation-only change; the current scientific receipts above remain applicable to identical bytes. Committed-byte/source-history and export checks are performed on the documentation commit before publication. Reproduce the metadata and committed-byte checks with: +No scientific replay was rerun for this documentation-only change; the then-current scientific receipts applied to identical bytes at `9946b1c`. The later Stone/control response is indexed separately above. Committed-byte/source-history and export checks are performed on the documentation commit before publication. Reproduce the metadata and committed-byte checks with: ```sh python3.12 -B scripts/research_package.py --package research/direct-flow-leaf-saturation --check-only diff --git a/research/direct-flow-leaf-saturation/VERIFY.json b/research/direct-flow-leaf-saturation/VERIFY.json index a4ca4629cc..12a862ef59 100644 --- a/research/direct-flow-leaf-saturation/VERIFY.json +++ b/research/direct-flow-leaf-saturation/VERIFY.json @@ -38,7 +38,7 @@ "{package}/test_controls.py" ], "timeout_seconds": 120, - "checks": "Reject altered bytes in both standalone entry points; re-pinned empty/truncated source branches rejected semantically in normal and optimized modes; fixed-bracket and receipt regressions." + "checks": "Reject altered bytes in both standalone entry points; re-pinned empty/truncated #4467 branches and altered #4436 returned histogram rejected by their comparisons in normal and optimized modes; fixed-bracket and receipt regressions." }, { "argv": [ diff --git a/research/direct-flow-leaf-saturation/logs/followup-validation.json b/research/direct-flow-leaf-saturation/logs/followup-validation.json new file mode 100644 index 0000000000..2124fd3d54 --- /dev/null +++ b/research/direct-flow-leaf-saturation/logs/followup-validation.json @@ -0,0 +1,159 @@ +{ + "python": "3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]", + "platform": "Linux-6.18.55-x86_64-with-glibc2.41", + "reviewed_snapshot": "6310550e932de70243fc2aaab6f4885688b6fe21", + "starting_head": "9946b1c42466ada889c10cd0cea7522d6360a63b", + "base": "721c03822c421b7f7fcbb2598993b947c4d88419", + "scientific_files_sha256": { + "PROOF.md": "6e32d89065b5fb14c457fa990a166f68c840ec16566c480000dc620ad842aa4e", + "verify.py": "3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d", + "RESULT.json": "d195c3fd5620bf2e64dc7d677c79ad52e780aefde9534d4e6a02a5ff1b9c9bdd", + "independent_source.py": "abe248ffc0012fdcb7a941c399cba0f5f943c006d86368553c1c3317442f5773", + "test_controls.py": "7039979fb32e410470bc5d2cd664c519cca2d0924b8e461b9290662b9b31fbb9", + "test_enclosures.py": "b92a75601ef676ab0b412395eb2ccaa52c8e802f89fe1fb2f3820cafa173aea4", + "SOURCES.json": "90997ec1be8cd8c3e588d71a349783b2f1696a224dc082749f3886bebd8c2c4a", + "VERIFY.json": "9c007727bbd9b0128e25d8394d40b60047f132b4d954b7eea974653de89b83f2" + }, + "runs": [ + { + "name": "metadata", + "command": [ + "/workspace/integer-mult-bounds/.venv/bin/python", + "-B", + "scripts/research_package.py", + "--package", + "research/direct-flow-leaf-saturation", + "--check-only" + ], + "reproduce": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/direct-flow-leaf-saturation", + "--check-only" + ], + "exit_code": 0, + "seconds": 0.3, + "stdout": "PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check)\n", + "stderr": "" + }, + { + "name": "registered", + "command": [ + "/workspace/integer-mult-bounds/.venv/bin/python", + "-B", + "scripts/research_package.py", + "--package", + "research/direct-flow-leaf-saturation" + ], + "reproduce": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/direct-flow-leaf-saturation" + ], + "exit_code": 0, + "seconds": 75.175, + "stdout": "CHECK Exact rational root/drift/tilt/limit enclosures, eight whole-flow fixtures, lattice and domain failure controls; classical LLT proof is written, not machine-checked.\n{\n \"controls\": {\n \"interval_domain_rejections\": 3,\n \"lattice_countermodel\": \"geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1\"\n },\n \"finite_law\": {\n \"ordered_word_max_depth\": 3,\n \"source_check\": \"complete actual X-BX histogram equals ordered-word enumeration\",\n \"terminal_cut_distinguishing_fixtures\": 8,\n \"whole_flow_fixtures\": 8\n },\n \"parameters\": {\n \"alpha\": [\n \"0.98981438244597\",\n \"0.98981438244599\"\n ],\n \"drift_above_log5\": [\n \"0.016477707041\",\n \"0.016477707042\"\n ],\n \"invoice_derivative_lower_bound_interval_0_99_to_1\": [\n \"211661.930309\",\n \"211661.930310\"\n ],\n \"lambda\": [\n \"0.00749912850515\",\n \"0.00749912850519\"\n ],\n \"mean_deficit_limit\": [\n \"133.34882837\",\n \"133.34882838\"\n ],\n \"mean_leaf_depth_limit\": [\n \"136.51870330\",\n \"136.51870331\"\n ],\n \"mean_log_rank\": [\n \"1.625915619475\",\n \"1.625915619476\"\n ],\n \"method\": \"exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds\",\n \"t_star\": [\n \"0.99731351095114\",\n \"0.99731351095116\"\n ]\n },\n \"scope\": \"Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.\",\n \"status\": \"PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS\"\n}\nCHECK Ten independent ordered-word fixtures compare complete #4436 and #4467 leaf histograms after authenticating every input; terminal-cut fields describe fixture sensitivity.\n{\n \"status\": \"PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION\",\n \"fixtures\": [\n {\n \"N\": 121,\n \"G\": 0,\n \"leaf_ranks\": 9,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 604,\n \"G\": 0,\n \"leaf_ranks\": 9,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 605,\n \"G\": 1,\n \"leaf_ranks\": 26,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 606,\n \"G\": 1,\n \"leaf_ranks\": 26,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 3024,\n \"G\": 1,\n \"leaf_ranks\": 30,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 3025,\n \"G\": 2,\n \"leaf_ranks\": 55,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 3026,\n \"G\": 2,\n \"leaf_ranks\": 55,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 15124,\n \"G\": 2,\n \"leaf_ranks\": 65,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 15125,\n \"G\": 3,\n \"leaf_ranks\": 98,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 15126,\n \"G\": 3,\n \"leaf_ranks\": 98,\n \"terminal_cut_distinguished\": true\n }\n ]\n}\nCHECK Reject altered bytes in both standalone entry points; re-pinned empty/truncated #4467 branches and altered #4436 returned histogram rejected by their comparisons in normal and optimized modes; fixed-bracket and receipt regressions.\nPASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized repinned_original_flow_return_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions\nCHECK Independent exact rational bounds at every executed log/exp argument; reject zero logarithm/exponential tails and invalid exponential remainder majorant.\n{\n \"all_exp_arguments_below\": \"479/100\",\n \"distinct_exp_rational_arguments\": 127,\n \"domain_sha256\": \"5e27ec5fc8e5fe372d5511730fd47d3d9acac76ae707221b11bfa99b963c58e4\",\n \"exp_oracle\": \"degree-82 positive series; exact ratio-bounded geometric tail\",\n \"log_integer_arguments\": [\n 1,\n 2,\n 3,\n 4,\n 5,\n 6,\n 7,\n 8,\n 9,\n 16,\n 25,\n 32,\n 41,\n 48,\n 57,\n 121\n ],\n \"log_oracle\": \"256-term -log(1-q) series; exact positive geometric tail\",\n \"mutations_rejected\": [\n \"zero_log_tail_at_log2\",\n \"zero_exp_tail_at_exp1\",\n \"invalid_exp_majorant_one_at_exp1\"\n ],\n \"production_source_sha256\": \"3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d\",\n \"scope\": \"Exact containment at every argument captured from current parameters and controls; finite mutation discrimination, not a formal verifier or an all-input enclosure proof.\",\n \"status\": \"PASS_INDEPENDENT_RATIONAL_ENCLOSURES\"\n}\nPASS_REGISTERED_RESEARCH_PACKAGE research/direct-flow-leaf-saturation outcome=completed\n", + "stderr": "" + } + ], + "independent_guard_runs": [ + { + "variant": "intact_comparison", + "mode": "normal", + "command": [ + "/workspace/integer-mult-bounds/.venv/bin/python", + "-I", + "-B", + "/workspace/work/assignment-20261028/followup2-s7bzl6f4/research/direct-flow-leaf-saturation/test_controls.py" + ], + "returncode": 0, + "elapsed_seconds": 31.698, + "result": "PASS_MUTATION_CONTROLS including intended original Flow comparison" + }, + { + "variant": "intact_comparison", + "mode": "optimized", + "command": [ + "/workspace/integer-mult-bounds/.venv/bin/python", + "-I", + "-O", + "-B", + "/workspace/work/assignment-20261028/followup2-s7bzl6f4/research/direct-flow-leaf-saturation/test_controls.py" + ], + "returncode": 0, + "elapsed_seconds": 31.589, + "result": "PASS_MUTATION_CONTROLS including intended original Flow comparison" + }, + { + "variant": "deleted_original_comparison", + "mode": "normal", + "command": [ + "/workspace/integer-mult-bounds/.venv/bin/python", + "-I", + "-B", + "/workspace/work/assignment-20261028/followup2-l1jemiz6/research/direct-flow-leaf-saturation/test_controls.py" + ], + "returncode": 1, + "elapsed_seconds": 1.439, + "result": "ValueError: control did not reject with \"(121, 'original Flow class')\": 0," + }, + { + "variant": "deleted_original_comparison", + "mode": "optimized", + "command": [ + "/workspace/integer-mult-bounds/.venv/bin/python", + "-I", + "-O", + "-B", + "/workspace/work/assignment-20261028/followup2-l1jemiz6/research/direct-flow-leaf-saturation/test_controls.py" + ], + "returncode": 1, + "elapsed_seconds": 1.541, + "result": "ValueError: control did not reject with \"(121, 'original Flow class')\": 0," + } + ], + "independent_positive_runs": [ + { + "command": [ + "/workspace/integer-mult-bounds/.venv/bin/python", + "-I", + "-B", + "research/direct-flow-leaf-saturation/independent_source.py" + ], + "elapsed_seconds": 0.109, + "returncode": 0, + "status": "positive baseline passed" + }, + { + "command": [ + "/workspace/integer-mult-bounds/.venv/bin/python", + "-I", + "-O", + "-B", + "research/direct-flow-leaf-saturation/independent_source.py" + ], + "elapsed_seconds": 0.182, + "returncode": 0, + "status": "positive baseline passed" + } + ], + "guard_reproduction": { + "mirror": "Copy test_controls.py, verify.py, independent_source.py, SOURCES.json, RESULT.json and every usage=input source into a scratch root at their original relative paths.", + "deletion": "Delete exactly the line need(other==exact,(N,'original Flow class')) from the scratch independent_source.py, preserving all other statements.", + "commands": [ + "python3.12 -I -B research/direct-flow-leaf-saturation/test_controls.py", + "python3.12 -I -O -B research/direct-flow-leaf-saturation/test_controls.py" + ], + "expected": "With comparison intact: exit0/PASS_MUTATION_CONTROLS. With it deleted: exit1 and control did not reject with original Flow class; its child had returned0." + }, + "internal_review": { + "verdict": "No unresolved blocker in scoped fix.", + "scope": "Independent argument/code check of N121 rank1 37305-to-37304 returned-histogram mutation, re-pinning/restoration and comparison deletion; one-paragraph Stone wording correction; evidence/provenance limits.", + "primary_text": "Precise Stone (6)/(8) reading supplied by Claude Code follow-up; fresh internal primary-PDF retrieval unavailable.", + "ai_assistance": "OpenAI Codex (GPT-6 Astra); Claude Code (Opus 5.5) follow-up. No human or formal verification." + } +} diff --git a/research/direct-flow-leaf-saturation/test_controls.py b/research/direct-flow-leaf-saturation/test_controls.py index 6b8c5a77ed..853574c027 100644 --- a/research/direct-flow-leaf-saturation/test_controls.py +++ b/research/direct-flow-leaf-saturation/test_controls.py @@ -74,6 +74,23 @@ def repin(package, root, relative): source.write_text(original) shutil.copy2(HERE / 'SOURCES.json', package / 'SOURCES.json') + # Corrupt only the original Flow class's returned boundary histogram, after + # its own conservation checks. This reaches the independent comparison + # instead of failing an earlier producer invariant or byte-authentication. + relative = 'research/direct-mixed-flow/flow.py' + source = root / relative + original = source.read_text() + field = "'boundary_exits': boundary," + if original.count(field) != 1: + raise ValueError('original Flow mutation anchor drift') + source.write_text(original.replace(field, "'boundary_exits': boundary + Counter({1: 1}),")) + repin(package, root, relative) + for mode in ([], ['-O']): + require_rejection([sys.executable, *mode, '-B', str(package / 'independent_source.py')], + root, "(121, 'original Flow class')") + source.write_text(original) + shutil.copy2(HERE / 'SOURCES.json', package / 'SOURCES.json') + expected = json.loads((package / 'RESULT.json').read_text()) expected['parameters']['lambda'][0] = '0.0' receipt = package / 'corrupt-result.json' @@ -93,4 +110,4 @@ def repin(package, root, relative): raise else: raise ValueError('changed histogram passed fixed root certificate: ' + name) -print('PASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions') +print('PASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized repinned_original_flow_return_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions') From 3a6aad36191db560a241b9a2f05a272bef28b859 Mon Sep 17 00:00:00 2001 From: Figo Lam Date: Wed, 28 Oct 2026 13:45:18 +0000 Subject: [PATCH 7/7] Record committed follow-up export and portable control evidence --- .../direct-flow-leaf-saturation/VALIDATION.md | 2 +- .../logs/followup-validation.json | 67 +++++++++++++++++++ 2 files changed, 68 insertions(+), 1 deletion(-) diff --git a/research/direct-flow-leaf-saturation/VALIDATION.md b/research/direct-flow-leaf-saturation/VALIDATION.md index 6c7f5819a9..cda10273f7 100644 --- a/research/direct-flow-leaf-saturation/VALIDATION.md +++ b/research/direct-flow-leaf-saturation/VALIDATION.md @@ -12,7 +12,7 @@ The current hashes, exact commands, stdout/stderr and results are in [followup-v | Committed export and Git-free changed-control replay | [current run record](logs/followup-validation.json) | The changed mutation suite is replayed from an exported tree without Git. Earlier full export replays remain evidence for unchanged direct entry points. | | Written theorem and review | [PROOF.md](PROOF.md), [review findings](REVIEW.md) | Scoped analytic argument with Stone's theorem as an external input; corrected prose makes no quantitative-rate claim. | -The registered replay passed in 75.175 s and metadata in 0.300 s. The isolated mutation suite passed in normal/optimized modes in 31.698/31.589 s; deleting only the original-Flow comparison caused the intended control failure in 1.439/1.541 s. Both positive independent-source baselines passed. All five unchanged numerical/source files were compared byte-for-byte with `6310550e`; the proof differs in exactly one explanatory paragraph. Internal review found no unresolved blocker. Exported-tree results are added to the same current record after execution. +The registered replay passed in 75.175 s and metadata in 0.300 s. The isolated mutation suite passed in normal/optimized modes in 31.698/31.589 s; deleting only the original-Flow comparison caused the intended control failure in 1.439/1.541 s. Both positive independent-source baselines passed. All five unchanged numerical/source files were compared byte-for-byte with `6310550e`; the proof differs in exactly one explanatory paragraph. Internal review found no unresolved blocker. At scientific follow-up commit `309eff43c247b711026eda5e5629409a89ff6242`, committed-byte/source-history and official export/check commands passed for 47 package/input files. The changed mutation suite then passed in isolated optimized mode without Git in 33.424 s; all 48 exported files, including the export manifest, remained byte-identical. The subsequent evidence commit adds only this record and the consolidated log, without changing scientific files. `followup-validation.json` is the current response record. The `claude-` receipts below identify the first response at `553198839618962e07519b51cb3bbe808ca6f1dc`; they do not exercise the new #4436 mutation. Unprefixed receipts identify the initial `ff365dba` evidence. Earlier numerical receipts still apply where their scientific hashes match unchanged files; historical proof/control hashes must not be mistaken for current hashes. No original receipt was replaced. diff --git a/research/direct-flow-leaf-saturation/logs/followup-validation.json b/research/direct-flow-leaf-saturation/logs/followup-validation.json index 2124fd3d54..bdfa91cfc1 100644 --- a/research/direct-flow-leaf-saturation/logs/followup-validation.json +++ b/research/direct-flow-leaf-saturation/logs/followup-validation.json @@ -58,6 +58,31 @@ "seconds": 75.175, "stdout": "CHECK Exact rational root/drift/tilt/limit enclosures, eight whole-flow fixtures, lattice and domain failure controls; classical LLT proof is written, not machine-checked.\n{\n \"controls\": {\n \"interval_domain_rejections\": 3,\n \"lattice_countermodel\": \"geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1\"\n },\n \"finite_law\": {\n \"ordered_word_max_depth\": 3,\n \"source_check\": \"complete actual X-BX histogram equals ordered-word enumeration\",\n \"terminal_cut_distinguishing_fixtures\": 8,\n \"whole_flow_fixtures\": 8\n },\n \"parameters\": {\n \"alpha\": [\n \"0.98981438244597\",\n \"0.98981438244599\"\n ],\n \"drift_above_log5\": [\n \"0.016477707041\",\n \"0.016477707042\"\n ],\n \"invoice_derivative_lower_bound_interval_0_99_to_1\": [\n \"211661.930309\",\n \"211661.930310\"\n ],\n \"lambda\": [\n \"0.00749912850515\",\n \"0.00749912850519\"\n ],\n \"mean_deficit_limit\": [\n \"133.34882837\",\n \"133.34882838\"\n ],\n \"mean_leaf_depth_limit\": [\n \"136.51870330\",\n \"136.51870331\"\n ],\n \"mean_log_rank\": [\n \"1.625915619475\",\n \"1.625915619476\"\n ],\n \"method\": \"exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds\",\n \"t_star\": [\n \"0.99731351095114\",\n \"0.99731351095116\"\n ]\n },\n \"scope\": \"Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.\",\n \"status\": \"PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS\"\n}\nCHECK Ten independent ordered-word fixtures compare complete #4436 and #4467 leaf histograms after authenticating every input; terminal-cut fields describe fixture sensitivity.\n{\n \"status\": \"PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION\",\n \"fixtures\": [\n {\n \"N\": 121,\n \"G\": 0,\n \"leaf_ranks\": 9,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 604,\n \"G\": 0,\n \"leaf_ranks\": 9,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 605,\n \"G\": 1,\n \"leaf_ranks\": 26,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 606,\n \"G\": 1,\n \"leaf_ranks\": 26,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 3024,\n \"G\": 1,\n \"leaf_ranks\": 30,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 3025,\n \"G\": 2,\n \"leaf_ranks\": 55,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 3026,\n \"G\": 2,\n \"leaf_ranks\": 55,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 15124,\n \"G\": 2,\n \"leaf_ranks\": 65,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 15125,\n \"G\": 3,\n \"leaf_ranks\": 98,\n \"terminal_cut_distinguished\": true\n },\n {\n \"N\": 15126,\n \"G\": 3,\n \"leaf_ranks\": 98,\n \"terminal_cut_distinguished\": true\n }\n ]\n}\nCHECK Reject altered bytes in both standalone entry points; re-pinned empty/truncated #4467 branches and altered #4436 returned histogram rejected by their comparisons in normal and optimized modes; fixed-bracket and receipt regressions.\nPASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized repinned_original_flow_return_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions\nCHECK Independent exact rational bounds at every executed log/exp argument; reject zero logarithm/exponential tails and invalid exponential remainder majorant.\n{\n \"all_exp_arguments_below\": \"479/100\",\n \"distinct_exp_rational_arguments\": 127,\n \"domain_sha256\": \"5e27ec5fc8e5fe372d5511730fd47d3d9acac76ae707221b11bfa99b963c58e4\",\n \"exp_oracle\": \"degree-82 positive series; exact ratio-bounded geometric tail\",\n \"log_integer_arguments\": [\n 1,\n 2,\n 3,\n 4,\n 5,\n 6,\n 7,\n 8,\n 9,\n 16,\n 25,\n 32,\n 41,\n 48,\n 57,\n 121\n ],\n \"log_oracle\": \"256-term -log(1-q) series; exact positive geometric tail\",\n \"mutations_rejected\": [\n \"zero_log_tail_at_log2\",\n \"zero_exp_tail_at_exp1\",\n \"invalid_exp_majorant_one_at_exp1\"\n ],\n \"production_source_sha256\": \"3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d\",\n \"scope\": \"Exact containment at every argument captured from current parameters and controls; finite mutation discrimination, not a formal verifier or an all-input enclosure proof.\",\n \"status\": \"PASS_INDEPENDENT_RATIONAL_ENCLOSURES\"\n}\nPASS_REGISTERED_RESEARCH_PACKAGE research/direct-flow-leaf-saturation outcome=completed\n", "stderr": "" + }, + { + "name": "git-free-optimized-mutation-controls", + "export_commit": "309eff43c247b711026eda5e5629409a89ff6242", + "command": [ + "/workspace/integer-mult-bounds/.venv/bin/python", + "-I", + "-O", + "-B", + "research/direct-flow-leaf-saturation/test_controls.py" + ], + "reproduce": [ + "python3.12", + "-I", + "-O", + "-B", + "research/direct-flow-leaf-saturation/test_controls.py" + ], + "git_available": false, + "path": "empty directory", + "exit_code": 0, + "seconds": 33.424, + "stdout": "PASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized repinned_original_flow_return_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions\n", + "stderr": "", + "exported_files_unchanged": 48 } ], "independent_guard_runs": [ @@ -155,5 +180,47 @@ "scope": "Independent argument/code check of N121 rank1 37305-to-37304 returned-histogram mutation, re-pinning/restoration and comparison deletion; one-paragraph Stone wording correction; evidence/provenance limits.", "primary_text": "Precise Stone (6)/(8) reading supplied by Claude Code follow-up; fresh internal primary-PDF retrieval unavailable.", "ai_assistance": "OpenAI Codex (GPT-6 Astra); Claude Code (Opus 5.5) follow-up. No human or formal verification." + }, + "committed_export": { + "commit": "309eff43c247b711026eda5e5629409a89ff6242", + "files_including_inputs": 47, + "source_history_ancestor": "721c03822c421b7f7fcbb2598993b947c4d88419", + "checks": [ + "PASS_RESEARCH_COMMIT_BYTES --check-source-history", + "PASS_RESEARCH_EXPORT export", + "PASS_RESEARCH_EXPORT check" + ], + "reproduction": [ + [ + "python3.12", + "-B", + "scripts/check_research_commit.py", + "--package", + "research/direct-flow-leaf-saturation", + "--ref", + "309eff43c247b711026eda5e5629409a89ff6242", + "--check-source-history" + ], + [ + "python3.12", + "-B", + "scripts/export_research_package.py", + "export", + "--package", + "research/direct-flow-leaf-saturation", + "--ref", + "309eff43c247b711026eda5e5629409a89ff6242", + "--output", + "/tmp/leaf-followup.tar" + ], + [ + "python3.12", + "-B", + "scripts/export_research_package.py", + "check", + "/tmp/leaf-followup.tar" + ] + ], + "command_note": "Preflight ran at scientific HEAD309eff43c; export used --ref HEAD and a temporary archive outside the repository. Reproduction commands resolve that head explicitly and substitute /tmp for the archive path." } }