arXiv subjects

Martin Dvorak

Publications and source records attributed to Martin Dvorak.

At least 19 recordsLinked to original sources

arXiv2026

Pursuit of Truth and Beauty in Lean 4: Formally Verified Theory of Grammars, Optimization, Matroids

This thesis documents a voyage towards truth and beauty via formal verification of theorems. To this end, we develop libraries in Lean 4 that present definitions and results from diverse areas of MathematiCS (i.e., Mathematics and Computer Science). The aim is to create code that is understandable, believable, useful, and elegant. The code should stand for itself as much as possible without a need for documentation; however, this text redundantly documents our code artifacts and provides additional context that isn't present in the code. This thesis is written for readers who know Lean 4 but are not familiar with any of the topics presented. We manifest truth and beauty in three formalized areas of MathematiCS (optimization theory, matroid theory, and the theory of grammars). In the pursuit of truth, we focus on identifying the trusted code in each project and presenting it faithfully. We emphasize the readability and believability of definitions rather than choosing definitions that are easier to work with. In search for beauty, we focus on the philosophical framework of Roger Scruton, who emphasizes that beauty is not a mere decoration but, most importantly, beauty is the means for shaping our place in the world and a source of redemption, where it can be viewed as a substitute for religion.

cs.LO↗

arXiv2026

A Blueprint for the Formalization of Seymour's Matroid Decomposition Theorem

This document is a blueprint for the formalization in Lean of the structural theory of regular matroids underlying Seymour's decomposition theorem. We present a modular account of regularity via totally unimodular representations, show that regularity is preserved under $1$-, $2$-, and $3$-sums, and establish regularity for several special classes of matroids, including graphic, cographic, and the matroid $R_{10}$. The blueprint records the logical structure of the proof, the precise dependencies between results, and their correspondence with Lean declarations. It is intended both as a guide for the ongoing formalization effort and as a human-readable reference for the organization of the proof.

math.CO↗

arXiv2025

The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

We report on the Equational Theories Project (ETP), an online collaborative pilot project to explore new ways to collaborate in mathematics with machine assistance. The project successfully determined all 22 028 942 edges of the implication graph between the 4694 simplest equational laws on magmas, by a combination of human-generated and automated proofs, all validated by the formal proof assistant language Lean. As a result of this project, several new constructions of magmas satisfying specific laws were discovered, and several auxiliary questions were also addressed, such as the effect of restricting attention to finite magmas.

math.RA↗

arXiv2025

Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified

Seymour's decomposition theorem is a hallmark result in matroid theory presenting a structural characterization of the class of regular matroids. Formalization of matroid theory faces many challenges, most importantly that only a limited number of notions and results have been implemented so far. In this work, we formalize the proof of the forward (composition) direction of Seymour's theorem for regular matroids. To this end, we develop a library in Lean 4 that implements definitions and results about totally unimodular matrices, vector matroids, their standard representations, regular matroids, and 1-, 2-, and 3-sums of matrices and binary matroids given by their standard representations. Using this framework, we formally state Seymour's decomposition theorem and implement a formally verified proof of the composition direction in the setting where the matroids have finite rank and may have infinite ground sets.

math.CO↗

arXiv2024

Duality theory in linear optimization and its extensions -- formally verified

Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state and formally prove several Farkas-like theorems over linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the case when some coefficients are allowed to take "infinite values".

math.OC↗

arXiv2023

Closure Properties of General Grammars -- Formally Verified

We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction.

cs.FL↗

arXiv2022

JUNO Sensitivity on Proton Decay $p\to \bar\nu K^+$ Searches

The Jiangmen Underground Neutrino Observatory (JUNO) is a large liquid scintillator detector designed to explore many topics in fundamental physics. In this paper, the potential on searching for proton decay in $p\to \bar\nu K^+$ mode with JUNO is investigated.The kaon and its decay particles feature a clear three-fold coincidence signature that results in a high efficiency for identification. Moreover, the excellent energy resolution of JUNO permits to suppress the sizable background caused by other delayed signals. Based on these advantages, the detection efficiency for the proton decay via $p\to \bar\nu K^+$ is 36.9% with a background level of 0.2 events after 10 years of data taking. The estimated sensitivity based on 200 kton-years exposure is $9.6 \times 10^{33}$ years, competitive with the current best limits on the proton lifetime in this channel.

hep-ex↗

arXiv2022

Prospects for Detecting the Diffuse Supernova Neutrino Background with JUNO

We present the detection potential for the diffuse supernova neutrino background (DSNB) at the Jiangmen Underground Neutrino Observatory (JUNO), using the inverse-beta-decay (IBD) detection channel on free protons. We employ the latest information on the DSNB flux predictions, and investigate in detail the background and its reduction for the DSNB search at JUNO. The atmospheric neutrino induced neutral current (NC) background turns out to be the most critical background, whose uncertainty is carefully evaluated from both the spread of model predictions and an envisaged \textit{in situ} measurement. We also make a careful study on the background suppression with the pulse shape discrimination (PSD) and triple coincidence (TC) cuts. With latest DSNB signal predictions, more realistic background evaluation and PSD efficiency optimization, and additional TC cut, JUNO can reach the significance of 3$σ$ for 3 years of data taking, and achieve better than 5$σ$ after 10 years for a reference DSNB model. In the pessimistic scenario of non-observation, JUNO would strongly improve the limits and exclude a significant region of the model parameter space.

hep-ex↗

arXiv2022

Mass Testing and Characterization of 20-inch PMTs for JUNO

Main goal of the JUNO experiment is to determine the neutrino mass ordering using a 20kt liquid-scintillator detector. Its key feature is an excellent energy resolution of at least 3 % at 1 MeV, for which its instruments need to meet a certain quality and thus have to be fully characterized. More than 20,000 20-inch PMTs have been received and assessed by JUNO after a detailed testing program which began in 2017 and elapsed for about four years. Based on this mass characterization and a set of specific requirements, a good quality of all accepted PMTs could be ascertained. This paper presents the performed testing procedure with the designed testing systems as well as the statistical characteristics of all 20-inch PMTs intended to be used in the JUNO experiment, covering more than fifteen performance parameters including the photocathode uniformity. This constitutes the largest sample of 20-inch PMTs ever produced and studied in detail to date, i.e. 15,000 of the newly developed 20-inch MCP-PMTs from Northern Night Vision Technology Co. (NNVT) and 5,000 of dynode PMTs from Hamamatsu Photonics K. K.(HPK).

physics.ins-det↗

arXiv2022

Damping signatures at JUNO, a medium-baseline reactor neutrino oscillation experiment

We study damping signatures at the Jiangmen Underground Neutrino Observatory (JUNO), a medium-baseline reactor neutrino oscillation experiment. These damping signatures are motivated by various new physics models, including quantum decoherence, $ν_3$ decay, neutrino absorption, and wave packet decoherence. The phenomenological effects of these models can be characterized by exponential damping factors at the probability level. We assess how well JUNO can constrain these damping parameters and how to disentangle these different damping signatures at JUNO. Compared to current experimental limits, JUNO can significantly improve the limits on $τ_3/m_3$ in the $ν_3$ decay model, the width of the neutrino wave packet $σ_x$, and the intrinsic relative dispersion of neutrino momentum $σ_{\rm rel}$.

hep-ex↗

arXiv2022

Sub-percent Precision Measurement of Neutrino Oscillation Parameters with JUNO

JUNO is a multi-purpose neutrino observatory under construction in the south of China. This publication presents new sensitivity estimates for the measurement of the $Δm^2_{31}$, $Δm^2_{21}$, $\sin^2 θ_{12}$, and $\sin^2 θ_{13}$ oscillation parameters using reactor antineutrinos, which is one of the primary physics goals of the experiment. The sensitivities are obtained using the best knowledge available to date on the location and overburden of the experimental site, the nuclear reactors in the surrounding area and beyond, the detector response uncertainties, and the reactor antineutrino spectral shape constraints expected from the TAO satellite detector. It is found that the $Δm^2_{31}$, $Δm^2_{21}$, and $\sin^2 θ_{12}$ oscillation parameters will be determined to better than 0.5% precision in six years of data collection, which represents approximately an order of magnitude improvement over existing constraints.

hep-ex↗

arXiv2021

Radioactivity control strategy for the JUNO detector

JUNO is a massive liquid scintillator detector with a primary scientific goal of determining the neutrino mass ordering by studying the oscillated anti-neutrino flux coming from two nuclear power plants at 53 km distance. The expected signal anti-neutrino interaction rate is only 60 counts per day, therefore a careful control of the background sources due to radioactivity is critical. In particular, natural radioactivity present in all materials and in the environment represents a serious issue that could impair the sensitivity of the experiment if appropriate countermeasures were not foreseen. In this paper we discuss the background reduction strategies undertaken by the JUNO collaboration to reduce at minimum the impact of natural radioactivity. We describe our efforts for an optimized experimental design, a careful material screening and accurate detector production handling, and a constant control of the expected results through a meticulous Monte Carlo simulation program. We show that all these actions should allow us to keep the background count rate safely below the target value of 10 Hz in the default fiducial volume, above an energy threshold of 0.7 MeV.

physics.ins-det↗

arXiv2021

JUNO sensitivity to low energy atmospheric neutrino spectra

Atmospheric neutrinos are one of the most relevant natural neutrino sources that can be exploited to infer properties about cosmic rays and neutrino oscillations. The Jiangmen Underground Neutrino Observatory (JUNO) experiment, a 20 kton liquid scintillator detector with excellent energy resolution is currently under construction in China. JUNO will be able to detect several atmospheric neutrinos per day given the large volume. A study on the JUNO detection and reconstruction capabilities of atmospheric $ν_e$ and $ν_μ$ fluxes is presented in this paper. In this study, a sample of atmospheric neutrino Monte Carlo events has been generated, starting from theoretical models, and then processed by the detector simulation. The excellent timing resolution of the 3'' PMT light detection system of JUNO detector and the much higher light yield for scintillation over Cherenkov allow to measure the time structure of the scintillation light with very high precision. Since $ν_e$ and $ν_μ$ interactions produce a slightly different light pattern, the different time evolution of light allows to discriminate the flavor of primary neutrinos. A probabilistic unfolding method has been used, in order to infer the primary neutrino energy spectrum from the detector experimental observables. The simulated spectrum has been reconstructed between 100 MeV and 10 GeV, showing a great potential of the detector in the atmospheric low energy region.

hep-ex↗

arXiv2021

Generalized minimum 0-extension problem and discrete convexity

Given a fixed finite metric space $(V,\mu)$, the {\em minimum $0$-extension problem}, denoted as ${\tt 0\mbox{-}Ext}[\mu]$, is equivalent to the following optimization problem: minimize function of the form $\min\limits_{x\in V^n} \sum_i f_i(x_i) + \sum_{ij}c_{ij}\mu(x_i,x_j)$ where $c_{ij},c_{vi}$ are given nonnegative costs and $f_i:V\rightarrow \mathbb R$ are functions given by $f_i(x_i)=\sum_{v\in V}c_{vi}\mu(x_i,v)$. The computational complexity of ${\tt 0\mbox{-}Ext}[\mu]$ has been recently established by Karzanov and by Hirai: if metric $\mu$ is {\em orientable modular} then ${\tt 0\mbox{-}Ext}[\mu]$ can be solved in polynomial time, otherwise ${\tt 0\mbox{-}Ext}[\mu]$ is NP-hard. To prove the tractability part, Hirai developed a theory of discrete convex functions on orientable modular graphs generalizing several known classes of functions in discrete convex analysis, such as $L^\natural$-convex functions. We consider a more general version of the problem in which unary functions $f_i(x_i)$ can additionally have terms of the form $c_{uv;i}\mu(x_i,\{u,v\})$ for $\{u,v\}\in F$, where set $F\subseteq\binom{V}{2}$ is fixed. We extend the complexity classification above by providing an explicit condition on $(\mu,F)$ for the problem to be tractable. In order to prove the tractability part, we generalize Hirai's theory and define a larger class of discrete convex functions. It covers, in particular, another well-known class of functions, namely submodular functions on an integer lattice. Finally, we improve the complexity of Hirai's algorithm for solving ${\tt 0\mbox{-}Ext}[\mu]$ on orientable modular graphs.

cs.CC↗

arXiv2021

Massively Winning Configurations in the Convex Grabbing Game on the Plane

The convex grabbing game is a game where two players, Alice and Bob, alternate taking extremal points from the convex hull of a point set on the plane. Rational weights are given to the points. The goal of each player is to maximize the total weight over all points that they obtain. We restrict the setting to the case of binary weights. We show a construction of an arbitrarily large odd-sized point set that allows Bob to obtain almost 3/4 of the total weight. This construction answers a question asked by Matsumoto, Nakamigawa, and Sakuma in [Graphs and Combinatorics, 36/1 (2020)]. We also present an arbitrarily large even-sized point set where Bob can obtain the entirety of the total weight. Finally, we discuss conjectures about optimum moves in the convex grabbing game for both players in general.

math.CO↗

arXiv2021

JUNO Physics and Detector

The Jiangmen Underground Neutrino Observatory (JUNO) is a 20 kton LS detector at 700-m underground. An excellent energy resolution and a large fiducial volume offer exciting opportunities for addressing many important topics in neutrino and astro-particle physics. With 6 years of data, the neutrino mass ordering can be determined at 3-4 sigma and three oscillation parameters can be measured to a precision of 0.6% or better by detecting reactor antineutrinos. With 10 years of data, DSNB could be observed at 3-sigma; a lower limit of the proton lifetime of 8.34e33 years (90% C.L.) can be set by searching for p->nu_bar K^+; detection of solar neutrinos would shed new light on the solar metallicity problem and examine the vacuum-matter transition region. A core-collapse supernova at 10 kpc would lead to ~5000 IBD and ~2000 (300) all-flavor neutrino-proton (electron) scattering events. Geo-neutrinos can be detected with a rate of ~400 events/year. We also summarize the final design of the JUNO detector and the key R&D achievements. All 20-inch PMTs have been tested. The average photon detection efficiency is 28.9% for the 15,000 MCP PMTs and 28.1% for the 5,000 dynode PMTs, higher than the JUNO requirement of 27%. Together with the >20 m attenuation length of LS, we expect a yield of 1345 p.e. per MeV and an effective energy resolution of 3.02%/\sqrt{E (MeV)}$ in simulations. The underwater electronics is designed to have a loss rate <0.5% in 6 years. With degassing membranes and a micro-bubble system, the radon concentration in the 35-kton water pool could be lowered to <10 mBq/m^3. Acrylic panels of radiopurity <0.5 ppt U/Th are produced. The 20-kton LS will be purified onsite. Singles in the fiducial volume can be controlled to ~10 Hz. The JUNO experiment also features a double calorimeter system with 25,600 3-inch PMTs, a LS testing facility OSIRIS, and a near detector TAO.

hep-ex↗

arXiv2021

The Design and Sensitivity of JUNO's scintillator radiopurity pre-detector OSIRIS

The OSIRIS detector is a subsystem of the liquid scintillator fillling chain of the JUNO reactor neutrino experiment. Its purpose is to validate the radiopurity of the scintillator to assure that all components of the JUNO scintillator system work to specifications and only neutrino-grade scintillator is filled into the JUNO Central Detector. The aspired sensitivity level of $10^{-16}$ g/g of $^{238}$U and $^{232}$Th requires a large ($\sim$20 m$^3$) detection volume and ultralow background levels. The present paper reports on the design and major components of the OSIRIS detector, the detector simulation as well as the measuring strategies foreseen and the sensitivity levels to U/Th that can be reached in this setup.

physics.ins-det↗

arXiv2021

Calibration Strategy of the JUNO Experiment

We present the calibration strategy for the 20 kton liquid scintillator central detector of the Jiangmen Underground Neutrino Observatory (JUNO). By utilizing a comprehensive multiple-source and multiple-positional calibration program, in combination with a novel dual calorimetry technique exploiting two independent photosensors and readout systems, we demonstrate that the JUNO central detector can achieve a better than 1% energy linearity and a 3% effective energy resolution, required by the neutrino mass ordering determination.

physics.ins-det↗