{"id":"df4daad4-0dd7-484d-a80d-214b25e54906","arxiv_id":"2606.06807","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"full","parameter_count":0,"one_line_summary":"The authors establish K_KR ≤ 694198146664396294486127753 / 34994834677886019996000000 ≈ 19.837, halving the original Kalton-Roberts upper bound.","lead":"The paper proves a new upper bound of approximately 19.837 for the Kalton-Roberts constant K_KR governing nearly additive set functions on algebras. A smart generalist might read it to see how expander graphs combined with formal verification in Lean can halve a long-standing bound in combinatorial mathematics.","discovery_kind":"extension","skeptic_critique":{"model":"grok-4.3","headline":"Certification of the four expander families via exact rational interval arithmetic is the least secure step supporting the numerical bound.","rationale":"The reader's weakest_assumption matches the load-bearing point: the numerical claim rests on four external certified inputs whose correctness is not mechanically verified inside the Lean formalization. All other parts of the argument (recombination logic, Lean-checked derivations) are covered by the formalization, so the interval-arithmetic step is the single place where an undetected flaw would directly affect the headline constant.","tokens_in":1674,"tokens_out":284,"duration_ms":18748,"concrete_test":"Re-run the exact rational interval arithmetic procedure described for one of the four expander families (using the same rational endpoints and arithmetic rules given in the paper) and verify whether the certified interval still contains the numerical parameters fed into the recombination step.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The claimed upper bound is produced by a recombination construction that takes four specific expander families as inputs and combines them with new source collections. The paper certifies the required expansion and spectral properties of these families by exact rational interval arithmetic computations rather than deriving them from first principles or including them in the Lean formalization. The formalization covers the combinatorial argument assuming those certifications are correct; an undetected error in any of the four interval-arithmetic checks would invalidate the final rational upper bound.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.3","summary":"The paper proves that the optimal Kalton-Roberts constant K_KR for approximately additive real-valued set functions satisfies K_KR ≤ 694198146664396294486127753 / 34994834677886019996000000 ≈ 19.837. This halves the original Kalton-Roberts upper bound of 89/2 and improves on the previous best bound of 38.8. The argument modifies the source collections in an expander-recombination construction, certifies the required properties of four specific expander families by exact rational interval arithmetic, and includes a Lean formalization of the combinatorial steps.","tokens_in":1739,"tokens_out":331,"duration_ms":17411,"significance":"If the result holds, the improvement is substantial and directly addresses a long-standing quantitative question in functional analysis and combinatorics. Credit is due for the machine-checked Lean formalization of the core argument and for the parameter-free explicit rational bound obtained via certified interval arithmetic; these features strengthen verifiability beyond typical analytic proofs in the area.","major_comments":[{"comment":"Abstract and § on the recombination construction: the final numerical bound is produced by feeding four externally certified expander families into the recombination step. The Lean formalization assumes the expansion and spectral properties of these families; an undetected error in any of the four interval-arithmetic certifications would invalidate the claimed constant. The manuscript should indicate whether the exact rational interval-arithmetic scripts or their outputs are deposited for independent checking.","section":"Abstract and recombination construction"}],"minor_comments":[],"recommendation":"accept","confidential_remarks":null},"author_rebuttal":{"model":"grok-4.3","summary":"We thank the referee for the positive report and the recommendation to accept. We respond to the major comment below.","responses":[{"response":"We agree that explicitly indicating the availability of the certification materials would improve verifiability. In the revised manuscript we will add a sentence in the abstract and in the section on the recombination construction stating that the exact rational interval-arithmetic scripts together with their outputs are deposited both in the supplementary files on the arXiv and in the public repository accompanying the Lean formalization.","revision_made":"yes","referee_comment":"[Abstract and recombination construction] Abstract and § on the recombination construction: the final numerical bound is produced by feeding four externally certified expander families into the recombination step. The Lean formalization assumes the expansion and spectral properties of these families; an undetected error in any of the four interval-arithmetic certifications would invalidate the claimed constant. The manuscript should indicate whether the exact rational interval-arithmetic scripts or their outputs are deposited for independent checking."}],"tokens_in":1289,"tokens_out":224,"duration_ms":17859,"standing_objections":[]},"desk_editor":{"model":"grok-4.3","letter":"The headline result is a new explicit upper bound K_KR ≤ 694198146664396294486127753 / 34994834677886019996000000 ≈ 19.837. That is more than half the prior 38.8 bound from Bondarenko-Prymak-Radchenko. The authors reach it by feeding different source collections into the expander-recombination construction while keeping the expander graphs themselves. The combinatorial steps are formalized in Lean, and the bound is given as an exact rational.\n\nThe formalization is the clearest strength. It removes the usual worry about arithmetic slips in the final calculation. The improvement is concrete and the paper states the numerical value outright rather than hiding it behind big-O notation.\n\nThe remaining uncertainty sits with the four chosen expander families. Their expansion and spectral properties are certified by separate exact rational interval arithmetic rather than being included in the Lean script. An error in any of those four checks would break the claimed bound, even though the recombination logic itself is verified. The paper presents those families as verified inputs, so the formalization is conditional on them.\n\nThis is a narrow, technical improvement inside combinatorial functional analysis. Specialists who care about the precise value of K_KR or who use expander-recombination arguments will want to see the details. It is solid enough on its own terms to merit referee time; the Lean artifact and the explicit rational make the central claim checkable.","headline":"This cuts the Kalton-Roberts constant to roughly 19.837 via a Lean proof on modified recombination, with the main gap being external certification of the four expanders.","tokens_in":2245,"tokens_out":370,"would_cite":false,"duration_ms":11207,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.3","headline":"The Kalton-Roberts constant K_KR for nearly additive set functions is at most approximately 19.837.","keywords":["Kalton-Roberts constant","nearly additive set functions","expander graphs","recombination method","upper bound","interval arithmetic","Lean formalization"],"falsifier":"A concrete nearly additive set function whose deviation from additivity exceeds 19.837 times its total variation, or an arithmetic error found in the rational interval certification of any of the four expander families.","tokens_in":2539,"feed_emoji":"","tokens_out":716,"duration_ms":19886,"temperature":0.7,"pith_summary":"The paper proves a new upper bound on the Kalton-Roberts constant K_KR, which measures how far a real-valued set function on an algebra can deviate from additivity while remaining controlled by its variation. Earlier results gave K_KR ≤ 89/2 = 44.5 and then ≤ 38.8; the new bound is the explicit rational 694198146664396294486127753 / 34994834677886019996000000 ≈ 19.837. The improvement comes from feeding different source collections into an expander-recombination procedure whose four final expander families are certified by exact rational interval arithmetic, with the entire argument formalised in Lean.","feed_headline":"Kalton-Roberts constant bound cut to ≈19.837","feed_subtitle":"Certified expanders halve the 1983 upper bound of 44.5 for how far set functions can deviate from additivity.","key_machinery":"Expander-recombination step driven by four specific expander families whose parameters are certified by exact rational interval arithmetic.","core_discovery":"Let K_KR denote the optimal Kalton--Roberts constant for approximately additive real-valued set functions on algebras of sets. We prove that K_KR ≤ 694198146664396294486127753 / 34994834677886019996000000 ≈ 19.837. Thus the original Kalton--Roberts upper bound is more than halved. The proof changes the source collections fed into the expander-recombination step however still uses expander graphs as the other proofs do. The four expander families used in the final recombination are certified by exact rational interval arithmetic, and the proof has been formalised in Lean.","pith_inferences":["The same certified-recombination technique might tighten other constants that arise from additive approximation problems on set algebras.","Explicit lower-bound constructions for K_KR would now be more informative, since the gap between 19.837 and the true optimum is smaller than before.","If smaller expander families with the required spectral properties can be found, the same proof skeleton would immediately yield a still tighter rational upper bound."],"forward_implications":["The deviation of any nearly additive set function from true additivity is controlled by a constant less than 20 times its variation.","The original Kalton-Roberts bound of 44.5 is replaced by a value less than half that size.","Machine-verified certificates for expander families can be reused or improved in subsequent calculations of the same constant."],"fun_headline_variants":["Kalton-Roberts constant bound halved to ≈19.837","Certified expanders halve bound to ≈19.837","Lean proof yields Kalton-Roberts constant ≈19.837","Halved bound K_KR ≤19.837 formalised in Lean"],"cache_read_input_tokens":2112,"weakest_assumption_plain":"The four specific expander families chosen for the final recombination step are correctly certified by the exact rational interval arithmetic computations described in the proof.","fun_headline_variants_meta":{"raw":{"variants":["Kalton-Roberts constant bound halved to ≈19.837","Certified expanders halve bound to ≈19.837","Lean proof yields Kalton-Roberts constant ≈19.837","Halved bound K_KR ≤19.837 formalised in Lean"]},"model":"grok-4.3","cost_usd":0.007382,"raw_usage":{"total_tokens":3312,"prompt_tokens":665,"num_sources_used":0,"completion_tokens":65,"cost_in_usd_ticks":73815500,"prompt_tokens_details":{"text_tokens":665,"audio_tokens":0,"image_tokens":0,"cached_tokens":64},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":2582,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":665,"tokens_out":65,"duration_ms":17275,"temperature":1.0,"reasoning_tokens":2582,"cache_read_input_tokens":64,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-06-27T22:09:11.061982+00:00","model_set":{"reader":"grok-4.3"},"falsifier":"A concrete nearly additive set function whose deviation from additivity exceeds 19.837 times its total variation, or an arithmetic error found in the rational interval certification of any of the four expander families.","supporting_citations":[],"review_version":1}