{"id":"b6c04c7a-637c-4ab9-b5ba-06024c781919","arxiv_id":"2607.09632","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"full","parameter_count":0,"one_line_summary":"Lean-QIT formalizes Schumacher compression, HSW classical capacity, and entanglement-assisted capacity (with strong converse) in Lean 4 via independent operational and analytic layers.","lead":"The authors built Lean-QIT, a Lean 4 library that machine-checks core quantum coding theorems by defining codes and rates separately from entropy formulas. This gives humans and AI systems a reusable, typed foundation for formal quantum Shannon theory.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified","rationale":"The paper’s strongest claim is an infrastructure result: operational objects are defined independently of their later analytic characterisations, and three cornerstone QST theorems are obtained as kernel-checked equalities relating those objects. The finite-dimensional restriction is declared in the notation section and is carried by every State/Channel typeclass; the three theorems are classical finite-dimensional statements, so the restriction does not create an internal gap. Concurrent Lean-Quantum work is disclosed and correctly scoped as complementary. The public repository and the explicit direct/converse/limit decomposition supply independent support for the claim. No hidden assumption that would falsify the three equalities inside the stated regime was identified; therefore the reader’s ACCEPT verdict stands.","tokens_in":24558,"tokens_out":427,"duration_ms":5335,"concrete_test":"Clone the public repository, pin the July 2026 snapshot commit, and run `lake build` on the three public endpoints `schumacher_data_compression_limit`, `hswClassicalCapacityTheorem_proved`, and `entanglementAssisted_capacity_and_strongConverseCapacity_eq_information_of_sandwichedLimit`; confirm zero `sorry`/`admit` and that each equality is kernel-checked.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that Lean-QIT supplies a reusable operational layer (codes, error criteria, rates, capacities defined independently of analytic formulae) and uses it to kernel-check Schumacher, HSW, and EA classical capacity (with strong converse). The manuscript states the finite-dimensional restriction up front, separates operational predicates from Holevo/mutual-information characterisations, and exhibits the direct/converse/limit assembly for each theorem. The reader’s weakest assumption (finite-dimensionality) is already explicit and does not undermine the three formalised equalities inside that regime. Residual risks (snapshot-level sorries, unpinned commit) are secondary engineering issues, not load-bearing threats to the architectural or theorem claims as stated.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The manuscript introduces Lean-QIT, a Lean 4 library for finite-dimensional quantum information theory organized into object, analytic, and operational layers. Its central design choice is to define codes, error criteria, achievable rates, and capacities independently of the entropic formulae that later characterize them, so that capacity equalities become theorems relating separately specified objects. Using this infrastructure, the authors formalize three classical quantum Shannon theory endpoints: Schumacher source coding (R_Sch(ρ)=S(ρ)), the HSW classical capacity (C(N)=lim (1/n)χ(N^⊗n)), and the entanglement-assisted classical capacity together with its strong converse (C_EA(N)=C̃_EA(N)=I(N)). The paper documents typed state/channel APIs, subsystem and measurement calculus, state geometry, mutual information and sandwiched Rényi data processing, hypothesis-testing interfaces, smooth-entropy/AEP bridges, and the direct/converse/limit assembly for each coding theorem, with public endpoint wrappers collected in Appendix A.","tokens_in":24747,"tokens_out":1164,"duration_ms":25822,"significance":"If the kernel-checked claims hold as stated, this is a substantial contribution to formal quantum information theory. Prior Lean developments have emphasized operator/entropy foundations or specialized tasks; Lean-QIT targets the underdeveloped operational coding layer that connects finite-block protocols to asymptotic capacities. Shipping machine-checked Schumacher, HSW, and EA (with strong converse) theorems, with operational rates defined before analytic characterizations and with named reusable direct/converse components, is a genuine advance. The finite-dimensional restriction is stated up front and does not undermine the three equalities inside that regime. The library’s size metrics, public repository, and explicit separation of operational predicates from Holevo/mutual-information formulae make the work a useful substrate for both human formalization and AI-assisted proof search.","major_comments":[{"comment":"The central claim is that the three capacity equalities are proved public endpoints checked by the Lean kernel (§2 terminology; Theorems 4.2, 4.7, 4.11 and the corresponding Lean declarations in §§4.1–4.3). The manuscript cites a “July 9, 2026 snapshot” and github.com/QuAIR/Lean-QIT but does not pin a commit hash, release tag, or lake lockfile, nor does it state whether the critical path for these three endpoints is free of sorry and of non-Mathlib axioms. For a formalization paper whose load-bearing claim is kernel-checked completeness, a short reproducibility subsection (pinned commit + axiom/sorry inventory for the Schumacher, HSW, and EA public endpoints) is needed so that referees and readers can verify the claim as stated.","section":null},{"comment":"§4.2–4.3 present packing/expurgation, Hayashi–Nagaoka, position-based coding, sequential decoding/quantum union bound, Petz and sandwiched Rényi limits, and cb-norm bridges as named witnesses consumed by the capacity squeezes. The paper is careful that operational definitions do not bake in analytic formulae, but it is not fully explicit which of these intermediate analytic ingredients are fully formalized in Lean-QIT versus imported as trusted lemmas or reduced to Mathlib. A brief table or paragraph mapping each named witness in Figure 3 to “fully proved / reduced to Mathlib / remaining obligation” would make the formalization depth of the HSW and EA spines auditable without changing the architectural claim.","section":null}],"minor_comments":[{"comment":"Figure 1 caption: typo “libaray” → “library”.","section":null},{"comment":"Abstract and title use both “LeanQIT” and “Lean-QIT”; standardize on one spelling throughout (including the GitHub URL branding).","section":null},{"comment":"Notation section defines R̄ = R ∪ {−∞,+∞} but later code listings use EReal; a one-line cross-reference would help readers map Lean types to the mathematical extended reals.","section":null},{"comment":"§3.4’s discussion of concurrent Lean-Quantum is useful; a short sentence clarifying non-overlap (basis-independent operator layer vs operational coding spine) would reduce ambiguity for readers who only skim the introduction.","section":null},{"comment":"Appendix A wrappers are thin by design; consider adding the fully-qualified Lean declaration names (module paths) next to each wrapper so that documentation and the paper stay synchronized as the library evolves.","section":null},{"comment":"In Definition 4.1 / Eq. (21), the joint purification error e_jp is used but only briefly glossed; a one-line definition matching the SchumacherCompressionCode interface would improve self-containment.","section":null}],"recommendation":"minor_revision","confidential_remarks":"This is a strong formalization paper for a quant-ph or formal-methods venue that values machine-checked infrastructure. The concurrent Lean-Quantum work is appropriately framed as complementary rather than competitive. My only editorial concern is verification logistics: without a pinned commit and sorry/axiom inventory, referees cannot independently confirm the kernel-checked claim that is the paper’s main deliverable. That is a standard fix, not a conceptual flaw. Scope fit is good if the journal accepts library/infrastructure contributions with theorem-scale validation."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The thing worth knowing is that this is not another isolated formalization of a single inequality. They built a typed operational spine—codes, error predicates, achievable-rate sets, capacities as sSup/sInf—and then proved the three classical equalities as theorems relating those objects to entropy/Holevo/mutual-information characterizations. That separation is the actual contribution, and the concurrent Lean-Quantum operator work is disclosed cleanly rather than papered over.\n\nWhat they do well is architectural honesty. Finite-dimensionality is stated up front. Direct, converse, and asymptotic pieces are named before they are assembled (typical subspace + AFW for Schumacher; packing/expurgation + Holevo for HSW; Petz lower bound + sandwiched Rényi meta-converse for EA, including the strong converse). The public wrappers and the >150k-line library claim are concrete enough that a referee can check the kernel status. Citation pattern tracks the modern Khatri–Lami–Wilde organization and the original sources; no free parameters, no circular definitions of capacity.\n\nSoft spots are real but secondary. Everything is finite-dimensional, so continuous-variable or infinite-dimensional extensions are future work, not delivered. The AI-agent rhetoric is aspirational packaging, not a result. Snapshot-level risks (possible unstated sorries, unpinned commit) are engineering hygiene, not load-bearing threats to the three equalities as stated. None of that undoes the formalization.\n\nThis is for people who care about machine-checked QIT infrastructure and for anyone who has ever had to re-derive the same DPI/AFW/Rényi bookkeeping. It deserves a serious referee. I would engage with the library and cite the operational-layer design when the formalization status is confirmed against a pinned commit.","headline":"A real, reusable Lean operational layer that machine-checks Schumacher, HSW, and EA capacity (with strong converse) while keeping codes and rates independent of the analytic formulae.","tokens_in":25355,"tokens_out":459,"would_cite":true,"duration_ms":5799,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["81P45","68V15","94A15"],"pacs":["03.67.-a","03.67.Hk"],"model":"grok-4.5","headline":"A Lean 4 library defines quantum codes and rates first, then proves the classic Shannon theorems as equalities between those objects and entropy formulae.","keywords":["quantum information theory","quantum Shannon theory","formal verification","Lean 4","Schumacher compression","HSW theorem","entanglement-assisted capacity","strong converse"],"falsifier":"Open the public repository snapshot and attempt to check the three named capacity endpoints (Schumacher rate equality, classicalCapacity equals regularized Holevo information, and both EA capacity and strong-converse capacity equal channel mutual information); a failed kernel check or a missing proof obligation would falsify the claim that those equalities are fully formalized.","tokens_in":25480,"feed_emoji":"⚛️","tokens_out":902,"duration_ms":8785,"temperature":0.7,"pith_summary":"This paper builds Lean-QIT, a machine-checked library for finite-dimensional quantum information theory. Its design choice is to define source codes, channel codes, error criteria, achievable rates, and capacities as independent operational objects, then prove that those rates equal the usual entropy and mutual-information formulae. With that spine the authors formalize Schumacher’s quantum source-coding theorem, the Holevo–Schumacher–Westmoreland classical capacity theorem, and the entanglement-assisted classical capacity theorem (including its strong converse). The point is that a capacity statement becomes a kernel-checked theorem relating two separately specified things, not a definition that already assumes the answer. A sympathetic reader cares because the same reusable interfaces—states, channels, hypothesis testing, one-shot quantities, and asymptotic bridges—can now support further coding theorems and give both humans and proof agents a typed place to audit assumptions and compose arguments.","feed_headline":"Lean library proves quantum coding theorems as true equalities","feed_subtitle":"Codes and rates are defined first; entropy formulae become theorems, not definitions","key_machinery":"The operational coding spine: typed definitions of source and channel codes, finite-block performance predicates, achievable-rate sets, and capacities (via sSup/sInf), kept independent of entropy formulae and later linked by named direct, converse, and asymptotic lemmas.","core_discovery":"By separating operational definitions of codes, error criteria, and capacities from their analytic characterizations, Lean-QIT turns the central equalities of quantum Shannon theory into kernel-checked theorems that relate independently defined objects. The library realizes this architecture by fully formalizing Schumacher source coding, the HSW classical capacity, and the entanglement-assisted classical capacity with its strong converse.","pith_inferences":["If the operational-first pattern holds for further theorems, formal QIT libraries may converge on a shared capacity API rather than theorem-specific scripts.","The finite-dimensional restriction suggests a natural next stress test: whether continuous-variable or infinite-dimensional coding can reuse the same rate predicates once a different state model is supplied.","Exposing one-shot and strong-converse layers as first-class endpoints may lower the cost of formalizing finite-blocklength refinements that currently sit outside textbook asymptotic statements."],"forward_implications":["Capacity equalities become auditable theorems rather than definitional identities, so suppressed side conditions can be inspected.","The same state, channel, testing, and asymptotic APIs can be reused for quantum, private, and resource-assisted capacities without rewriting the operational layer.","Direct and converse proof routes stay named and composable, so later theorems can cite packing, expurgation, or Rényi bounds as modular interfaces.","Typed objects and explicit side conditions supply a machine-readable substrate for retrieval, proof completion, and assumption auditing by humans or agents."],"fun_headline_variants":["Lean-QIT turns quantum coding equalities into kernel-checked theorems","Codes first: Lean proves quantum capacity equalities as true theorems","Lean formalizes Schumacher and HSW as operational equalities","Operational layer makes QIT rates Lean-proven theorems","Lean-QIT separates codes from entropy to prove capacity equalities"],"cache_read_input_tokens":16512,"weakest_assumption_plain":"Every system is finite-dimensional; the whole library and the three proved theorems rest on finite index types and matrix representations.","fun_headline_variants_meta":{"raw":{"variants":["Lean-QIT turns quantum coding equalities into kernel-checked theorems","Codes first: Lean proves quantum capacity equalities as true theorems","Lean formalizes Schumacher and HSW as operational equalities","Operational layer makes QIT rates Lean-proven theorems","Lean-QIT separates codes from entropy to prove capacity equalities"]},"model":"grok-4.5","effort":"low","cost_usd":0.00533,"raw_usage":{"total_tokens":1467,"prompt_tokens":772,"num_sources_used":0,"completion_tokens":71,"cost_in_usd_ticks":53300000,"prompt_tokens_details":{"text_tokens":772,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":624,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":772,"tokens_out":71,"duration_ms":5417,"temperature":1.0,"reasoning_tokens":624,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-13T01:35:35.828108+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Open the public repository snapshot and attempt to check the three named capacity endpoints (Schumacher rate equality, classicalCapacity equals regularized Holevo information, and both EA capacity and strong-converse capacity equal channel mutual information); a failed kernel check or a missing proof obligation would falsify the claim that those equalities are fully formalized.","supporting_citations":[],"review_version":1}