# Object generators 2: everyday sets, categories, and the “missing axiom” of
ZFC set theory

Frank Quinn

(Date: May 2023)

###### Contents

  1. 1 Introduction
  2. 2 Everyday set theory
    1. 2.1 Brief definitions
    2. 2.2 Unions of relaxed sets
    3. 2.3 Products
  3. 3 Large domains
  4. 4 Primitives of object-generator theory
    1. 4.1 Primitive objects
    2. 4.2 Assertion logic
    3. 4.3 Primitive hypotheses
  5. 5 Categories
    1. 5.1 Definition
      1. 5.1.1 The category OD
    2. 5.2 Isomorphism classes
    3. 5.3 Skeleta
    4. 5.4 Size of categories
    5. 5.5 Functor categories
  6. 6 Relationship to traditional set theory
    1. 6.1 Unions in ZFC
    2. 6.2 The Increasing Union Axiom

##  1\. Introduction

In _Object generators 1: set theory_ , [Quinn 1], we developed a theory of
object generators, and described a “relaxed” version of set theory inside it.
This turns out to be the set theory implicitly used in mainstream mathematics
for the last century. The main goal of [Quinn 1] is to clarify this, and
enable direct comparison with traditional axiomatic Zermillo-Fraenkel-Choice
(ZFC) set theories. In particular it describes a universal object satisfying
the ZFC-1 axioms. Here ‘-1’ indicates that the first-order logical constraints
in the Separation and Replacement axioms are omitted, and universality asserts
that this contains all models of these axioms.

In Section 2 we illustrate that the set theory by itself can be described
avoiding some of the complexities of general object-generator theory. In
particular this uses standard binary logic.

Section 3 provides information about the smallest object outside set theory:
the “ordinal numbers” or “class of all sets”. Many of its properties cannot be
formulated in standard binary logic, and the work-arounds give concrete
illustrations of the assertion logic described in Section 4.

Section 4 summarizes the axioms of object-generator theory.

In Section 5, we see that general object-generator theory gives a good setting
for categories. This is illustrated with fully detailed proofs of some
standard facts, e.g. existence of skeleta. More substantial applications will
probably occur in specialized settings such as higher-order category theory.

Section 6 shows that the union and product properties—in the way they are used
in practice—may fail in traditional ZFC theories. To illustrate the problem,
recall that a bounded nonempty subset of the reals has a supremum. So, for
example if we have a positive-term series with bounded partial sums, then the
sum of the series is the supremum of the partial sums. Unfortunately, in ZFC
existence of suprema only applies to sub _sets_. Without further hypotheses,
the collection of all partial sums may not be a _set_ in the given theory, so
may not have a supremum in the real numbers of the theory.

Finally we implement an idea of Gödel. The existence of many models of ZFC,
with dramatically different properties, suggested to Gödel that there should
be a “missing” axiom that would uniquely specify a particularly capable model.
The maximal model in [Quinn 1] coming from relaxed set theory seems to qualify
as “particularly capable”. We show that the “Increasing Union Axiom”, a
particularly explicit case of unions giving sets, characterizes the maximal
model. This seems to achieve Gödel’s goal.

##  2\. Everyday set theory

Most mathematicians use naïve set theory, with the admonition “don’t say ‘set
of all sets’ ”. We trace the history in more detail elsewhere, but the short
version is that naïve set theory was already being used successfully before
Russell’s Paradox became widely known, in 1902. The paradox seriously
disrupted the study of set theory but, mindful of the set-of-sets admonition,
mainstream mathematicians continued to have success with it. Many presumed
that other flaws would be revealed when set theorists got their act together.
In fact naïve set theory has solidly supported mathematical development for
more than a century, without additional problems. In this section we formulate
relaxed set theory so it is essentially the same as, and almost as easy to use
as, naïve set theory. This “explains” why naïve set theory has been so
successful.

###  2.1. Brief definitions

The primitive ideas here are “collection of elements”, and functions of these.
Technically a collection of elements is an object generator, but the general
theory is not needed here because these are used only as starting points for
immediate transitions into set theory. Being primitive, we have to rely on
heuristic or intuitive understandings rather than definitions from lower-level
objects. We use the term “collection of elements” here because it suggests
intuitions better suited for the current context. First definitions are:

  1. (1)

A binary function on a collection of elements is a function that has values
either ‘yes’ or ‘no’.

  2. (2)

A logical domain is a collection of elements with a binary pairing $D\times
D\to\textsf{y/n}$ that detects whether elements are the same or not. Such
pairings are denoted, as usual, by ‘=’, so $a=b$ has value ‘yes’ if $a$ and
$b$ are the same, and ‘no’ otherwise. (Detail about “sameness” is given in the
next Section.)

  3. (3)

The powerset of a logical domain is the collection of all binary functions on
it, see Note (1). Powersets are denoted $\textsf{P}[D]$.

  4. (4)

A domain $D$ supports quantification if there is a binary function
$\textsf{P}[D]\to\textsf{y/n}$ that detects the empty (always ‘no’) function.

  5. (5)

A (relaxed) set is a logical domain that supports quantification.

#### Notes

  1. (1)

A binary function determines a subdomain, namely the subcollection on which
the function has value ‘yes’. The traditional focus is on the subcollection,
but here we will find it advantageous to emphasize the function. This requires
some notation. For example, suppose $A$ is a domain with a partial order
$\leq\colon A\times A\to\textsf{y/n}$, and $a\in A$. Then $(\\#<a)$ is the
function that returns ‘yes’ if $\\#$ is strictly smaller than $a$. Here $\\#$
is a dummy variable for elements of $A$, used to avoid having to introduce a
name for the function. If it is useful to make the domain explicit, we use
something closer to the traditional set-builder notation: $(\\#\in
A\mid\\#<a)$. We also use square brackets to denote function evaluation: if
$f$ is a function then $f[a]$ denotes its value on $a$. This avoids confusion
with grouping, and again avoids extra notation. For instance
“$(\\#<a)[b]=(b<a)$” replaces the traditional “$f[b]$, where $f[x]:=(x<a)$”.

  2. (2)

In relaxed and naïve set theory, “functions” are primitive objects. In ZFC
functions are _not_ primitive, so must be defined. The only functions we can
be sure are in a ZFC theory come from formulas in the first-order logic of set
theory, cf. [Jech], p. 7. This can be problematic, as we see below.

  3. (3)

In ZFC and naïve set theory, any two elements can be compared. This means they
have “universes” of all possible elements, and the universe is a logical
domain. In relaxed set theory, elements of different domains generally cannot
be compared.

  4. (4)

In standard notation the function $\textsf{P}[D]\to\textsf{y/n}$ that detects
the empty function is $f\mapsto(\forall x\in D,f[x]=\textsf{no})$. The point
here is that if this one quantification expression is implemented by a binary
function, then all quantification expressions over $D$ are.

  5. (5)

The powerset of a logical domain $D$ is again a logical domain if and only if
$D$ supports quantification. There are domains that do not support
quantification.

  6. (6)

The Quantification Hypothesis asserts that first-order quantification implies
infinite-order quantification. This is assumed here. Without this, things are
more complicated and “sets” must be defined as domains that support infinite-
order quantification, see [Quinn 1].

  7. (7)

Sets in naïve set theory are essentially the same as collections of elements.
This lack of precision does not cause trouble essentially because when input
data is given in terms of sets (eg. groups, manifolds, etc. have underlying
sets) then standard operations always give sets. The discussion of unions,
given next, illustrates this.

###  2.2. Unions of relaxed sets

We begin with a more-general statement, then explain what it says about
unions. This is Proposition 3.5 of [Quinn 1]:

######  Proposition.

Suppose $f\colon A\to B$ is a function of collections of elements, and is onto
$B$. Then $A$ is a set if and only if $B$ and each point-preimage $f^{-1}[b]$
are sets.

#### Proof

We use the proof from [Quinn 1], changing terminology to fit the current
setting. The “if” direction is the useful one, so suppose $B$ and the
preimages are sets. The first step is to show $A$ is a logical domain by
exhibiting an equality pairing. Since $B$ is a set there is an equality
pairing $\stackrel{{\scriptstyle B}}{{=}}\colon B\times B\to\textsf{y/n}$.
Similarly, for each $b\in B$ there is an equality pairing
$\stackrel{{\scriptstyle b}}{{=}}$ on the preimage. The equality pairing on
$A$ is given by

$(x\stackrel{{\scriptstyle A}}{{=}}y):=(f[x]\stackrel{{\scriptstyle
B}}{{=}}f[y])\textsf{\,{and}\,}(x\stackrel{{\scriptstyle f[x]}}{{=}}y).$

The second step is to show $A$ supports quantification. A binary function
$h\colon A\to\textsf{y/n}$ is empty if and only restrictions to $f^{-1}[\\#]$
are empty, for all $\\#\in B$. The preimages are sets, so applying the empty-
detecting functions on each of those gives a binary function on $B$ that takes
$b$ to ‘yes’ if the restriction to $f^{-1}[b]$ is empty. The original function
is empty if and only if this function is identically ‘yes’, or equivalently if
the negation is empty. Applying the empty-detecting function on
$\textsf{P}[B]$ therefore gives an empty-detecting function on $A$, as
required.∎

#### Unions

To relate this to unions, suppose we have a collection of sets, indexed by a
set. Denote these by $A_{\\#}$, defined for $\\#\in B$. For example, if $S$ is
a set of objects in a category then $(x,y)\mapsto\textsf{morph}[x,y]$ is a
collection of sets indexed by $S\times S$.

######  Corollary.

The disjoint union $\amalg_{\\#\in B}A_{\\#}$ is a (relaxed) set.

The disjoint union is the collection of elements of the form $(b,a)$ where
$b\in B$ and $a\in A_{b}$. If the $A_{\\#}$ are all subsets of a logical
domain (e.g ZFC sets are all subsets of its Universe) then we can take the
internal union. But there is a function from the disjoint union onto an
internal union so, by the Proposition above, the Corollary implies the
conclusion for internal unions.

Proof of the Corollary: Denote the disjoint union by $C$, then there is a
function $C\to B$ defined by $(b,a)\mapsto b$. Now apply the Proposition to
conclude $C$ is a set.∎

###  2.3. Products

Suppose $A,B$ are sets and $f\colon A\to B$ is a function of collections of
elements. A section of $f$ is a function $g\colon B\to A$ such that $f\circ
g=\textsf{id}$. Alternately, if we view the point-inverses $f^{-1}[b]$ as a
family of sets indexed by $B$, then the collection of all sections is the
product $\times_{b\in B}f^{-1}[b]$.

The sections can be identified with a subcollection of the powerset
$\textsf{P}[A]$, namely the $h\colon A\to\textsf{y/n}$ such that for each
$b\in B$ there is a unique $a\in f^{-1}[b]$ with $h[a]=\textsf{yes}$. But $A$
is a set, so $\textsf{P}[A]$ is a set, and a subcollection of a set is a set.
Therefore products are sets.

##  3\. Large domains

A logical domain is said to be large if it does not support quantification.
$\mathbb{W}$ is the logical domain whose elements are equivalence classes of
well-ordered sets, [Quinn 1], §4.3. This corresponds to the universe, or
ordinal numbers, of a traditional axiomatic set theory and, consequently, is
not a set. In relaxed set theory what goes wrong is that it does not support
quantification, so is large in the sense above. Unlike traditional axiomatic
set theory we can say quite a bit about it, though this involves non-binary
logic.

#### The almost well-order

The orders on its elements induce a linear order on $\mathbb{W}$. This cannot
be a well-order because these require quantification, but it is an almost
well-order in the sense that the orders induced on bounded subdomains are
well-orders.

######  Proposition.

Suppose $A\subset\mathbb{W}$ is a subdomain.

  1. (1)

$A$ is bounded if and only if it is a set (ie. supports quantification);

  2. (2)

$A$ is cofinal if and only if it is order-isomorphic to $\mathbb{W}$; and

  3. (3)

there is no binary function defined on subdomains that detects which case
occurs.

In standard binary logic (1) and (2) are equivalent, being negations of each
other. However, (3) shows that binary logic does not apply. It might be
helpful to read (1) as “$A$ is _known_ to be bounded if and only if it is
_known_ to support quantification”. Trying to negate this gives only that
nothing is _known_ , which has no logical content.

We mention that subdomains of $\mathbb{W}$ are binary in the sense that they
are detected by binary functions. This means they correspond to elements of
the powerset $\textsf{P}[\mathbb{W}]$. Item (3) asserts that there is no
binary function on $\textsf{P}[\mathbb{W}]$ that distinguishes the two cases,
even though they are disjoint and together give all of
$\textsf{P}[\mathbb{W}]$.

#### Equivalence to $\mathbb{W}$

######  Proposition.

For a logical domain $A$ the following are equivalent:

  1. (1)

There is a bijection $A\simeq\mathbb{W}$;

  2. (2)

there is a function $A\to\mathbb{W}$ with point preimages sets and image
cofinal in $\mathbb{W}$; and

  3. (3)

there are injective (or surjective) functions $A\to\mathbb{W}$ and
$\mathbb{W}\to A$.

Again, these properties are not binary, so this should be read as “knowing one
case applies implies knowing the others”. (3) follows from the Cantor-
Bernstein theorem, see [Quinn 1] 3.3. Note this theorem requires the
injections to have binary image, but images in $\mathbb{W}$ are known to be
binary. The image of $\mathbb{W}\to A$ is binary because the composition
$\mathbb{W}\to A\to\mathbb{W}$ identifies it as an image in $\mathbb{W}$.
Applications, eg. to category theory, usually use case (2).

#### Minimality

The “minimality” of $\mathbb{W}$ mentioned above is:

######  Proposition.

If $A$ is a logical domain, then it does not support quantification if and
only if there is an injection $\mathbb{W}\to A$.

As above, both directions in this implication are assertions, and there is no
binary function on domains that identifies which case applies. Injections
$\mathbb{W}\to A$ are obtained by recursion, and this gives no information
about whether or not the image is binary. Comparing with the previous
proposition we see that if there is an injection whose image is not binary
then $A$ cannot inject into $\mathbb{W}$. At present we have no way to
construct such a thing, nor applications for it.

##  4\. Primitives of object-generator theory

We give an overview of the general theory to clarify the discussion of large
domains, and for use with categories. For details see [Quinn 1].

There are three types of primitive ingredients: primitive objects, primitive
logic, and primitive hypotheses. Primitives are not described in terms of
other things, so reliability is an experimental conclusion.

###  4.1. Primitive objects

Deductive systems need objects that are not defined, as starting points.
Behavior and usage of primitive objects are specified directly, since they
cannot be inferred from a definition. Anything that behaves in the required
way then qualifies as such an object.

#### Object generators

Object generators, sometimes shortened to just “generators”, generate things.
The things generated are called ‘objects’ or ‘outputs’. Usage takes the form
$x{\in\in}A$, which we read as “$x$ is an output of the generator
${{\in\in}}A$”, or “$x$ is an object in $A$”.

The term “generator” is intended to suggest that these give outputs but,
unlike the “element of” primitive in set theory, they have no logical ability
to identify outputs. In more detail, if $x$ is already specified then in
standard set theory the expression “$x\in A$” may be expected (by excluded
middle) to be ‘true’ or ‘false’. Here, for previously specified $x$,
$x{\in\in}A$ must be proved or asserted, otherwise it is a usage error that
invalidates arguments.

Syntax for defining generators takes the form “$x{\in\in}A$ means (…) ”. For
example, the generator whose objects are themselves generators is defined by:

$A{\in\in}\textsf{OG}$ means “$A$ is an object generator.”

A more standard example is the generator for groups. “$G$ is a group”, or
$G{\in\in}$(groups) means “$G$ is a set together with a binary operation that
is associative, and has a unit and inverses”.

#### Morphisms

Morphisms of generators are essentially the primitives behind functors of
categories. “$f\colon{\in\in}A\to{\in\in}B$ is a morphism” means that $f$
assigns to every object $x{\in\in}A$ an object $f[x]{\in\in}B$.

Morphisms have some of the structure expected of functors: for instance
morphisms
$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{B}$
and
$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\textstyle{C}$
can be composed to get a morphism

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.75pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
10.20538pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{g\circ f}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 30.75pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
30.75pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{C}$}}}}}}}\ignorespaces}}}}\ignorespaces.$

This composition is associative, for the usual reason, but stating this
requires the assertion form of $=$, see below.

#### Discipline

There are silly examples of generators. Fortunately, it is not necessary to
try to avoid this because binary functions provide discipline later in the
development. For instance, binary functions are time-independent, and
therefore cannot distinguish objects in the physical world. The examples given
in standard presentations of set theory are generators, but not actually sets.

###  4.2. Assertion logic

Logic provides methods of reasoning with primitive objects and hypotheses.
Traditional set theory uses _binary_ (ie yes/no valued) logic. The core logic
here is weaker in that it is based on assertions. We describe primitive
logical terms, and provide examples to illustrate useage.

There is a language problem: binary logic is deeply embedded in both our
natural language and our mathematical thinking. If we say “A is B”, for
instance, it is usually implicit that this is a binary function that returns
‘yes’ if it is true, and ‘no’ if it is not. In particular we can formally
negate to get “A is not B” simply by interchanging ‘yes’ and ‘no’. To avoid
this we use the word ‘known’ in natural-language formulations, as for example,
“A is _known_ to be B”. This is sometimes awkward, but it does prevent
unwarrented negation. The formal negation of “A is known to be B” is “A is
_not_ known to be B”, which has no logical force.

#### Assertions

An assertion is a statement that is known to be correct. $a{\in\in}B$, for
instance, is implicitly an assertion because it means “$a$ is (known to be) an
output of $B$”. Assertions are often indicated by ‘!’. For example, if we
specify $a{\in\in}B$, then at a later time we could say $a{!\in\in}B$ because
this is known to be correct.

For clarity, statements implemented by binary functions are often indicated by
‘?’. For example, suppose $a!{\in\in}A$ and $A\supset B$. Then “$a?{\in\in}B$”
means “there is a binary function $(\\#?{\in\in}B)\colon A\to\textsf{y/n}$,
and $a?{\in\in}B$ is the value of that function on $a$”. Officially the
statement itself does not include an assertion about its value, but it is
common to omit “is ‘yes’ ” when the context doesn’t make sense otherwise. For
example if $h\colon B\to\textsf{y/n}$ is a binary function on a set then the
collection of elements it identifies is traditionally written $\\{a\in B\mid
h[a]\\}$, rather than $\\{a\in B\mid h[a]=\textsf{yes}\\}$.

#### Examples

Examples relevant to set and generator theory include:

  1. (1)

“$a\,!{\in\in}A$” is read as “it is known that $a$ is an output of the
generator ${\in\in}A$”.

  2. (2)

“$a{\;!\\!\\!=\,}b$” is read as “ $a$ is known to be the same as $b$” (see
below for “same as”);

  3. (3)

“$!\exists\,a\mid(\dots)$” is read as “it is known that there exist an element
$a$ such that (…) holds ”. Beware that this is not quantification in the
traditional sense, because it is not a binary function of $(\dots)$.

  4. (4)

“$!\forall a\mid\dots$” is read as “it is known that for all $a$, (…) holds”.

  5. (5)

Negative statements can be asserted, for example $a{\,!\\!\neq}b$ asserts that
$a$ is known to be different from $b$.

  6. (6)

$!\textsf{not}$ is the denial modifier, read as “it cannot be that”. For
example $!\textsf{not}[a{\;!\\!\\!=\,}b]$ translates as “it cannot be that $a$
is known to be the same as $b$”. We understand this to be equivalent to “$a$
is known to not be the same as $b$”, and we use the corresponding notation
$a{\,!\\!\neq}b$. Similarly, $!\textsf{not}[!\exists\,a\mid(\dots)]$ is the
same as $!\\!\\!\\!\not\exists\,a\mid(\dots)]$.

We also use the common notation $:=$ for “defined by”. Note
$(:=)\Rightarrow({\;!\\!\\!=\,})$.

#### More about ‘${\;!\\!\\!=\,}$’

Officially, $a{\;!\\!\\!=\,}b$ means that $a,b$ are symbols representing a
_single_ output of a generator.

Example: This formulation of “same as” makes the usual proof of associativity
of composition work. Explicity, suppose

$\textstyle{A_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{1}}$$\textstyle{A_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{2}}$$\textstyle{A_{3}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{3}}$$\textstyle{A_{4}}$

are morphisms of generators. Then we can see $f_{3}\circ(f_{2}\circ
f_{1}){\;!\\!\\!=\,}(f_{3}\circ f_{2})\circ f_{1}$.

The traditional set-builder notation can be used to describe images of
generator morphisms, but does not encode whether or not the image is binary.
In almost all cases of interest this is automatic.

Suppose $f\colon{\in\in}B\to{\in\in}A$ is a morphism of generators. The image
of $f$ is the generator

$a{\in\in}\textsf{im}[f]\text{ means ``}!\exists\,b{\in\in}B\mid
f[b]{\;!\\!\\!=\,}a\text{''}$

together with the projection to $a{\in\in}A$. This is almost the standard set-
builder notation for images. Writing it that way, and writing the element of
$B$ explicitly as a dummy variable gives

$a{\in\in}\textsf{im}[f]:=\\{!\exists\,\\#{\in\in}B\mid
f[\\#]{\;!\\!\\!=\,}a\\}.$

Note that the use of ‘$!\exists\,$’ means this expression does _not_ define a
binary function of $a$, and an attempt to use it that way is, in general, a
usage error.

Next, suppose $p\colon A\to\textsf{y/n}$ is a binary function. We say $p$
detects the image of $f$ if

$(y{\in\in}A\textsf{\,{and}\,}p[y]=\textsf{yes})\Longleftrightarrow(!\exists\,\\#{\in\in}B\mid
f[\\#]{\;!\\!\\!=\,}y).$

If such $p$ exists we say “$f$ has binary image.” In these terms, the point of
the previous paragraph is that there are exotic generator morphisms whose
images are not binary. Fortunately, it is a theorem that if $B$ is a set then
the image is binary.

Finally, a binary function $p\colon{\in\in}A\to\textsf{y/n}$ defines a
generator with an injective morphism to $A$ whose image is detected by p. We
usually denote this generator by the same name as the binary function: define
$x{\in\in}p:=(x{\in\in}A\textsf{\,{and}\,}p[x]=\textsf{yes})$.

###  4.3. Primitive hypotheses

Primitive hypotheses are assertions that we believe are consistent, but cannot
justify by reasoning with other primitives. Instead we regard these as
experimental proposals. Extremely heavy use suggests all of these, with the
possible exception of Quantification, should be completely reliable.

#### Hypotheses

Two:

There is a generator ${\in\in}\textsf{y/n}$ such that
$\textsf{yes}{\in\in}\textsf{y/n}$, $\textsf{no}{\in\in}\textsf{y/n}$ and if
$a{\in\in}\textsf{y/n}$ then either $a{\;!\\!\\!=\,}\textsf{yes}$ or
$a{\;!\\!\\!=\,}\textsf{no}$, but not both.

Choice:

Suppose $f\colon{\in\in}A\to{\in\in}B$ is a morphism of object generators and
$f$ is known to be onto. Then there is a morphism
$g\colon{\in\in}B\to{\in\in}A$ so that $g\circ f$ is (known to be) the
identity. We refer to such $g$ as sections.

Infinity:

The natural numbers support quantification.

Quantification:

If a domain supports quantification then so does its powerset.

#### Discussion:

_About Two_ : The force of this hypothesis is that, unlike general generators,
we can tell the objects apart. This is an excluded-middle property that needs
to be made explicit because we do not require the general principle.

The names ‘yes’, ‘no’ are chosen to make it easy to remember operations
(‘and’, ‘or’, etc.). One might prefer ‘1’ and ‘0’ for indexing or connections
to Boolean algebra. We avoid ‘true’ and ‘false’ because philosophers have
attached so much baggage to them.

_About Choice_ : The term “choice” comes from the idea that if a morphism is
onto, then we can “choose” an element in each preimage. Note that in general
there is no binary-function way to determine if a morphism is onto, or if the
composition is the identity. These must be _assertions_ , as above.

The axiom of choice in the traditional setting has strong consequences that
have been extensively tested for more than a century. No contradictions have
been found, and it is now generally accepted. The above form extends the well-
established version to contexts without quantification. This extension has
implicitly been used in category theory, again without difficulty.

_About Infinity_ : Using primitive objects and hypotheses other than Infinity,
we can construct the natural numbers $\mathbb{N}$ as a logical domain. However
we cannot show that it supports quantification. The Infinity hypothesis
asserts this. This is essentially the same as the ZFC axiom “there is an
infinite set”.

_About Quantification_ The ‘powerset’ of $A$ is the generator defined by
“$f{\in\in}\textsf{P}[A]$ means ‘$f$ is a binary function $f\colon
A\to\textsf{y/n}$’ ”. Details about quantification are given in §2 and [Quinn
1], §3.4. Here we use the characterization that $A$ supports quantification if
and only if $\textsf{P}[A]$ is a logical domain. The Hypothesis asserts that
$\textsf{P}[A]$ also supports quantification, and consequently
$\textsf{P}^{2}[A]$ is a domain. Iterating shows that if $A$ supports
quantification then it supports infinite-order quantification.

The exploration in [Quinn 1] shows that the Quantification Hypothesis has
essentially no impact on everyday use. It makes the theory cleaner, easier to
develop, and more beautiful, so we assume it here.

##  5\. Categories

The definition illustrates the suitability of the primitive objects in this
theory. To show the logic and hypotheses in action we demonstrate the
existence of skeleta, and work through a formally-complete proof that if
categories $\mathcal{A},\mathcal{B}$ are small, then the functor category
$\textsf{funct}[\mathcal{A},\mathcal{B}]$ is also small.

###  5.1. Definition

A category $\mathcal{C}$ in the terminology here is:

  1. (1)

an object generator $\textsf{obj}_{\mathcal{C}}$;

  2. (2)

for every pair $A,B{\in\in}\textsf{obj}_{\mathcal{C}}$ a ‘morphism’ object
generator $\textsf{morph}[A,B]$

  3. (3)

for every triple $A,B,C{\in\in}\textsf{obj}_{\mathcal{C}}$ a ‘composition’
morphism
$*\colon\textsf{morph}[A,B]\times\textsf{morph}[B,C]\to\textsf{morph}[A,C]$;

  4. (4)

composition is associative: for every quadruple
$A,B,C,D{\in\in}\textsf{obj}_{\mathcal{C}}$ the two orders of composition give
the same morphism

$\textsf{morph}[A,B]\times\textsf{morph}[B,C]\times\textsf{morph}[C,D]\to\textsf{morph}[A,D].$

  5. (5)

and for every object $A{\in\in}\mathcal{C}$ there is an ‘identity’ morphism
$\textsf{id}_{A}{\in\in}\textsf{morph}[A,A]$ so that
$f{\in\in}\textsf{morph}[A,B]$ implies
$\textsf{id}_{A}*f{\;!\\!\\!=\,}f{\;!\\!\\!=\,}f*\textsf{id}_{B}$.

The ‘$*$’ notation for composition reverses the usual order: $f*g=g\circ f$.
We use it here because the expressions are slightly easier to write and parse.

####  5.1.1. The category OD

Object generators and their morphisms form a category. Explicitly,
$A{\in\in}\textsf{obj}_{\textsf{OD}}$ means “$A$ is an object generator”, and
$F{\in\in}\textsf{morph}_{\textsf{OD}}[A,B]$ means “$F$ is a morphism of
object generators $A\to B$”. Composition is composition of generator
morphisms, and associativity is explained in §4.2.

####  Domain and range matching

The composability criterion for morphisms can be stated as:
$f\in\textsf{morph}[A,B],g\in\textsf{morph}[C,D]$ and $B{\;!\\!\\!=\,}C$. Note
$B{\;!\\!\\!=\,}C$ is an _assertion_. In the traditional formulation ‘B=C’ is
understood to be a binary function that detects composability. Here there is
no such logical function, so this version is unavailable.

#### Functors etc.

Functors, and natural transformations of functors are defined as usual (see
[Mac Lane], §I). Categories and functors form a category.

###  5.2. Isomorphism classes

A category is ordinary if the morphism generators are all sets. The category
OD described above is not ordinary.

In this section we see that isomorphism classes of objects in an ordinary
category constitute a logical domain. Morphisms do not naturally descend to
isomorphism classes, but we can get unnatural ones using the axiom of Choice.
The result is called a “skeleton” of the category. This is a standard
construction in category theory, cf. [Mac Lane], but the set-theory
foundations used previously do not fully support the way skeleta are used.

#### Isomorphism classes

Suppose $X,Y{{\in\in}}\mathcal{A}$ are objects in a category. An isomorphism
is, as usual, a morphism $i{\in\in}\textsf{morph}[X,Y]$ such that there exists
a morphism $j{\in\in}\textsf{morph}[Y,X]$ so that the compositions $i*j$ and
$j*i$ are identities. If $i$ is an isomorphism then, again as usual, the
inverse $j$ is unique, and is also an isomorphism. Composition of isomorphisms
give isomorphisms. The isomorphisms in a category thus define a subcategory,
which we denote by $\textsf{iso}[\mathcal{A}]$.

If $\mathcal{A}$ is an ordinary category then “is there an isomorphism $X\to
Y$?” is a binary function of $X,Y$. This gives an equivalence relation on
objects, and the equivalence classes form a logical domain. We denote this by
$\textsf{obj}\mathcal{A}/\textsf{iso}$. There is a quotient morphism (of
object generators)
$q\colon\textsf{obj}\mathcal{A}\to\textsf{obj}\mathcal{A}/\textsf{iso}$.

Since functors preserve identity morphisms, they also preserve isomorphisms. A
functor $F\colon\mathcal{A}\to\mathcal{B}$ therefore induces a function
$F\colon\textsf{obj}\mathcal{A}/\textsf{iso}\to\textsf{obj}\mathcal{B}/\textsf{iso}$.
In other words $\textsf{obj}\\#/\textsf{iso}$ is a functor, from ordinary
categories and functors, to domains and functions.

###  5.3. Skeleta

A category $\mathcal{S}$ is skeletal if the objects $\textsf{obj}\mathcal{S}$
constitute a logical domain and isomorphic objects are equal. This is
equivalent to: the quotient function, from objects to isomorphism classes, is
a bijection.

A skeleton of a category $\mathcal{A}$ is a skeletal category and a functor
$s\colon\mathcal{S}\to\mathcal{A}$ that induces a bijection on isomorphism
classes of objects, and is a bijection on morphism sets.

######  Proposition.

(Existence of skeleta)

  1. (1)

Every ordinary category has a skeleton;

  2. (2)

the inclusion of a skeleton is an equivalence of categories. More precisely,
if $s\colon\mathcal{S}\to\mathcal{A}$ is the inclusion of a skeleton then
there is a functor $q\colon\mathcal{A}\to\mathcal{S}$ so that $q\circ s$ is
the identity of $\mathcal{S}$ and $s\circ q$ is naturally equivalent to the
identity of $\mathcal{A}$.

######  Corollary.

(Uniqueness) If $s_{n}\colon\mathcal{S}_{n}\to\mathcal{A}$ for $n=1,2$ are
skeleta, then there is an isomorphism of categories
$T\colon\mathcal{S}_{1}\to\mathcal{S}_{2}$ so that $s_{2}\circ T$ is naturally
equivalent to $s_{1}$.

For the Corollary, let $q_{2}\colon\mathcal{A}\to\mathcal{S}_{2}$ be the
natural inverse of (2). Then $T=p_{2}\circ s_{1}$ is the desired isomorphism.∎

The proof of the Proposition is routine, modulo use of the strong form of
‘Choice’. We give details to illustrate this.

For the first step note that the quotient
$q\colon\textsf{obj}\mathcal{(}A)\to\textsf{obj}\mathcal{(}A)/\textsf{iso}$ is
known to be a surjective morphism of generators. Choice therefore asserts that
there is a section,
$h\colon\textsf{obj}\mathcal{(}A)/\textsf{iso}\to\textsf{obj}\mathcal{(}A)$.
Define a category $\mathcal{S}$ with objects the equivalence classes
$\textsf{obj}\mathcal{(}A)/\textsf{iso}$ and morphisms
$\textsf{morph}_{\mathcal{S}}[x,y]:=\textsf{morph}_{\mathcal{A}}[h[x],h[y]]$.
It should be clear that $\mathcal{S}$ is skeletal. We get a functor
$s\colon\mathcal{S}\to\mathcal{A}$ by the section $h$ on objects, and the
identity on morphisms. It should be clear that this is a skeleton.

The next step is to extend the quotient function
$p\colon\textsf{obj}\mathcal{(}A)\to\textsf{obj}\mathcal{(}A)/\textsf{iso}=\textsf{obj}\mathcal{(}S)$
to a functor. To begin, consider the generator with objects $(a,\theta)$,
where $a$ is an object in $\mathcal{(}A)$ and $\theta$ is an isomorphism
$a\simeq h[q[a]]$. The forgetful morphism from this to
$\textsf{obj}\mathcal{(}A)$ is onto, so again we can chose a section. Denote
this by $a\mapsto(a,\theta_{1}[a])$. We tidy this up a bit. Define
$\theta_{2}$ by

$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\theta[a]}$$\textstyle{h[a]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\theta[h[a]]^{-1}}$$\textstyle{h[a].}$

Then $\theta_{2}$ has the benefit that it takes an image object $h[b]$ to
$(h[b],\textsf{id})$. Note that we cannot get $\theta_{2}$ by saying “for
objects in the image of $h$, define $\theta_{2}[h[a]]:=(h[a],\textsf{id})$ and
extend randomly to other objects”. For this to be valid we would need a binary
function on $\textsf{obj}\mathcal{(}A)$ that detects the image of $h$, and
there is generally no such function.

Now extend $q$ to morphisms by: for $f\colon a\to b$, $q[f]$ is the
composition

$\textstyle{h[q[a]]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\quad\theta_{2}[a]^{-1}}$$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\theta_{2}[b]\quad}$$\textstyle{h[q[b]]}$

Recall that this is a morphism in $\mathcal{S}$ because $h$ is the identity on
morphisms.

The proof is completed by observing that $q$ is a functor; $q\circ
h=\textsf{id}[\mathcal{S}]$; and $\theta_{2}$ is a natural equivalence $h\circ
q\simeq\textsf{id}[\mathcal{A}]$. ∎

###  5.4. Size of categories

Traditionally, a category is “small” if the collection of all objects is a
set, and “large” otherwise. We expand this terminology a bit to help track
things of size $\mathbb{W}$.

######  Definition.

Suppose $\mathcal{A}$ is a category. Then we say $\mathcal{A}$ is

  1. (1)

small if $\textsf{obj}[\mathcal{A}]/\textsf{iso}$ is a set;

  2. (2)

large if $\textsf{obj}[\mathcal{A}]/\textsf{iso}$ is not a set; and

  3. (3)

almost small if $\textsf{obj}[\mathcal{A}]/\textsf{iso}$ is bijective with
$\mathbb{W}$.

#### Examples

The category of sets and functions is almost small, but not small: the
cardinality function $\textsf{obj}_{\textsf{Set}}/\textsf{iso}\to\mathbb{W}$
is a bijection. If $k\in\mathbb{W}$ is a cardinal then the subcategory of sets
of cardinality less than $k$ is small.

#### Skeletal categories

Suppose $\mathcal{K}$ is ordinary and skeletal. Let
$\textsf{morph}[\mathcal{K}]$ denote the union of
$\textsf{morph}_{\mathcal{K}}[A,B]$ over all pairs of objects
$A,B\in\textsf{obj}[\mathcal{K}]$. There is a projection
$\textsf{morph}[\mathcal{K}]\to\textsf{obj}[\mathcal{K}]\times\textsf{obj}[\mathcal{K}]$
and, because $\mathcal{K}$ is ordinary, point preimages are sets. The results
in §3 give:

######  Proposition.

Suppose $\mathcal{K}$ is skeletal, then

  1. (1)

$\textsf{morph}[\mathcal{K}]$ is a logical domain;

  2. (2)

If $\mathcal{K}$ is small then $\textsf{morph}[\mathcal{K}]$ is a set; and

  3. (3)

If $\mathcal{K}$ is almost small, then there is a bijection
$\textsf{morph}[\mathcal{K}]\simeq\mathbb{W}$.

###  5.5. Functor categories

######  Proposition.

suppose $\mathcal{A}$ is small. Then

  1. (1)

if $\mathcal{B}$ is small then so is the functor category
$\textsf{funct}[\mathcal{A},\mathcal{B}]$; and

  2. (2)

if $\mathcal{B}$ is small or almost small then so is the functor category

In (2) note the possibility that the functor category is small even if
$\mathcal{B}$ is large.

Functors are the objects of the functor category, and natural equivalences are
the isomorphisms. Thus we want to show that natural equivalence classes of
functors has the size indicated.

First, compositions with equivalences induce equivalence of functor
categories. Existence of skeleta therefore reduces the problem to skeletal
categories. Suppose $\mathcal{A},\mathcal{B}$ are skeletal, with $\mathcal{A}$
small. Then a functor induces a function of total morphism domains
$\textsf{morph}[\mathcal{A}]\to\textsf{morph}[\mathcal{B}]$, and
$\textsf{funct}[\mathcal{A},\mathcal{B}]\subset\textsf{fn}[\textsf{morph}[\mathcal{A}],\textsf{morph}[\mathcal{B}]]$.
If $\mathcal{B}$ is small then both morphism domains are sets, so the domain
of functors is also a set. This completes case (1).

If $\textsf{obj}[\mathcal{B}]/\textsf{iso}$ is bijective to $\mathbb{W}$ then
so is $\textsf{morph}[\mathcal{B}]$, and so is the function domain
$\textsf{fn}[\textsf{morph}[\mathcal{A}],\textsf{morph}[\mathcal{B}]]$. The
functors are thus a subdomain of something bijective to $\mathbb{W}$ so either
small or minimally large . ∎

We caution, again, that there is no binary function that distinguishes between
subdomains of $\mathbb{W}$ that are sets and those bijective to $\mathbb{W}$.
This completes the goals of this section.

##  6\. Relationship to traditional set theory

A ZFC set theory consists of a universe of possible elements $U$, and a
membership pairing $\in\colon U\times U\to\textsf{y/n}$. A set is a binary
function $U\to\textsf{y/n}$ of the form $(\\#\,\in\,x)$ for some $x\in U$. In
other words, ‘$\in$’ gives a parameterization of sets by elements. Set-
theorists often suppress the parameterization and say “elements of sets are
again sets”. Many people find this formulation, and notations that follow it,
obscure.

###  6.1. Unions in ZFC

There is no direct analog of the Proposition in 2.2 because ZFC provides no
way to identify sets among more general objects. Instead we consider, as in
the Corollary, a collection of (ZFC) sets indexed by a (ZFC) set. In fact the
exact analog of the Corollary is false in most ZFC theories. To see what goes
wrong we trace through an attempted proof, then give a counterexample.

The Axiom of Union in ZFC is ([Jech], 1.4): suppose $Y\subset U$ is a set.
Then the union of the corresponding sets, $\cup_{b\in Y}(\\#\,\in\,b)$ is a
set. To relate this to the situation above, note that the assumption that each
$p^{-1}[b]$ is a set means there is an element $x_{b}\in U$ so that
$p^{-1}[b]=(\\#\,\in\,x_{b})$. Therefore $C$ is the union of sets
$(\\#\,\in\,x_{b})$, indexed by $b\in B$. To apply the Axiom of Union we must
see that the union of single-element sets $\widehat{B}=\cup_{b\in
B}\\{x_{b}\\}$ is a set. Note that the correspondence $b\mapsto x_{b}$ gives a
bijection (at least in the relaxed sense), $B\to\widehat{B}$.

The Axiom of Replacement ([Jech], 1.7) asserts that if $B$ is a set and $B\to
U$ is a function given by a first-order logical formula, then the image is a
set. To apply this to the assignment $b\mapsto x_{b}$ we would need to know
that it is given by a formula. Putting this together gives, for a model of
ZFC: if $B$ is a set in the model, and there is an collection of sets $A_{b}$
indexed by $b\in B$ and obtained by a “first-order logical process” then the
union is a set in the model.

Without the first-order condition this is false: [Quinn 1], 6.4, asserts that
If a ZFC theory is not a truncation of relaxed set theory, there is a relaxed
bijection $g\colon B\to X$ with $B$ a set in the theory and $X$ not a set in
the theory. Note $X$ is the union of single-element sets $g[b]$, indexed by
the ZFC set $B$.

###  6.2. The Increasing Union Axiom

This is supposed to implement Gödel’s idea about a “missing axiom” of set
theory.

#### Axiom

Suppose $A$ is well-ordered, unbounded, and for each $a\in A$ a subset
$W_{a}\subset(\\#<a)$ is given, such that if $b\leq a$ then
$W_{b}=W_{a}\cap(\\#<b)$. _Then_ the union $\cup\\{W_{b}\mid b\in A\\}$ is a
set.

Explicitly the union consists of $x\in A$ such that for $a>x$, $x\in W_{a}$.
This can be understood either as “for every $a>x$” or “there exists $a>x$”;
the intersection condition implies these are equivalent.

######  Proposition.

A ZFC set theory is a truncation of the maximal theory if and only if it
satisfies the Increasing Union Axiom.

#### Proof

We use the temporary notation $\Sigma$ for the given theory, and $\Omega$ for
the maximal one. If $\Sigma$ is a truncation of $\Omega$ then the axiom is a
very special case of the union theorem.

For the converse we start with: $\Sigma$ is _not_ a truncation if and only if
there is a $\Sigma$-set that contains an non $\Sigma$-set. This is essentially
what is meant by “not a truncation”. Suppose, then, that $X\subset A$ is not a
$\Sigma$ set. $A$ is well-ordered, so there is a minimal $a$ so that $(\\#<a)$
contains a non-$\Sigma$ set $X$. Define, for $b<a$, $W_{b}:=X\cap(\\#<b)$. By
minimality of $a$, each $W_{b}$ is a set. This sequence therefore satisfies
the hypotheses of the Increasing union axiom, but not the conclusion, as
required. ∎

## References

  * [Jech] Thomas J. Jech: _Set theory – 3rd Millennium ed, rev. and expanded._ Springer monographs in mathematics (2002) ISBN 3-540-44085-2
  * [Mac Lane] Saunders Mac Lane: _Categories for the Working Mathematician_ Springer Graduate Texts in Mathematics 5 (1971)
  * [Quinn 1] Frank Quinn _Object generators 1: set theory_


# Heavy Neutrino searches through Double-Bang Events at Super-Kamiokande,
DUNE, and Hyper-Kamiokande

M.C. Atkinson  TRIUMF, Vancouver, BC V6T 2A3, Canada<EMAIL_ADDRESS>Pilar Coloma  Instituto de Fisica Teorica UAM/CSIC, Calle Nicolas Cabrera
13-15, Universidad Autonoma de Madrid, 28049 Madrid, Spain
<EMAIL_ADDRESS>Ivan Martinez-Soler
<EMAIL_ADDRESS>Fermi National Accelerator Laboratory,
Batavia, IL 60510, USA  Northwestern University, Evanston, IL 60208, USA
Colegio de Física Fundamental e Interdisciplinaria de las Américas (COFI), 254
Norzagaray street, San Juan, Puerto Rico 00901.  Noemi Rocco  Fermi National
Accelerator Laboratory, Batavia, IL 60510, USA<EMAIL_ADDRESS>Ian M.
Shoemaker<EMAIL_ADDRESS>Center for Neutrino Physics, Department of
Physics, Virginia Tech University, Blacksburg, VA 24601, USA

###### Abstract

A variety of new physics scenarios allows for neutrinos to up-scatter into a
heavy neutral lepton state. For a range of couplings and neutrino energies,
the heavy neutrino may travel some distance before decaying to visible final
states. When both the up-scattering and decay occur within the detector
volume, these “double bang” events produce distinctive phenomenology with very
low background. In this work, we first consider the current sensitivity at
Super-Kamiokande via the atmospheric neutrino flux, and find current data may
already provide new constraints. We then examine projected future sensitivity
at DUNE and Hyper-Kamiokande, including both atmospheric and beam flux
contributions to double-bang signals.

††preprint: IFT-UAM/CSIC-21-59, FERMILAB-PUB-21-239-T, NUHEP-TH/21-04

##  I Introduction.

The nature of neutrino masses remains mysterious and requires physics beyond
the Standard Model (SM) of particle physics. One of the simplest scenarios
leading to the generation of light neutrino masses invokes right-handed
sterile neutrinos (also known as heavy neutral leptons), $N$, which are
singlet states under the SM gauge interactions. In this case, the neutrino
mass Lagrangian reads

$\mathcal{L}_{mass}^{\nu}\supset
Y_{\nu}\overline{L}_{L}\tilde{\phi}N_{R}+\frac{1}{2}M_{R}\overline{N_{R}^{c}}N_{R}\,+\textrm{h.c.}\,,$
(1)

where $\tilde{\phi}\equiv i\sigma_{2}\phi^{*}$, $N_{R}^{c}\equiv
C\bar{N}_{R}^{T}$ is the charge conjugate of $N_{R}$ and we have omitted
flavor and mass indices. This is the well-known Type I Seesaw
LagrangianMinkowski:1977sc ; GellMann:1980vs ; Mohapatra:1979ia . Upon
electroweak symmetry breaking, the left- and right-handed neutrinos mix, and
the sterile neutrinos effectively inherit a reduced coupling to the weak force
through the mixing matrix parameters. Therefore, in this scenario a HNL could
be obtained using the same production mechanisms as for the SM neutrinos,
provided that its mass is below that of the parent meson. The mixing mediates
both the production as well as the decay of the heavy neutrino back into SM
particles and, being weakly coupled, the HNL will be typically long-lived.

It should be kept in mind that although the Lagrangian in Eq. (1) implies a
Majorana HNL, the conclusions from this study hold regardless of its
Dirac/Majorana nature. The mass of the HNL is obtained after diagonalization
of the mass Lagrangian and will eventually depend on the values of the Yukawa
couplings and the Majorana mass in Eq. (1). Here, for simplicity, we follow a
phenomenological approach and denote as $U$ the leptonic mixing matrix, and
$m_{N}$ the mass of the HNL. As we will see, mixing at the level $|U|^{2}\sim
10^{-2}-10^{-3}$, lead to HNL decay lengths around the size of the detector.

For HNL masses in the GeV range, fixed-target experiments set the best
constraints on the mixing of the HNL with electron and muon neutrinos, see
e.g. Refs. Atre:2009rg ; Bryman:2019ssi ; Bryman:2019bjg ; Drewes:2015iva .
Moreover the DUNE near detector complex should be able to significantly
improve on these Ballett:2019bgd ; Berryman:2019dme ; Coloma:2020lgy ;
Breitbach:2021gvv . However, if the HNL mixes primarily with tau neutrinos
then its existence is much more difficult to probe using this approach: the
HNL would have to be produced either in $\tau$ decays or in the decays of
heavy mesons with a sizable branching ratio into $\nu_{\tau}$ (such as $D$ or
$D_{s}$), which have a much smaller production cross section than lighter
mesons. For $m_{N}\sim\mathcal{O}(0.1-10)~{}\textrm{GeV}$ the strongest
constraints come from the DELPHI Abreu:1996pa  and CHARM Orloff:2002de
experiments, but values of $|U_{\tau 4}|^{2}\sim 10^{-2}$ are still allowed
for a heavy neutrino with mass around
$m_{N}\sim\mathcal{O}(400)~{}\textrm{MeV}$ Atre:2009rg . Note that light HNLs
below the CHARM bound, can be probed via terrestrial up-scattering followed by
HNL decay in large volume detectors Plestid:2020ssy .

However, it is important to stress that this is not the only possibility for a
HNL to interact with the visible sector. For example, the active and HNL
states may be coupled via a transition dipole moment. At low energies this is
described by an effective operator

$\mathcal{L}^{\nu}_{{\rm
dipole}}\supset\mu(\bar{\nu}_{L}\sigma^{\mu\nu}N)F_{\mu\nu}+\textrm{h.c.}\,,$
(2)

where $\mu$ is a coefficient with units $({\rm mass})^{-1}$ which controls the
strength of the interaction, while $F_{\mu\nu}$ is the electromagnetic field
strength tensor, and
$\sigma^{\mu\nu}\equiv\left[\gamma^{\mu},\gamma^{\nu}\right]$.

Compared with their electron and muon counterparts, tau neutrinos are more
challenging to produce since they come from either $\tau$ or heavy meson
decays, as outlined above. Consequently, the resulting bounds on transition
magnetic moments which dominantly couple the HNL to the $\nu_{\tau}$ are
significantly weaker than those coupling to either $\nu_{e}$ or $\nu_{\mu}$
Gninenko:2009ks ; Coloma:2017ppo ; Magill:2018jla ; Shoemaker:2018vii ;
Shoemaker:2020kji ; Brdar:2020quo ; Plestid:2020vqf ; Vergani:2021tgc .

Previously, in Ref. Coloma:2017ppo  it was shown that both such models can be
probed using double-bang (DB) events at IceCube with atmospheric neutrinos.
These DB events occur when an incoming neutrino $\nu$ scatters on a target $T$
in the detector:

$\displaystyle\nu+T\longrightarrow{\rm cascade}~{}+~{}$ $\displaystyle N$ (3)
$\displaystyle\hookrightarrow$ $\displaystyle N\rightarrow{\rm cascade}$ (4)

In this paper, we extend the work of Ref. Coloma:2017ppo  by computing the DB
sensitivity at Super-Kamiokande (SK), DUNE, and Hyper-Kamiokande (HK). Despite
their smaller detector volume when compared to Icecube/DeepCore, they offer
several advantages:

Sensitivity to smaller separation between the two bangs.

Both liquid Argon time projection chambers (LAr TPC) and water Cherenkov (WC)
detectors have a much better spatial resolution, which at Icecube/DeepCore is
eventually limited by the spacing between the Digital Optical Modules in the
ice.

Lower-energy sensitivity.

IceCube/DeepCore lacks sensitivity to showers with energies below a few GeV,
while WC are a priori sensitive to the production of any charged particles as
long as they lie above Cherenkov threshold. LAr TPCs are also sensitive to
neutrino interactions with energies as low as 50 MeV Acciarri:2014gev ;
Acciarri:2018myr . Since the flux of atmospheric neutrinos rises steeply at
low energies, the total number of events will be comparatively larger on a
per-detector-mass basis.

Availability of neutrino beam data.

Besides the atmospheric neutrino sample, at SK, HK and DUNE an additional
event sample is available from the use of a conventional neutrino beam. In
addition to atmospheric neutrino events, we also include the beam data in our
study.

The manuscript is structured as follows. Our computation of the cross section
for the interaction vertex is described in Sec. II for both scenarios
discussed above. Section III contains some relevant details regarding the
lifetime of the HNL and the branching ratio into visible states, while the
more technical details used in the computation of the signal event rates are
discussed in Sec. IV. Section V contains an explanation of the expected
background event rates, while we present our results in Sec. VI and summarize
and conclude in Sec. VII.

##  II Cross section calculation

In this section we describe our derivation of the interaction cross section in
the quasi-elastic (QE) regime. Our calculation for the cross section in the
deep inelastic scattering (DIS) regime is very similar to the one performed in
Ref. Coloma:2015kiu , with the difference that in the present work the HNL
mass has been properly included in the computation.

We consider the scattering of a neutrino ($\nu_{\ell}$) or an anti-neutrino
($\bar{\nu}_{\ell}$) off a nuclear target and we denote by
$k=(E_{\nu},\mathbf{k})$ and $k=(E^{\prime}_{\nu},\mathbf{k}^{\prime})$ the
momentum of the initial and outgoing lepton. The double-differential cross
section for a neutral-current (NC) process can be written as Shen:2012xz ;
Benhar:2006nr

$\Big{(}\frac{d\sigma}{dE^{\prime}_{\nu}d\Omega^{\prime}}\Big{)}_{\nu_{\ell}/\bar{\nu}_{\ell}}=\frac{G^{2}}{4\pi^{2}}\,k^{\prime}E^{\prime}\,L_{\mu\nu}R^{\mu\nu}\,,$
(5)

where $G=G_{F}\cos\theta_{c}$ with $\cos\theta_{c}=0.97425$ Nakamura:2010zzi
and for the Fermi coupling constant we use $G_{F}=1.1803\times 10^{-5}$
Herczeg:1999dx . Performing the Lorentz contraction of the leptonic and
hadronic tensor of Eq. (5), we obtain

$\displaystyle\Big{(}\frac{d\sigma}{dE^{\prime}_{\nu}d\Omega^{\prime}}\Big{)}_{\nu/\bar{\nu}}$
$\displaystyle=\frac{G_{F}^{2}\cos^{2}\theta_{c}}{4\pi^{2}}\frac{k^{\prime}}{2E_{\nu}}\left[\hat{L}_{CC}R_{CC}+2\hat{L}_{CL}R_{CL}\right.$
$\displaystyle\left.+\hat{L}_{LL}R_{LL}+\hat{L}_{T}R_{T}\pm
2\hat{L}_{T^{\prime}}R_{T^{\prime}}\right]\ .$ (6)

We define $q$ and $Q$ as

$\displaystyle q$ $\displaystyle=k-k^{\prime}=(\omega,{\bf q})\,,\quad
Q=k+k^{\prime}=(\Omega,{\bf Q})\,.$ (7)

Taking the three-momentum transfer along the $z$ axis and the total three-
momentum in the $x-z$ plane, we write the leptonic kinematical factors as

$\displaystyle\hat{L}_{CC}$ $\displaystyle={\Omega}^{2}-q_{z}^{2}-M_{N}^{2},\
\ \ \ \ \ \ \ \hat{L}_{CL}=(-\Omega Q_{z}+\omega q_{z})$
$\displaystyle\hat{L}_{LL}$ $\displaystyle={Q_{z}}^{2}-\omega^{2}+M_{N}^{2},\
\ \ \ \ \ \ \hat{L}_{T}=\frac{{Q_{x}}^{2}}{2}-q^{2}+M_{N}^{2}$
$\displaystyle\hat{L}_{T^{\prime}}$ $\displaystyle=\Omega q_{z}-\omega
Q_{z}\,,$ (8)

with $M_{N}^{2}=k^{\prime\,2}$ the mass of the outgoing neutrino. The five
electroweak response functions correspond to different components of the
hadron tensor

$\displaystyle R_{CC}$ $\displaystyle=R^{00},\ \ \ \ \ \ \ \
R_{CL}=-\frac{1}{2}(R^{03}+R^{30})$ $\displaystyle R_{LL}$
$\displaystyle=R^{33},\ \ \ \ \ \ \ R_{T}=R^{11}+R^{22}$ $\displaystyle
R_{T^{\prime}}$ $\displaystyle=-\frac{i}{2}(R^{12}-R^{21})\,.$ (9)

The hadronic tensor describes the transition between the initial and final
nuclear states $|\Psi_{0}\rangle$ and $|\Psi_{f}\rangle$, with energies
$E_{0}$ and $E_{f}$. For nuclei of spin-zero, it can be written as

$\displaystyle R^{\mu\nu}({\bf
q},\omega)=\sum_{f}\langle\Psi_{0}|j^{\mu\,\dagger}({\bf
q},\omega)|\Psi_{f}\rangle\langle\Psi_{f}|j^{\nu}({\bf
q},\omega)|\Psi_{0}\rangle\delta(E_{0}+\omega-E_{f})\,.$ (10)

where we sum over all hadronic final states and $J^{\mu}({\bf q},\omega)$ is
the nuclear current operator. The one-body current operator is the sum of
vector (V) and axial (A) terms NC processes and it can be written as

$\displaystyle j^{\mu}=(J^{\mu}_{V}+J^{\mu}_{A})$ $\displaystyle
J^{\mu}_{V}={\cal F}_{1}\gamma^{\mu}+i\sigma^{\mu\nu}q_{\nu}\frac{{\cal
F}_{2}}{2M}$ $\displaystyle J^{\mu}_{A}=-\gamma^{\mu}\gamma_{5}{\cal F}_{A}\
.$ (11)

The single-nucleon form factors relevant to the NC neutrino-nucleon scattering
${\cal F}^{N}_{i}$ (i=1,2) and $N=p,n$ read

$\displaystyle{\cal F}^{N}_{i}=$
$\displaystyle\pm\frac{1}{2}(F_{i}^{p}-F_{i}^{n})-2\sin^{2}\theta_{W}F^{N}_{i}\,,$
$\displaystyle{\cal F}_{A}=$ $\displaystyle\frac{1}{2}(F_{A}^{s}\pm F_{A})\,,$
(12)

where the + (-) sign is for the proton (neutron), and $\theta_{W}$ is the
Weinberg angle ($\sin^{2}\theta_{W}=0.2312$ Nakamura:2010zzi ). We assumed a
dipole parametrization for the axial form factor ${\cal F}_{A}=F_{A}$

$\displaystyle F_{A}$ $\displaystyle=\frac{g_{A}}{(1-q^{2}/M_{A}^{2})^{2}}\ ,$
(13)

where the nucleon axial-vector coupling constant is taken to be $g_{A}=1.2694$
PDG  and the axial mass $M_{A}=1.049$ GeV. The form factors $F_{A}^{s}$ is
introduced to describe the strangeness content of the nucleon. Following Ref.
Leitner:2008ue , we set

$\displaystyle F_{A}^{s}$
$\displaystyle=-\frac{0.15}{(1-q^{2}/M_{A}^{2})^{2}}\,.$ (14)

The second reaction mechanism we consider is the heavy neutrino production via
a transition magnetic moment

$\displaystyle\Big{(}\frac{d\sigma}{dE^{\prime}_{\nu}d\Omega^{\prime}}\Big{)}_{\nu_{\ell}/\bar{\nu}_{\ell}}=\frac{1}{4\pi}\frac{\alpha\mu_{\rm
tr}^{2}}{Q^{4}}\frac{E_{\nu}^{\prime}}{E_{\nu}}\,L_{\mu\nu}R^{\mu\nu}\,,$ (15)

where $\alpha=1/137$ is the electromagnetic fine structure constant, and
$\mu_{\rm tr}=0.296$ MeV-1 is the neutrino transition magnetic moment. In this
case we can write the contraction between the lepton and the hadron tensor as

$\displaystyle L_{\mu\nu}R^{\mu\nu}=$
$\displaystyle\frac{W_{1}}{2}(2M_{N}^{2}-Q^{2})(M_{N}^{2}+Q^{2})+\frac{W_{2}}{2}\big{[}E_{\nu}^{2}(Q^{2}-3M_{N}^{2})+2E_{\nu}E^{\prime}_{\nu}(M_{N}^{2}+Q^{2})$
$\displaystyle+(E_{\nu}^{\prime}-M_{N})(E_{\nu}^{\prime}+M_{N})(M_{N}^{2}+Q^{2})\big{]}$
(16)

where

$\displaystyle W_{1}$ $\displaystyle=\frac{(R^{11}+R^{22})}{2}$ $\displaystyle
W_{2}$ $\displaystyle=\frac{Q^{4}}{|{\bf q}|^{4}}R^{00}+\frac{Q^{2}}{|{\bf
q}|^{2}}\frac{(R^{11}+R^{22})}{2}$ (17)

with $M_{N}$ the mass of the right handed neutrino. The general expression of
the hadron tensor is given in Eq. (10). Since the exchanged boson is a
$\gamma$, for the hadron vertex, the current operator coincides with the
electromagnetic one

$\displaystyle j^{\mu}_{\rm
EM}={\mathcal{F}}_{1}\gamma^{\mu}+i\sigma^{\mu\nu}q_{\nu}\frac{{\mathcal{F}}_{2}}{2m_{N}}\,.$
(18)

The isoscalar (S) and isovector (V) form factors, ${\mathcal{F}}_{1}$ and
${\mathcal{F}}_{2}$, are given by combination of the Dirac and Pauli ones,
$F_{1}$ and $F_{2}$, as

$\displaystyle{\mathcal{F}}_{1,2}=\frac{1}{2}[F_{1,2}^{S}+F_{1,2}^{V}\tau_{z}]$
(19)

where $\tau_{z}$ is the isospin operator and

$\displaystyle F_{1,2}^{S}=F_{1,2}^{p}+F_{1,2}^{n},\ \ \ \ \ \ \ \
F_{1,2}^{V}=F_{1,2}^{p}-F_{1,2}^{n}\,.$ (20)

### Spectral function formalism

The cross sections computed in this work have been obtained using a
factorization scheme. For large values of the energy transfer $\omega$ and
momentum transfer $|{\bf q}|$, we can factorize the hadronic final state and
provide a relativistic description of $|\Psi_{f}\rangle$ and of the current
operator. To model the dynamics of the target nucleus and account for
correlation effects we used a realistic spectral function obtained from the
non-local dispersive optical model (DOM) Mahaux91 ; Mahzoon:2014 .

Figure 1: Here we display the cross sections in the mass-mixing (left) and
transition magnetic moment (right) cases. The QE (solid) and DIS (dashed)
contributions are shown separately for representative values of the HNL
neutrino mass. Note that for the magnetic moment case, the DIS contribution
has been magnified by 10 times in order for it to be visible.

We consider only the one-body current terms and we rewrite the hadronic final
state as

$|\Psi_{f}\rangle\rightarrow|p\rangle\otimes|\psi_{f}^{A-1}\rangle$ (21)

where the outgoing nucleon with momentum $|{\bf p}|$ and energy $e({\bf
p})=\sqrt{|{\bf p}|^{2}+m_{N}^{2}}$ is described in terms of a plane wave,
while $|\psi_{f}^{A-1}\rangle$ stems for the $(A-1)$-body spectator system.
The energy and momentum of the latter are obtained by energy and momentum
conservation relations

$\displaystyle E_{f}^{A-1}=\omega+E_{0}-e({\bf p})\,,\quad{\bf
P}^{A-1}_{f}={\bf q}-{\bf p}\,.$ (22)

The hadron tensor of Eq. (10) can be easily rewritten by inserting a single-
nucleon completeness relation

$\displaystyle R^{\mu\nu}=$
$\displaystyle\int\frac{d^{3}k}{(2\pi)^{3}}dES_{h}({\bf
k},E)\frac{m^{2}}{e({\bf k})e({\bf k+q})}\sum_{i}\,\langle
k|{j_{i}^{\mu}}^{\dagger}|k+q\rangle\langle
k+q|j_{i}^{\nu}|k\rangle\delta(\tilde{\omega}+e({\bf k})-e(\mathbf{k+q}))\,,$
(23)

where $m$ is the nucleon nucleon mass. In order to account for the off-
shellness of the initial nucleon, we introduced
$\tilde{\omega}=\omega-E+m-e({\bf k})$ and replace $q=(\omega,{\bf
q})\rightarrow\tilde{q}=(\tilde{\omega},{\bf q})$ in the calculation of the
hadronic tensor. The factors $m/e({\bf k})$ and $m/e({\bf k+q})$ ensure the
implicit covariant normalization of the nucleon quadri-spinors.

The spectral function, $S_{h}({\bf k},E)$ in Eq. (23), is obtained for 16O
using the DOM. This method constrains a complex self-energy $\Sigma^{*}$ using
both scattering and bound-state data of 16O Mahaux91 ; Mahzoon:2014 . The
self-energy is a complex, nonlocal, energy-dependent potential that unites the
nuclear structure and reaction domains through dispersion relations Mahaux91 ;
Mahzoon:2014 ; Dickhoff:2017 . The Dyson equation generates the single-
particle propagator, or Green’s function, $G_{h}({\bf k},E)$ from which bound-
state and scattering observables can be deduced Atkinson:2020 . The energy
dependence of the self-energy ensures that many-body correlations manifest in
$G_{h}({\bf k},E)$, providing a description beyond that of a mean field. The
spectral function determined by $G_{h}({\bf k},E)$ in the following equation

$S_{h}({\bf k},E)=\frac{1}{\pi}\textrm{Im}G_{h}({\bf k},E)$ (24)

yields the probability density of finding a nucleon in the target nucleus with
a given momentum ${\bf k}$ and removal energy $E$.

In Fig. 1 we show representative cross sections in both the mass-mixing with
$|U_{\tau 4}|^{2}=10^{-2}$ (left panel) and magnetic moment with
$\mu=10^{-8}~{}\mu_{B}$ (right panel), where $\mu_{B}\equiv e/(2m_{e})$ stands
for the Bohr magneton.

##  III HNL decay

###  III.1 Mixing with tau neutrinos

The computation of the lifetime of the HNL in this scenario, as well as the
branching ratios into the different decay channels, is done following Ref.
Coloma:2020lgy . For a HNL with mass $m_{N}\sim\mathcal{O}(\rm{GeV})$ that
mixes primarily with $\nu_{\tau}$, the decay channels involving tau leptons
are kinematically forbidden. In this mass range the HNL will primarily decay
into two-body final states, namely, neutral mesons plus a tau neutrino. While
$N\to\nu_{\tau}\pi^{0}$ is the dominant decay channel of this type (with a
branching ratio between 20% and 30%, depending on $M_{N}$), non-negligible
branching ratios (sometimes as large as 10%) are also found for
$N\to\nu_{\tau}\rho$ and $N\to\nu_{\tau}\eta$ (see bottom panels in Fig. 1 in
Ref. Coloma:2020lgy ). Slightly smaller branching ratios are found for the
decay into the three-body fully leptonic decay channels, $N\to\nu_{\tau}ee$
and $N\to\nu_{\tau}\mu\mu$. The resulting decay length in the lab frame, for a
neutrino with energy $E_{N}$ and total decay width $\Gamma_{tot}$, is in the
ballpark

$L_{{\rm lab}}=c\tau\gamma\beta\simeq 10~{}{\rm
m}~{}\left(\frac{10^{-2}}{|U_{\tau 4}|^{2}}\right)~{}\left(\frac{0.5~{}{\rm
GeV}}{m_{N}}\right)^{5}~{}\left(\frac{E_{N}}{1~{}{\rm GeV}}\right)\,,$ (25)

where $\tau=1/\Gamma_{tot}$ is the lifetime of the HNL in its rest frame.

When computing the event rates, however, we take into account that in this
range of masses the branching ratio for the decay
$N\to\nu_{\tau}\nu_{\alpha}\nu_{\alpha}$ is dominant and would lead to an
invisible HNL decay in any neutrino detector. In order to take this into
account, our event rates are multiplied by the branching ratio into visible
decay channels

$\mathcal{B}_{vis}=1-\frac{\Gamma(N\to\nu\nu\nu)}{\Gamma_{tot}}\,.$ (26)

Figure 2 shows the branching ratio into visible states for a HNL that mixes
with tau neutrinos only, as a function of its mass.

Figure 2: Branching ratio for the decay of a HNL of mass $M_{N}$ into visible
final states, defined in Eq. 26, assuming it only mixes with tau neutrinos.

###  III.2 Magnetic Dipole Moment

In the case of the magnetic dipole coupling, for simplicity we will assume
that the mixing to light sterile neutrinos is negligible. In this case, the
operator in Eq. (2) induces the two-body decay $N\to\nu\gamma$ with the width

$\Gamma(N\rightarrow\nu\gamma)=\frac{\mu^{2}m_{N}^{3}}{16\pi}\,,$ (27)

which is the only relevant decay channel in this scenario. Thus, in this case
we have $\mathcal{B}_{vis}=1$, and the decay length in the lab frame reads

$L_{{\rm lab}}=c\tau\gamma\beta\simeq 10~{}{\rm
m}~{}\left(\frac{10^{-8}~{}\mu_{B}}{\mu}\right)^{2}~{}\left(\frac{100~{}{\rm
MeV}}{m_{N}}\right)^{3}~{}\left(\frac{E_{N}}{1~{}{\rm GeV}}\right)\,.$ (28)

##  IV Calculation of Double-Bang Event Rates

The Double-Bang (DB) signal consists on a composite signal given by the
interaction of an active neutrino (“first bang”), where a HNL is produced, and
the posterior decay of the heavy state (“second bang”) after the propagation
of a macroscopic distance. The separation between both bangs depends on the
mass of the heavy state and the decay channel into SM particles. As stated
before, our goal is to determine the present and future sensitivities to this
signal in two of the most relevant type of detectors for neutrino physics:
water Cherenkov and Liquid Argon TPC. In particular, we will consider the
present sensitivity of Super-Kamiokande (SK) and its future upgrade Hyper-
kamiokande (HK), as well as DUNE. As a neutrino source, we consider the two
largest fluxes that can be measured by those experiments: the atmospheric
neutrino flux and the neutrinos generated in an accelerator. In the case of SK
and HK, the beam experiments are called T2K and T2HK respectively.

Note that the rate of NC $\nu_{\tau}$ events at each experimental setup sets
the scale for their ability to probe HNLs. For illustration, we plot in Fig. 3
number of $\nu_{\tau}$ induced NC events at Super-K via the atmospheric flux,
and T2K and DUNE via their respective beam fluxes. From this we expect the
existing sensitivity of Super-K and the future DUNE beam sensitivity to set
the most stringent limits on HNLs.

The DB rate generated by the interaction of $\nu_{\alpha}$ which upscatter
into the heavy state, for a HNL with lifetime $c\tau$, is proportional to

$N^{\alpha}_{\rm
DB}(c\tau)=\sum_{\beta}\mathcal{B}_{vis}\\!\int\\!dE_{\nu}dc_{\theta}dE_{N}\frac{d\phi_{\nu_{\beta}}}{dE_{\nu}}P_{\beta\alpha}(E_{\nu})~{}\frac{d^{2}\sigma_{\nu_{\alpha}N}}{dE_{N}dc_{\theta}}(E_{\nu})~{}P_{d}(c\tau,E_{N})~{}V_{\rm
det}(c\tau,E_{N},c_{\theta}),$ (29)

where $E_{\nu}$ is the incident neutrino energy, while $E_{N}$ and
$c_{\theta}\equiv\cos\theta$ refer to the energy and the scattering angle of
the heavy state with respect to the incident neutrino direction. The flux of
active neutrinos is given by $\phi_{\beta}$ and it will have oscillated into
$\nu_{\alpha}$ by the time that they arrive to the detector, with a
probability $P_{\beta\alpha}$. The cross section for neutrino upscattering
into the heavy state is given by $\sigma_{\nu_{\alpha}N}$. The NC quasi-
elastic neutrino interaction is computed as described in Sec. II, for the DIS
regime, we followed Ref. Coloma:2017ppo  including the correct dependence with
the HNL mass. After propagation over a distance $L$, the HNL will decay with a
probability $P_{d}=e^{-L/L_{\rm lab}}/L_{\rm lab}\equiv P_{d}(c\tau,E_{N})$,
where $L_{\rm lab}$ depends on the specific model considered as outlined in
Sec. III. Finally, the effective volume $V_{\rm det}$ includes the probability
that the second bang takes place inside the detector, which depends on the
expected separation between the two bangs for a given value of $c\tau$ and the
boost factor.

In the case of T2K, we use the fluxes published by the collaboration
Abe:2021gky . A similar energy-dependent flux will be used for T2HK, although
we will assume a beam power of 1.3 MW Hasegawa:2018bjo ; Igarashi:2019txx
(see also e.g., Ref.Ballett:2016daj ), corresponding to $2.7\times 10^{22}$
POT in 10 years. For DUNE, we will use the collaboration flux predictions
Abi:2020evt , and a beam power of 1.2 MW that will correspond to $1.1\times
10^{22}$ POT in 10 years. While for beam calculations we consider $\nu_{\mu}$
as the initial neutrino flavor, neglecting the intrinsic contamination of the
beam, for atmospheric neutrinos we consider both $\beta=e,\mu$, according to
Honda’s table Honda:2015fha . In the case of atmospheric neutrinos, the flux
and the oscillation probability also depend on the zenith angle. We will
integrate over all the incoming neutrino directions and separations between
the “bangs” to obtain the total DB rate. Also, note that antineutrino events
will give a similar contribution to the total number of events, replacing
$\phi_{\nu_{\mu}}$, $\sigma_{\nu_{\tau}N}$ and $P_{\mu\tau}$ in Eq. (29) by
their analogous expressions for antineutrinos.

To be detected, a DB signal must happen inside the detector. The asymmetry of
the detectors in each direction implies that the effective volume of the
detector will depend on the separation between the bangs, but also on the
scattering angle. The effective detector volume has been obtained via Monte
Carlo integration, where we have included the detector geometry and the
minimum separation between bangs that can be resolved in each detector. In the
case of SK, the vertex resolution is 50 cm at 12.5 MeV and closer to 80 cm at
5 MeV Abe:2016nxk . In our simulation, we have conservatively assumed a
minimum separation of 80 cm between the two events, for all neutrino energies.
In the case of Liquid Argon TPC, the vertex resolution can be reduced to the
millimeter scale Arguelles:2019xgp . However, in this case backgrounds can
arise from several sources, as described in more detail in Sec. V. Thus, we
have conservatively set the minimum separation between the two bangs at 20 cm.

##  V Expected backgrounds

As argued in Ref. Coloma:2017ppo , the main advantage of searching for new
physics through double-bang events is that the number of background events
from SM processes is expected to be very small. Here we provide some estimates
regarding the expected background rate for LAr TPC and WC detectors, since
there are some relevant differences with respect to the case of
Icecube/DeepCore.

If the separation between the two events is above a few meters, the only
background to this search comes from coincidental events, that is, two events
taking place within the same time window $\Delta t$. Naively, for an
atmospheric neutrino experiment the event rates can be estimated as in Ref.
Coloma:2017ppo :

$R_{atm}\sim\frac{N_{atm}(N_{atm}-1)}{2}\left(\frac{\Delta t}{T}\right)^{2},$
(30)

where $N_{atm}$ is the number of atmospheric neutrino events which take place
within a time period $T$. Our computation of the number of atmospheric events
in each detector gives $N_{atm}^{DUNE}\simeq 1.2\times 10^{3}~{}{\rm
yr}^{-1}$, $N_{atm}^{SK}\simeq 8\times 10^{2}~{}{\rm yr}^{-1}$, and
$N_{atm}^{HK}\simeq 6.6\times 10^{3}~{}{\rm yr}^{-1}$. Thus, assuming $\Delta
t=10$ s (which is likely very conservative) we find $R_{atm}^{\rm
DUNE}=7.2\times 10^{-8}~{}{\rm yr}^{-1}$ , $R_{atm}^{\rm SK}=3.2\times
10^{-8}~{}{\rm yr}^{-1}$, and $R_{atm}^{\rm HK}=2.2\times 10^{-6}~{}{\rm
yr}^{-1}$ for DUNE, SK and HK, respectively.

In the case of the beam, the number of coincidental events within the same
beam spill can be estimated in a similar fashion. In this case, the much
smaller time window, which is given by the beam spill width (for example,
$\Delta t=10~{}\mu\textrm{s}$ in the case of DUNE Abi:2018dnh ), leads to a
negligible background level, well below that of atmospheric neutrinos. We find
this to be the case for the coincidence of two beam events within the same
spill, as well as for the case where one event comes from the beam and the
other is an atmospheric neutrino.

However, once the separation between the two events is smaller than $\sim$50
cm additional backgrounds arise. For example, events in which a neutron is
knocked out of the nucleus can exhibit a double-bang-like event topology,
depending on the energy-dependent mean free path of the neutron. Similarly,
photons can take some time to convert to electron/positron pairs and therefore
NC events with vertex activity and a $\pi^{0}$ in the final state could a
priori constitute a background as well (for example, the typical conversion
distance for the two photons coming from a $\pi^{0}$ decay in LAr is 24 cm
Adams:2018sgn ). Thus, in our analysis we impose a minimum separation between
the two events of 20 cm for the DUNE detector.

##  VI Results

As a rough estimate of the DB sensitivity, one can expect the number of
$\nu_{\tau}$-induced DB events to scale as

$N^{\tau}_{DB}\simeq N_{\nu_{\tau}}^{NC}(E_{\nu}\gtrsim
m_{N})\times\frac{V_{{\rm
det}}}{V_{0}}\frac{\sigma_{\nu_{\tau}N}}{\sigma^{NC}_{SM}}\times\mathcal{B}_{vis}\times
P_{d}\,,$ (31)

where $N_{\nu_{\tau}}^{NC}(E_{\nu}\gtrsim m_{N})$ is the number of NC
$\nu_{\tau}$ events with energies above the kinematic threshold for
$\nu_{\tau}\rightarrow N$ up-scattering, $\sigma^{NC}_{SM}$ is the neutrino NC
interaction cross section in the SM, and $V_{0}$ is the full (fiducial) volume
of the detector.

Let us first examine the mass-mixed HNL case at DUNE via the beam flux. For
illustration, let us assume $m_{N}$ = 0.5 GeV. From our calculations, we find
that the number of $\nu_{\tau}$-induced NC events above the kinematic
threshold is $N_{\nu_{\tau}}^{NC}(E_{\nu}\gtrsim m_{N})\simeq 4\times 10^{3}$,
see Fig. 3.

Figure 3: Total number of standard NC $\nu_{\tau}$ interactions with neutrino
energies above a given value $E_{0}$, for the atmospheric flux at SK, as well
as for the T2K and for the DUNE beams.

Next, inspection of Fig. 1 reveals that the total up-scattering cross section
at this HNL mass is reduced by about a factor of $\sim(1/3)|U_{\tau 4}|^{2}$
compared to the SM case. Thus Eq. (31) implies that we should expect
sensitivities to the mixing angle, $|U_{\tau 4}|^{2}\gtrsim 10^{-3}$ at best
(of course, the visible branching ratio, effective detector volume, and
probability to decay will reduce this sensitivity somewhat). Our numerical
results for the mixing scenario are shown in Fig. 4 for DUNE, Super-K, and
Hyper-K sensitivity in Fig. 4. Upon inspection of the DUNE sensitivity in the
left panel of Fig. 4, we see that the more detailed estimate finds that
$|U_{\tau 4}|^{2}\gtrsim 3\times 10^{-3}$ can be reached at $m_{N}=0.5$ GeV.
One can also see that this is consistent with the requirement that the decay
occurs within the detector volume, see Eq. (25).

Figure 4: Iso-contours indicating the regions where more than one DB event is
expected, for the HNL scenario via mixing with $\nu_{\tau}$. Results are shown
for DUNE (left), Super-K (center), and Hyper-K (right), for the atmospheric
(blue) and nominal beam (red) fluxes separately. The solid curves for the
Super-K and T2K sensitivity correspond to current exposures. The shaded
regions indicate the regions of the parameter space disfavored by CHARM
Orloff:2002de  and DELPHI Abreu:1996pa  data, taken from Ref. Atre:2009rg .

A similar estimate can be performed in the dipole interaction case. From Fig.
1 we see that for a HNL with mass $m_{N}=0.6$ GeV the cross section with
$\mu=10^{-8}~{}\mu_{B}$ is about 10 times larger than the SM cross section.
Thus using $N_{\nu_{\tau}}^{NC}(E_{\nu}\gtrsim m_{N})\simeq 4\times 10^{3}$
with Eq. (31) roughly suggests that $\mu\gtrsim 10^{-10}~{}\mu_{B}$ may be
within reach for a HNL of mass $m_{N}=0.5$ GeV. However in this case one can
see from the decay length requirement that a value closer to $\mu\gtrsim
10^{-9}~{}\mu_{B}$ is necessary to decay within the detector volume while
still being moderately relativistic, see Eq. (28). This roughly agrees with
the results from our numerical calculation for the sensitivity using the DUNE
nominal beam, shown in Fig. 5. While we have discussed the DUNE case as an
example, the same reasoning can be applied to the other cases as well.

Figure 5: Iso-contours indicating the region of parameter space where more
than one DB event is expected, for the transition magnetic moment between
$\nu_{\tau}$ and $N$. Results are shown for DUNE (left), Super-K (center), and
Hyper-K (right). Same plotting conventions as in Fig. 4. The shaded gray areas
indicate the regions currently disfavored by Borexino Bellini:2014uqa , DONUT
Schwienhorst:2001sj , and ALEPH Decamp:1991uy ; Gninenko:2010pr  data. The
shaded purple area indicates the region leading to delayed neutrino-photon
decoupling in the early universe Coloma:2017ppo .

Notice that the dominance of the sensitivity for SK atmospheric and the DUNE
beam that was already apparent in Fig. 3 is confirmed in Figs. 4 and 5.
Moreover, DUNE’s dominance at the level of $\nu_{\tau}$ NC events occurs for
neutrino energies between roughly $\sim 2-20$ GeV. This explains why the DUNE
beam sensitivity to HNLs can exceed the atmospheric Super-K sensitivity at
larger HNLs masses, as seen in Figs. 4 and 5.

Lastly, in Fig. 6 we show that DUNE’s LAr near detector can also be sensitive
to DB events. In this case, the large $\nu_{\mu}$ flux at the near detector
can allow for $\nu_{\mu}-N$ transition moments to be very well probed, and in
fact push into new parameter space which is currently unconstrained. We note
that MiniBooNE Magill:2018jla  also constrains a small window of parameter
space between the CHARM-II and NOMAD bounds in Fig. 6. Based on the
sensitivity we find in Fig. 6, we note that the DUNE near detector appears
capable of testing a dipole interpretation of the MiniBooNE excess
Vergani:2021tgc .

Figure 6: Expected sensitivity to the transition magnetic moment $\nu_{\mu}-N$
from DBs signals in the DUNE LAr near detector. The CHARM-II and NOMAD bounds
are reproduced from Ref. Coloma:2017ppo .

##  VII Conclusions

In this work we have studied the potential of present and future neutrino
oscillation experiments, namely, SK, HK and DUNE, to observe double-bang
events at low energies, which are characteristic signals of HNL production and
decay within the detector. We have considered both atmospheric neutrinos and
neutrino beams from meson decays as possible sources for the events, and
computed the number of events that would be obtained for the signal in two
different scenarios: HNL that mixes with $\nu_{\tau}$, and a dipole portal
involving a transition magnetic moment between the light neutrinos and the
HNL. Our results include a detailed calculation of the QE cross section for
both scenarios within the spectral function formalism, and a proper treatment
of the kinematic effects due to the nonzero HNL mass.

We have shown that an analysis of current Super-K data may be able to set new
and competitive bounds, especially in the HNL mass range 0.3-1 GeV for the
mixing scenario. We have also found that DUNE will be able to extend this
bound by roughly half an order of magnitude using the DUNE beam flux. This is
contrast with the atmospheric neutrinos which do not extend the bounds in the
allowed mass range. We have also examined the bounds on active-heavy
transition magnetic moments and find that Super-K may be able to considerably
improve over the DONUT bounds on tau-flavored transition moments.

Our analysis may be improved on several fronts. First, we are only including
QE and DIS events in our signal rates, and the inclusion of resonant
scattering processes will only improve the sensitivity further. Second, a
detailed analysis of the backgrounds for LAr TPC detectors may reveal
additional handles which could be used to reduce the minimum separation
between the two events while keeping a good signal-to-background ratio.
Finally, a third possibility could be to go beyond the QE and DIS
contributions considered here for the magnetic moment scenario and also
include the coherent contributions to $\nu\rightarrow N$ up-scattering, where
the interaction takes place with the whole nucleus. Although this would
considerably enhance the signal rate Magill:2018jla ; Plestid:2020vqf ;
Brdar:2020quo , it may suffer from a larger background as well since the first
bang would go unobserved at typical neutrino detectors. A detailed calculation
of the signal and background rates needs to be made in order to determine the
benefits of coherent scattering for enhancing the sensitivity to HNLs in
neutrino experiments, something which is beyond the scope of the present work.

Acknowledgements. We warmly thank Justo Martín-Albo for helpful discussions on
the separation of events in LAr TPC detectors. The work of IMS is supported by
the U.S. Department of Energy under the award number de-sc0020250. This
project has received funding/support from the European Union’s Horizon 2020
research and innovation program under the Marie Skłodowska-Curie grant
agreement No 860881-HIDDeN, and from the Spanish Agencia Estatal de
Investigación through the grant “IFT Centro de Excelencia Severo Ochoa
SEV-2016-0597”. The work of PC is supported by the Spanish MICINN through the
“Ramón y Cajal” program under grant RYC2018-024240-I. TRIUMF receives federal
funding via a contribution agreement with the National Research Council of
Canada. This manuscript has been authored by Fermi Research Alliance, LLC
under Contract No. DE-AC02-07CH11359 with the U.S. Department of Energy,
Office of Science, Office of High Energy Physics.

## References

  * (1) P. Minkowski, _$\mu\to e\gamma$ at a Rate of One Out of $10^{9}$ Muon Decays?_, _Phys. Lett._ B67 (1977) 421–428.
  * (2) M. Gell-Mann, P. Ramond and R. Slansky, _Complex Spinors and Unified Theories_ , _Conf. Proc._ C790927 (1979) 315–321, [1306.4669].
  * (3) R. N. Mohapatra and G. Senjanovic, _Neutrino Mass and Spontaneous Parity Violation_ , _Phys. Rev. Lett._ 44 (1980) 912.
  * (4) A. Atre, T. Han, S. Pascoli and B. Zhang, _The Search for Heavy Majorana Neutrinos_ , _JHEP_ 05 (2009) 030, [0901.3589].
  * (5) D. A. Bryman and R. Shrock, _Improved Constraints on Sterile Neutrinos in the MeV to GeV Mass Range_ , _Phys. Rev. D_ 100 (2019) 053006, [1904.06787].
  * (6) D. A. Bryman and R. Shrock, _Constraints on Sterile Neutrinos in the MeV to GeV Mass Range_ , _Phys. Rev. D_ 100 (2019) 073011, [1909.11198].
  * (7) M. Drewes and B. Garbrecht, _Combining experimental and cosmological constraints on heavy neutrinos_ , _Nucl. Phys. B_ 921 (2017) 250–315, [1502.00477].
  * (8) P. Ballett, T. Boschi and S. Pascoli, _Heavy Neutral Leptons from low-scale seesaws at the DUNE Near Detector_ , _JHEP_ 03 (2020) 111, [1905.00284].
  * (9) J. M. Berryman, A. de Gouvea, P. J. Fox, B. J. Kayser, K. J. Kelly and J. L. Raaf, _Searches for Decays of New Particles in the DUNE Multi-Purpose Near Detector_ , _JHEP_ 02 (2020) 174, [1912.07622].
  * (10) P. Coloma, E. Fernández-Martínez, M. González-López, J. Hernández-García and Z. Pavlovic, _GeV-scale neutrinos: interactions with mesons and DUNE sensitivity_ , _Eur. Phys. J. C_ 81 (2021) 78, [2007.03701].
  * (11) M. Breitbach, L. Buonocore, C. Frugiuele, J. Kopp and L. Mittnacht, _Searching for Physics Beyond the Standard Model in an Off-Axis DUNE Near Detector_ , 2102.03383.
  * (12) DELPHI collaboration, P. Abreu et al., _Search for neutral heavy leptons produced in Z decays_ , _Z. Phys. C_ 74 (1997) 57–71.
  * (13) J. Orloff, A. N. Rozanov and C. Santoni, _Limits on the mixing of tau neutrino to heavy neutrinos_ , _Phys. Lett. B_ 550 (2002) 8–15, [hep-ph/0208075].
  * (14) R. Plestid, _Luminous solar neutrinos II: Mass-mixing portals_ , 2010.09523.
  * (15) S. N. Gninenko, _The MiniBooNE anomaly and heavy neutrino decay_ , _Phys. Rev. Lett._ 103 (2009) 241802, [0902.3802].
  * (16) P. Coloma, P. A. Machado, I. Martinez-Soler and I. M. Shoemaker, _Double-Cascade Events from New Physics in Icecube_ , _Phys. Rev. Lett._ 119 (2017) 201804, [1707.08573].
  * (17) G. Magill, R. Plestid, M. Pospelov and Y.-D. Tsai, _Dipole Portal to Heavy Neutral Leptons_ , _Phys. Rev. D_ 98 (2018) 115015, [1803.03262].
  * (18) I. M. Shoemaker and J. Wyenberg, _Direct Detection Experiments at the Neutrino Dipole Portal Frontier_ , _Phys. Rev. D_ 99 (2019) 075010, [1811.12435].
  * (19) I. M. Shoemaker, Y.-D. Tsai and J. Wyenberg, _An Active-to-Sterile Neutrino Transition Dipole Moment and the XENON1T Excess_ , 2007.05513.
  * (20) V. Brdar, A. Greljo, J. Kopp and T. Opferkuch, _The Neutrino Magnetic Moment Portal: Cosmology, Astrophysics, and Direct Detection_ , _JCAP_ 01 (2021) 039, [2007.15563].
  * (21) R. Plestid, _Luminous solar neutrinos I: Dipole portals_ , 2010.04193.
  * (22) S. Vergani, N. W. Kamp, A. Diaz, C. A. Argüelles, J. M. Conrad, M. H. Shaevitz et al., _Explaining the MiniBooNE Excess Through a Mixed Model of Oscillation and Decay_ , 2105.06470.
  * (23) ArgoNeuT collaboration, R. Acciarri et al., _Detection of Back-to-Back Proton Pairs in Charged-Current Neutrino Interactions with the ArgoNeuT Detector in the NuMI Low Energy Beam Line_ , _Phys. Rev. D_ 90 (2014) 012008, [1405.4261].
  * (24) ArgoNeuT collaboration, R. Acciarri et al., _Demonstration of MeV-Scale Physics in Liquid Argon Time Projection Chambers Using ArgoNeuT_ , _Phys. Rev. D_ 99 (2019) 012002, [1810.06502].
  * (25) P. Coloma, _Non-Standard Interactions in propagation at the Deep Underground Neutrino Experiment_ , _JHEP_ 03 (2016) 016, [1511.06357].
  * (26) G. Shen, L. E. Marcucci, J. Carlson, S. Gandolfi and R. Schiavilla, _Inclusive neutrino scattering off deuteron from threshold to GeV energies_ , _Phys. Rev. C_ 86 (2012) 035503, [1205.4337].
  * (27) O. Benhar and D. Meloni, _Total neutrino and antineutrino nuclear cross-sections around 1-GeV_ , _Nucl. Phys. A_ 789 (2007) 379–402, [hep-ph/0610403].
  * (28) Particle Data Group collaboration, K. Nakamura et al., _Review of particle physics_ , _J. Phys. G_ 37 (2010) 075021.
  * (29) P. Herczeg, C. M. Hoffman and H. V. Klapdor-Kleingrothaus, eds., _Physics beyond the standard model. Proceedings, 5th International WEIN Symposium, Santa Fe, USA, June 14-19, 1998_ , 1999.
  * (30) K. Nakamura and P. D. Group, _Review of particle physics_ , _Journal of Physics G: Nuclear and Particle Physics_ 37 (2010) 075021.
  * (31) T. Leitner, O. Buss, L. Alvarez-Ruso and U. Mosel, _Electron- and neutrino-nucleus scattering from the quasielastic to the resonance region_ , _Phys. Rev. C_ 79 (2009) 034601, [0812.0587].
  * (32) C. Mahaux and R. Sartor, _Single-Particle Motion in Nuclei_ , pp. 1–223.  Springer US, Boston, MA, 1991.  10.1007/978-1-4613-9910-0_1.
  * (33) M. H. Mahzoon, R. J. Charity, W. H. Dickhoff, H. Dussan and S. J. Waldecker, _Forging the link between nuclear reactions and nuclear structure_ , _Phys. Rev. Lett._ 112 (Apr, 2014) 162503.
  * (34) W. H. Dickhoff, R. J. Charity and M. H. Mahzoon, _Novel applications of the dispersive optical model_ , _J. of Phys. G: Nucl. and Part. Phys._ 44 (2017) 033001.
  * (35) M. C. Atkinson, M. H. Mahzoon, M. A. Keim, B. A. Bordelon, C. D. Pruitt, R. J. Charity et al., _Dispersive optical model analysis of ${}^{208}\mathrm{Pb}$ generating a neutron-skin prediction beyond the mean field_, _Phys. Rev. C_ 101 (Apr, 2020) 044303.
  * (36) T2K collaboration, K. Abe et al., _Improved constraints on neutrino mixing from the T2K experiment with $\mathbf{3.13\times 10^{21}}$ protons on target_, 2101.03779.
  * (37) K. Hasegawa, N. Hayashi, M. Kinsho, T. Koseki, F. Naito, H. Oguri et al., _Performance and Status of the J-PARC Accelerators_ , in _9th International Particle Accelerator Conference_ , 6, 2018.  DOI.
  * (38) S. Igarashi, _Challenges to Higher Beam Power in J-PARC: Achieved Performance and Future Prospects_ , in _10th International Particle Accelerator Conference_ , 6, 2019.  DOI.
  * (39) P. Ballett, S. F. King, S. Pascoli, N. W. Prouse and T. Wang, _Sensitivities and synergies of DUNE and T2HK_ , _Phys. Rev. D_ 96 (2017) 033003, [1612.07275].
  * (40) DUNE collaboration, B. Abi et al., _Deep Underground Neutrino Experiment (DUNE), Far Detector Technical Design Report, Volume II: DUNE Physics_ , 2002.03005.
  * (41) M. Honda, M. Sajjad Athar, T. Kajita, K. Kasahara and S. Midorikawa, _Atmospheric neutrino flux calculation using the NRLMSISE-00 atmospheric model_ , _Phys. Rev._ D92 (2015) 023004, [1502.03916].
  * (42) Super-Kamiokande collaboration, K. Abe et al., _Solar Neutrino Measurements in Super-Kamiokande-IV_ , _Phys. Rev. D_ 94 (2016) 052010, [1606.07538].
  * (43) C. A. Argüelles et al., _New opportunities at the next-generation neutrino experiments I: BSM neutrino physics and dark matter_ , _Rept. Prog. Phys._ 83 (2020) 124201, [1907.08311].
  * (44) DUNE collaboration, B. Abi et al., _The DUNE Far Detector Interim Design Report Volume 1: Physics, Technology and Strategies_ , 1807.10334.
  * (45) MicroBooNE collaboration, C. Adams et al., _First measurement of $\nu_{\mu}$ charged-current $\pi^{0}$ production on argon with the MicroBooNE detector_, _Phys. Rev. D_ 99 (2019) 091102, [1811.02700].
  * (46) BOREXINO collaboration, G. Bellini et al., _Neutrinos from the primary proton–proton fusion process in the Sun_ , _Nature_ 512 (2014) 383–386.
  * (47) DONUT collaboration, R. Schwienhorst et al., _A New upper limit for the tau - neutrino magnetic moment_ , _Phys. Lett. B_ 513 (2001) 23–29, [hep-ex/0102026].
  * (48) ALEPH collaboration, D. Decamp et al., _Searches for new particles in $Z$ decays using the ALEPH detector_, _Phys. Rept._ 216 (1992) 253–340.
  * (49) S. N. Gninenko, _A resolution of puzzles from the LSND, KARMEN, and MiniBooNE experiments_ , _Phys. Rev. D_ 83 (2011) 015015, [1009.5536].