Building an event record from a graph

Physlib.HepMC3.Basic models an event as an ordered list of P and V records, because that order is part of the Asciiv3 format. Producing that order by hand is error-prone: a vertex's V line must follow the P lines of its incoming particles and precede those of its outgoing ones, and some vertices are not written at all.

This module takes the other view — a plain graph of particles and vertices, in any order — and derives the record sequence. A generator builds graphs; only this module needs to know what the serializer expects.

The two rules it implements

Topological order. A particle's parent field refers backwards, so every vertex is emitted only once all of its incoming particles have been emitted. Particles produced by no vertex (the beams) come first, carrying parent = 0.

Single-mother elision. A vertex with exactly one incoming particle, no position and no status carries no information that the daughters cannot: HepMC3's own writer omits it and records the mother particle's identifier — positive — in each daughter's parent field. GenEvent.numVertices already knows to count such vertices by recovering them from the distinct positive parent references, which is why an elided vertex still appears in the E line count.

The elision condition is deliberately conservative: a vertex is elided only when it has exactly one incoming particle, position = none, and status = 0. A vertex carrying a position or a status is always written, because that information has nowhere else to go.

Termination

The emission loop is driven by explicit fuel, one unit per vertex, rather than being marked partial. Each iteration emits at least one vertex, so the fuel bound is tight; exhausting it means the graph is cyclic or refers to a missing particle, and ofGraph? reports that as none rather than looping or silently truncating.

The body-only entry point is bodyOfGraph?; GenEvent.ofGraph? wraps it into an event. They are deliberately not both called ofGraph?: inside this namespace the bare name would resolve to the GenEvent one, silently passing the particle list where an event number is expected.

structure EpsilonEridani.HepMC3.GraphVertex : Type

A vertex of an event graph, before serialization order is decided.

• id : Int

  Object identifier; negative, unique within the event.

• incoming : List Nat

  Identifiers of the incoming particles.

• outgoing : List Nat

  Identifiers of the outgoing particles.

• status : Int

  Status code; 0 carries no information and permits elision.

• position : Option FourVector

  Optional space-time position; when present the vertex is never elided.

@[instance_reducible]

instance EpsilonEridani.HepMC3.instReprGraphVertex : Repr GraphVertex

Equations

• EpsilonEridani.HepMC3.instReprGraphVertex = { reprPrec := EpsilonEridani.HepMC3.instReprGraphVertex.repr }

def EpsilonEridani.HepMC3.instReprGraphVertex.repr : GraphVertex → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance EpsilonEridani.HepMC3.instInhabitedGraphVertex : Inhabited GraphVertex

Equations

• EpsilonEridani.HepMC3.instInhabitedGraphVertex = { default := EpsilonEridani.HepMC3.instInhabitedGraphVertex.default }

structure EpsilonEridani.HepMC3.GraphParticle : Type

A particle of an event graph. Unlike GenParticle this carries no parent: the production reference is derived from the graph.

• id : Nat

  Object identifier; positive, unique within the event.

• pdg : Int

  PDG Monte Carlo particle identifier.

• momentum : FourVector

  Four-momentum, in the event's momentum unit.

• mass : Float

  Generated mass.

• status : Int

  HepMC status code.

def EpsilonEridani.HepMC3.instReprGraphParticle.repr : GraphParticle → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance EpsilonEridani.HepMC3.instReprGraphParticle : Repr GraphParticle

Equations

• EpsilonEridani.HepMC3.instReprGraphParticle = { reprPrec := EpsilonEridani.HepMC3.instReprGraphParticle.repr }

@[instance_reducible]

instance EpsilonEridani.HepMC3.instInhabitedGraphParticle : Inhabited GraphParticle

Equations

• EpsilonEridani.HepMC3.instInhabitedGraphParticle = { default := EpsilonEridani.HepMC3.instInhabitedGraphParticle.default }

def EpsilonEridani.HepMC3.GraphVertex.elidable (v : GraphVertex) : Bool

Is this vertex elidable under the single-mother rule?

Equations

• v.elidable = (v.incoming.length == 1 && v.position.isNone && v.status == 0)

def EpsilonEridani.HepMC3.Graph.toGenParticle (p : GraphParticle) (parent : Int) : GenParticle

Turn a graph particle into a GenParticle with the given production reference.

Equations

• EpsilonEridani.HepMC3.Graph.toGenParticle p parent = { id := p.id, parent := parent, pdg := p.pdg, momentum := p.momentum, mass := p.mass, status := p.status }

def EpsilonEridani.HepMC3.Graph.step (parts : List GraphParticle) (emitted : List Nat) (pending : List GraphVertex) (acc : List EventRecord) : Option (List Nat × List GraphVertex × List EventRecord)

One emission step: pick the first vertex whose incoming particles have all been emitted, append its records, and return the extended state. none when no vertex is ready.

Equations

• One or more equations did not get rendered due to their size.

def EpsilonEridani.HepMC3.Graph.loop : Nat → List GraphParticle → List Nat → List GraphVertex → List EventRecord → Option (List EventRecord)

Drive step to exhaustion with explicit fuel.

Equations

• One or more equations did not get rendered due to their size.
• EpsilonEridani.HepMC3.Graph.loop 0 x✝³ x✝² x✝¹ x✝ = if x✝¹.isEmpty = true then some x✝ else none
• EpsilonEridani.HepMC3.Graph.loop n.succ x✝² x✝¹ [] x✝ = some x✝

def EpsilonEridani.HepMC3.bodyOfGraph? (parts : List GraphParticle) (verts : List GraphVertex) : Option (List EventRecord)

Derive the ordered event body from a graph, or none if the graph is cyclic or refers to a particle that is not present.

Beam particles — those produced by no vertex — are emitted first, in the order given, with parent = 0. Every other particle is emitted immediately after the vertex that produced it, which is written unless the single-mother rule elides it.

Equations

• One or more equations did not get rendered due to their size.

def EpsilonEridani.HepMC3.GenEvent.ofGraph? (eventNumber : Int) (parts : List GraphParticle) (verts : List GraphVertex) (weights : List Float := []) (attributes : List Attribute := []) : Option GenEvent

Build a GenEvent from a graph, keeping every other field at its default.

Returns none on a graph bodyOfGraph? rejects.

Equations

• One or more equations did not get rendered due to their size.