Belyi-map records and the translation of stored triples

The LMFDB table of Belyi maps stores, for each Galois orbit of Belyi maps, the monodromy triples of the maps in the orbit. The database composes permutations from left to right, so a stored triple (σ0, σ1, σinf) satisfies σ0 * σ1 * σinf = 1 in Mathlib's multiplication, the opposite of the relation σinf * σ1 * σ0 = 1 imposed on a TauCeti.PermutationTriple. Such a stored triple is a TauCeti.PermutationTriple.LMFDB.StoredTriple, and the triple it denotes is its image TauCeti.PermutationTriple.LMFDB.StoredTriple.toTriple under the inverse of TauCeti.PermutationTriple.equivOppositeConvention: the componentwise inverse.

The first part of this file proves that this translation preserves every invariant a record asserts, each computed directly on the stored permutations: the ordered full cycle partitions, the orders, the monodromy group, connectedness, the automorphism group, the Euler characteristic and genus, and membership in a passport. It also commutes with relabeling the sheets. Reading a stored triple without the translation is wrong as soon as its first two components do not commute, by TauCeti.PermutationTriple.LMFDB.StoredTriple.mul_mul_eq_one_iff_commute, so a stored triple whose first two components commute cannot detect the convention.

The second part mirrors one row of the table as a TauCeti.PermutationTriple.LMFDB.BelyiRecord. Its stored triples are listed position by position against the stored complex embeddings of the base field, which is recorded by the field TauCeti.PermutationTriple.LMFDB.BelyiRecord.storedEmbeddingCount_eq_triplesLength. The number of embedding entries is the natural number TauCeti.PermutationTriple.LMFDB.BelyiRecord.storedEmbeddingCount, and the stored orbit size is asserted to equal it, not the size of a Galois orbit of isomorphism classes: several stored triples may be simultaneously conjugate, so the isomorphism classes they represent, TauCeti.PermutationTriple.LMFDB.BelyiRecord.storedClasses, may be fewer than the stored entries. TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor states what a row asserts about a passport, and the theorems following it read the stored partitions, genus, and monodromy group off the stored permutations, and bound the number of stored classes by the passport size.

The table also stores each triple in disjoint cycle notation, which omits fixed points and writes the identity as the empty product. A row parses it into lists of cycles (TauCeti.PermutationTriple.LMFDB.CycleNotationTriple), and validity asks that it be a disjoint cycle notation (Equiv.Perm.IsCycleNotation) for the stored triple in the same position. The notation is not translated: the stored notation of a component is reversed cycle by cycle to give the notation of the corresponding component of the translated triple (TauCeti.PermutationTriple.LMFDB.StoredTriple.IsCycleNotation.isCycleNotation_toTriple_σ0). The listed lengths are the stored permutation's Equiv.Perm.cycleType, so the stored partitions are the listed lengths padded by parts equal to one (TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.lambdas_eq_of_mem_triplesCyc).

The stored base field, the defining equations of the curve and the map, the floating-point values of the embeddings, and the labels are carried as data and are not interpreted here.

Main definitions

• TauCeti.PermutationTriple.LMFDB.StoredTriple: a triple in the database's convention.
• TauCeti.PermutationTriple.LMFDB.StoredTriple.toTriple: the triple it denotes.
• TauCeti.PermutationTriple.LMFDB.StoredTriple.IsCycleNotation: a stored triple written in disjoint cycle notation.
• TauCeti.PermutationTriple.LMFDB.BelyiRecord: a parsed row of the Belyi-map table.
• TauCeti.PermutationTriple.LMFDB.BelyiRecord.storedEmbeddingCount: the number of stored embedding entries.
• TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor: validity of a row for a passport.

Main results

• TauCeti.PermutationTriple.LMFDB.StoredTriple.toTriple_eq_iff: the translation is the opposite-convention equivalence.
• TauCeti.PermutationTriple.LMFDB.StoredTriple.genus_toTriple and TauCeti.PermutationTriple.LMFDB.StoredTriple.hasPassport_toTriple_iff, with their companions: the invariants of the translated triple, read off the stored permutations.
• TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.lambdas_eq_of_mem_triplesCyc: the stored partitions of a valid row are the cycle lengths of its stored cycle notation, padded by fixed points.
• TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.card_storedClasses_le_passportSize: the stored triples of a valid row represent at most as many isomorphism classes as the passport has.

References

• M. Musty, S. Schiavone, J. Sijsling, J. Voight, A database of Belyi maps, Proceedings of the Thirteenth Algorithmic Number Theory Symposium, Open Book Series 2, 2019, §2.
• LMFDB, Belyi maps.

@[reducible, inline]

abbrev TauCeti.PermutationTriple.LMFDB.StoredTriple (n : ℕ) : Type

A permutation triple as the LMFDB stores it. The database composes permutations from left to right, so its stored triples satisfy σ0 * σ1 * σinf = 1 in Mathlib's multiplication.

@[reducible, inline]

abbrev TauCeti.PermutationTriple.LMFDB.CycleNotationTriple (n : ℕ) : Type

A triple of permutations of Fin n in disjoint cycle notation, as the database's cycle notation is parsed: each component is a list of cycles, each cycle the list of its points in order, where the stored point i is the element i - 1 of Fin n.

def TauCeti.PermutationTriple.LMFDB.StoredTriple.toTriple {n : ℕ} (s : StoredTriple n) : PermutationTriple n

The permutation triple denoted by a stored triple: its image under the inverse of the opposite-convention equivalence, which inverts every component.

@[simp]

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.toTriple_σ0 {n : ℕ} (s : StoredTriple n) : s.toTriple.σ0 = (↑s).1⁻¹

@[simp]

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.toTriple_σ1 {n : ℕ} (s : StoredTriple n) : s.toTriple.σ1 = (↑s).2.1⁻¹

@[simp]

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.toTriple_σinf {n : ℕ} (s : StoredTriple n) : s.toTriple.σinf = (↑s).2.2⁻¹

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.toTriple_eq_iff {n : ℕ} (s : StoredTriple n) {t : PermutationTriple n} : s.toTriple = t ↔ s = (equivOppositeConvention n) t

A stored triple denotes t exactly when it is the opposite-convention form of t.

@[simp]

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.toTriple_equivOppositeConvention {n : ℕ} (t : PermutationTriple n) : toTriple ((equivOppositeConvention n) t) = t

@[simp]

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.equivOppositeConvention_toTriple {n : ℕ} (s : StoredTriple n) : (equivOppositeConvention n) s.toTriple = s

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.mul_mul_eq_one_iff_commute {n : ℕ} (s : StoredTriple n) : (↑s).2.2 * (↑s).2.1 * (↑s).1 = 1 ↔ Commute (↑s).1 (↑s).2.1

The stored components also satisfy this library's relation exactly when the first two of them commute. A stored triple whose first two components do not commute is therefore not a permutation triple when read without translation.

@[simp]

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.toTriple_relabelOppositeConvention {n : ℕ} (s : StoredTriple n) (τ : Equiv.Perm (Fin n)) : toTriple (relabelOppositeConvention τ s) = τ • s.toTriple

Relabeling a stored triple relabels the triple it denotes.

Invariants of the translated triple

@[simp]

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.cycleData_toTriple {n : ℕ} (s : StoredTriple n) : s.toTriple.cycleData = ((↑s).1.partition.parts, (↑s).2.1.partition.parts, (↑s).2.2.partition.parts)

The ordered full cycle partitions of the translated triple are those of the stored components.

@[simp]

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.orderTriple_toTriple {n : ℕ} (s : StoredTriple n) : s.toTriple.orderTriple = (orderOf (↑s).1, orderOf (↑s).2.1, orderOf (↑s).2.2)

The orders of the components of the translated triple are those of the stored components.

@[simp]

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.monodromyGroup_toTriple {n : ℕ} (s : StoredTriple n) : s.toTriple.monodromyGroup = Subgroup.closure {(↑s).1, (↑s).2.1}

The monodromy group of the translated triple is generated by the first two stored components.

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.isConnected_toTriple_iff {n : ℕ} (s : StoredTriple n) : s.toTriple.IsConnected ↔ n ≠ 0 ∧ MulAction.IsPretransitive (↥(Subgroup.closure {(↑s).1, (↑s).2.1})) (Fin n)

The translated triple is connected exactly when there is a sheet and the first two stored components generate a transitive group.

@[simp]

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.automorphismGroup_toTriple {n : ℕ} (s : StoredTriple n) : s.toTriple.automorphismGroup = Subgroup.centralizer {(↑s).1, (↑s).2.1}

The automorphism group of the translated triple is the simultaneous centralizer of the first two stored components.

@[simp]

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.eulerChar_toTriple {n : ℕ} (s : StoredTriple n) : s.toTriple.eulerChar = ↑(orbitCount (↑s).1) + ↑(orbitCount (↑s).2.1) + ↑(orbitCount (↑s).2.2) - ↑n

The Euler characteristic of the translated triple, counted on the stored components.

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.genus_toTriple {n : ℕ} (s : StoredTriple n) : s.toTriple.genus = ((2 - (↑(orbitCount (↑s).1) + ↑(orbitCount (↑s).2.1) + ↑(orbitCount (↑s).2.2) - ↑n)) / 2).toNat

The genus of the translated triple, counted on the stored components.

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.hasPassport_toTriple_iff {n : ℕ} (s : StoredTriple n) (hs : s.toTriple.IsConnected) (P : PassportSpec n) : PassportSpec.HasPassport ⟨s.toTriple, hs⟩ P ↔ (∃ (τ : Equiv.Perm (Fin n)), Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) (Subgroup.closure {(↑s).1, (↑s).2.1}) = P.G) ∧ (↑s).1.partition.parts = P.lam0 ∧ (↑s).2.1.partition.parts = P.lam1 ∧ (↑s).2.2.partition.parts = P.laminf

A connected translated triple has passport P exactly when the group generated by the first two stored components is conjugate to the reference group of P and the stored components have the partitions of P.

Stored cycle notation

structure TauCeti.PermutationTriple.LMFDB.StoredTriple.IsCycleNotation {n : ℕ} (s : StoredTriple n) (c : CycleNotationTriple n) : Prop

c writes each component of s in disjoint cycle notation, as the database stores it: fixed points are omitted and the identity is the empty list of cycles.

• σ0 : (↑s).1.IsCycleNotation c.1

  c.1 writes the first stored component.

• σ1 : (↑s).2.1.IsCycleNotation c.2.1

  c.2.1 writes the second stored component.

• σinf : (↑s).2.2.IsCycleNotation c.2.2

  c.2.2 writes the third stored component.

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.exists_isCycleNotation {n : ℕ} (s : StoredTriple n) : ∃ (c : CycleNotationTriple n), s.IsCycleNotation c

Every stored triple can be written in disjoint cycle notation.

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.IsCycleNotation.isCycleNotation_toTriple_σ0 {n : ℕ} {s : StoredTriple n} {c : CycleNotationTriple n} (h : s.IsCycleNotation c) : s.toTriple.σ0.IsCycleNotation (List.map List.reverse c.1)

The stored cycle notation of the first component, reversed cycle by cycle, writes the first component of the translated triple.

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.IsCycleNotation.isCycleNotation_toTriple_σ1 {n : ℕ} {s : StoredTriple n} {c : CycleNotationTriple n} (h : s.IsCycleNotation c) : s.toTriple.σ1.IsCycleNotation (List.map List.reverse c.2.1)

The stored cycle notation of the second component, reversed cycle by cycle, writes the second component of the translated triple.

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.IsCycleNotation.isCycleNotation_toTriple_σinf {n : ℕ} {s : StoredTriple n} {c : CycleNotationTriple n} (h : s.IsCycleNotation c) : s.toTriple.σinf.IsCycleNotation (List.map List.reverse c.2.2)

The stored cycle notation of the third component, reversed cycle by cycle, writes the third component of the translated triple.

theorem TauCeti.PermutationTriple.LMFDB.StoredTriple.IsCycleNotation.cycleData_toTriple {n : ℕ} {s : StoredTriple n} {c : CycleNotationTriple n} (h : s.IsCycleNotation c) : s.toTriple.cycleData = (↑(List.map List.length c.1) + Multiset.replicate (n - (List.map List.length c.1).sum) 1, ↑(List.map List.length c.2.1) + Multiset.replicate (n - (List.map List.length c.2.1).sum) 1, ↑(List.map List.length c.2.2) + Multiset.replicate (n - (List.map List.length c.2.2).sum) 1)

The ordered full cycle partitions of the translated triple are the cycle lengths of the stored cycle notation, each padded by one part equal to one for every point it omits.

Belyi-map records

structure TauCeti.PermutationTriple.LMFDB.BelyiRecord (n : ℕ) : Type

A row of the LMFDB table of Belyi maps in degree n, with its stored fields parsed into Lean data. The row describes one Galois orbit of Belyi maps. Its stored degree is the field deg, which validity identifies with n.

The stored triples are kept in the database's convention, as StoredTriples, and are listed position by position against the stored complex embeddings of the base field: the i-th triple is the monodromy of the map under the i-th embedding. The remaining fields are carried as data and are not interpreted here.

• label : String

  The stored label of the Galois orbit.

• plabel : String

  The stored label of the passport containing the orbit.

• deg : ℕ

  The stored degree.

• lambdas : Multiset ℕ × Multiset ℕ × Multiset ℕ

  The stored full cycle partitions at 0, 1, and ∞, fixed points included.

• g : ℕ

  The stored genus.

• orbitSize : ℕ

  The stored orbit size.

• baseField : List ℚ

  The stored coefficients, in increasing degree, of a defining polynomial of the base field over which the stored equations are written. This is a field of definition of each map in the orbit, and is not asserted to be its field of moduli.

• embeddings : List (Float × Float)

  The stored floating-point values, as real and imaginary parts, of the complex embeddings of the base field.

• triples : List (StoredTriple n)

  The stored triples, in the database's convention.

• triplesCyc : List (CycleNotationTriple n)

  The stored triples in cycle notation, parsed into lists of cycles. The notation omits fixed points and writes the identity as the empty list of cycles.

• curve : String

  The stored equations of the curve.

• map : String

  The stored formula for the map.

• planeModel : String

  The stored plane model of the curve.

• planeConstant : String

  The stored constant attached to the plane model.

• curveLabel : Option String

  The stored label of the associated curve, absent on rows that have none.

• friends : List String

  The stored labels of related objects.

• storedEmbeddingCount_eq_triplesLength : self.embeddings.length = self.triples.length

  The stored triples are indexed by the stored embeddings, position by position.

def TauCeti.PermutationTriple.LMFDB.BelyiRecord.storedEmbeddingCount {n : ℕ} (r : BelyiRecord n) : ℕ

The number of stored embedding entries of a row. This is a count of stored entries, not the size of a Galois orbit of isomorphism classes.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.storedEmbeddingCount_def {n : ℕ} (r : BelyiRecord n) : r.storedEmbeddingCount = r.embeddings.length

noncomputable def TauCeti.PermutationTriple.LMFDB.BelyiRecord.storedClasses {n : ℕ} (r : BelyiRecord n) : Finset (IsoClass n)

The isomorphism classes of the triples denoted by the stored triples.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.mem_storedClasses {n : ℕ} (r : BelyiRecord n) {c : IsoClass n} : c ∈ r.storedClasses ↔ ∃ s ∈ r.triples, IsoClass.mk s.toTriple = c

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.card_storedClasses_le_storedEmbeddingCount {n : ℕ} (r : BelyiRecord n) : r.storedClasses.card ≤ r.storedEmbeddingCount

The stored triples represent at most as many isomorphism classes as there are stored embedding entries. The inequality is strict when two stored triples are simultaneously conjugate.

structure TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor {n : ℕ} (r : BelyiRecord n) (P : PassportSpec n) : Prop

A row is valid for the passport P when its stored degree is the degree, its stored orbit size is its number of stored embedding entries, it stores at least one triple, every stored triple denotes a connected triple with passport P, its stored cycle notation writes the stored triples position by position, the stored partitions are those of P, and the stored genus is the genus of every stored triple.

The labels, the base field, the equations, and the embedding values are not constrained.

• deg_eq : r.deg = n

  The stored degree is the degree.

• orbitSize_eq : r.orbitSize = r.storedEmbeddingCount

  The stored orbit size is the number of stored embedding entries.

• triples_ne_nil : r.triples ≠ []

  At least one triple is stored.

• hasPassport (s : StoredTriple n) : s ∈ r.triples → ∃ (hs : s.toTriple.IsConnected), PassportSpec.HasPassport ⟨s.toTriple, hs⟩ P

  Every stored triple denotes a connected triple with passport P.

• forall₂_isCycleNotation : List.Forall₂ (fun (c : CycleNotationTriple n) (s : StoredTriple n) => s.IsCycleNotation c) r.triplesCyc r.triples

  The stored cycle notation writes the stored triples, position by position.

• lambdas_eq : r.lambdas = (P.lam0, P.lam1, P.laminf)

  The stored partitions are those of P.

• g_eq (s : StoredTriple n) : s ∈ r.triples → r.g = s.toTriple.genus

  The stored genus is the genus of every stored triple.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.isConnected_toTriple {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} {s : StoredTriple n} (h : r.IsValidFor P) (hs : s ∈ r.triples) : s.toTriple.IsConnected

Every stored triple of a valid row denotes a connected triple.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.isAdmissible {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} (h : r.IsValidFor P) : P.IsAdmissible

The passport of a valid row is admissible.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.orbitSize_eq_length_triples {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} (h : r.IsValidFor P) : r.orbitSize = r.triples.length

The stored orbit size of a valid row is its number of stored triples.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.orbitSize_pos {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} (h : r.IsValidFor P) : 0 < r.orbitSize

The stored orbit size of a valid row is positive.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.lambdas_eq_cycleData {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} {s : StoredTriple n} (h : r.IsValidFor P) (hs : s ∈ r.triples) : r.lambdas = s.toTriple.cycleData

The stored partitions of a valid row are the ordered cycle data of every stored triple.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.lambdas_eq_partition {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} {s : StoredTriple n} (h : r.IsValidFor P) (hs : s ∈ r.triples) : r.lambdas = ((↑s).1.partition.parts, (↑s).2.1.partition.parts, (↑s).2.2.partition.parts)

The stored partitions of a valid row are the full cycle partitions of the stored components of every stored triple, read in the database's convention.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.lambdas_eq_cycleType_add {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} {s : StoredTriple n} (h : r.IsValidFor P) (hs : s ∈ r.triples) : r.lambdas = ((↑s).1.cycleType + Multiset.replicate (n - (↑s).1.support.card) 1, (↑s).2.1.cycleType + Multiset.replicate (n - (↑s).2.1.support.card) 1, (↑s).2.2.cycleType + Multiset.replicate (n - (↑s).2.2.support.card) 1)

The stored partitions of a valid row are the cycle types of the stored components, which omit fixed points, padded by one part equal to one for each fixed point.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.length_triplesCyc {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} (h : r.IsValidFor P) : r.triplesCyc.length = r.triples.length

A valid row stores one cycle notation for each stored triple.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.exists_mem_triples_isCycleNotation {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} (h : r.IsValidFor P) {c : CycleNotationTriple n} (hc : c ∈ r.triplesCyc) : ∃ s ∈ r.triples, s.IsCycleNotation c

Every stored cycle notation of a valid row writes one of its stored triples.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.lambdas_eq_of_mem_triplesCyc {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} (h : r.IsValidFor P) {c : CycleNotationTriple n} (hc : c ∈ r.triplesCyc) : r.lambdas = (↑(List.map List.length c.1) + Multiset.replicate (n - (List.map List.length c.1).sum) 1, ↑(List.map List.length c.2.1) + Multiset.replicate (n - (List.map List.length c.2.1).sum) 1, ↑(List.map List.length c.2.2) + Multiset.replicate (n - (List.map List.length c.2.2).sum) 1)

The stored partitions from the stored cycle notation. The stored partitions of a valid row are the cycle lengths of each of its stored cycle notations, padded by one part equal to one for every omitted fixed point.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.exists_map_closure_eq {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} {s : StoredTriple n} (h : r.IsValidFor P) (hs : s ∈ r.triples) : ∃ (τ : Equiv.Perm (Fin n)), Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) (Subgroup.closure {(↑s).1, (↑s).2.1}) = P.G

In a valid row, the group generated by the first two stored components of every stored triple is conjugate to the reference group of the passport.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.g_eq_toNat {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} {s : StoredTriple n} (h : r.IsValidFor P) (hs : s ∈ r.triples) : r.g = ((2 - (↑(orbitCount (↑s).1) + ↑(orbitCount (↑s).2.1) + ↑(orbitCount (↑s).2.2) - ↑n)) / 2).toNat

The stored genus of a valid row, counted on the stored components of any stored triple.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.g_eq_genus {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} (h : r.IsValidFor P) {t : ConnectedTriple n} (ht : PassportSpec.HasPassport t P) : r.g = (↑t).genus

The stored genus of a valid row is the genus of every connected triple with its passport.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.exists_mem_classSet_of_mem_storedClasses {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} (h : r.IsValidFor P) {c : IsoClass n} (hc : c ∈ r.storedClasses) : ∃ d ∈ P.classSet, d.forget = c

Every stored class of a valid row is the class of a connected triple in its passport.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.card_storedClasses_le_passportSize {n : ℕ} {r : BelyiRecord n} {P : PassportSpec n} (h : r.IsValidFor P) : r.storedClasses.card ≤ P.passportSize

The stored triples of a valid row represent at most as many isomorphism classes as its passport contains.

theorem TauCeti.PermutationTriple.LMFDB.BelyiRecord.exists_isValidFor {n : ℕ} (t : ConnectedTriple n) : ∃ (r : BelyiRecord n), r.IsValidFor t.passportOf ∧ r.triples = [(equivOppositeConvention n) ↑t]

Every connected triple is the stored triple of a formal row that is valid for its passport, so TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor is not vacuous. The row carries placeholder data in the fields that validity leaves unconstrained: the base-field polynomial X - 1 with a single embedding entry, and empty labels and equations. Its cycle notation is some disjoint cycle notation for the stored triple. It is not a certificate that the corresponding Belyi map is defined over ℚ, which this theorem does not establish.