Rank-one witnesses from indexed harmonic maps

This file isolates the small mathematical interface behind the familiar ``harmonic morphism to a tree gives a g^1_d'' argument.

IndexedHarmonicCertificate is passive finite data: a vertex map, positive local degrees, and the total positive indices over each pair of source vertices. Its Boolean checker verifies the local harmonicity equations. For unit indices, pullback_prin_of_unitIndexed proves the required Laplacian identity and no pullback hypothesis remains. General metric dilation indices would require a weighted source Laplacian, so that genuinely broader case is still exposed separately as PullbackPrincipalCompatible rather than being silently accepted by the ordinary CFGraph checker.

Once that compatibility is available, the soundness proof is deliberately tiny: a fibre is effective, has degree d, and contains a chip above every source vertex. Equivalence of one-chip divisors on the target transports the corresponding fibres, so the fibre has rank at least one.

structure MarkedGraphs.IndexedHarmonicCertificate (G : CFGraph) (H : CFGraph) : Type (max u_1 u_2)

Passive finite data emitted by a search program for an indexed harmonic map. Valid below, rather than this structure, records its correctness.

• vertexMap : G.V → H.V

  The proposed map of source vertices to target vertices; harmonicity and adjacency conditions are imposed by Valid.

• localDegree : G.V → ℕ

  The proposed local degree at each source vertex, used in the harmonicity equations checked by Valid.

• edgeIndex : G.V → G.V → ℕ

  The total index assigned to each parallel bundle between source vertices; positivity and compatibility are required separately by Valid.

def MarkedGraphs.IndexedHarmonicCertificate.Valid {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) : Prop

Propositional validity of the finite edge-index data.

edgeIndex x y is the total index of the parallel bundle between x and y. The lower bound by numEdges G x y says that each source edge has a positive integral index; the target-adjacency condition says that no edge is contracted. The local equation is harmonicity, expressed after aggregating parallel edges.

Equations

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

structure MarkedGraphs.IndexedHarmonicData (G : CFGraph) (H : CFGraph) extends MarkedGraphs.IndexedHarmonicCertificate G H : Type (max u_1 u_2)

Validated finite data for a nondegenerate indexed harmonic map.

• vertexMap : G.V → H.V
• localDegree : G.V → ℕ
• edgeIndex : G.V → G.V → ℕ
• localDegree_pos (x : G.V) : 0 < self.localDegree x
• edgeIndex_symmetric (x y : G.V) : self.edgeIndex x y = self.edgeIndex y x
• edgeIndex_zero_of_no_source_edge (x y : G.V) : numEdges G x y = 0 → self.edgeIndex x y = 0
• sourceMultiplicity_le_edgeIndex (x y : G.V) : numEdges G x y ≤ self.edgeIndex x y
• maps_source_edges_to_target_edges (x y : G.V) : numEdges G x y > 0 → self.vertexMap x ≠ self.vertexMap y ∧ numEdges H (self.vertexMap x) (self.vertexMap y) > 0
• harmonic (x : G.V) (z : H.V) : (∑ y : G.V, if self.vertexMap y = z then self.edgeIndex x y else 0) = self.localDegree x * numEdges H (self.vertexMap x) z

def MarkedGraphs.IndexedHarmonicCertificate.UnitIndexed {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) : Prop

Compatibility with ordinary (unweighted) CFGraph chip-firing: the total index of a parallel source bundle is its ordinary edge multiplicity. General metric dilation indices require a weighted Laplacian and are intentionally not silently accepted by this predicate.

Equations

• c.UnitIndexed = ∀ (p : G.V × G.V), c.edgeIndex p.1 p.2 = numEdges G p.1 p.2

def MarkedGraphs.IndexedHarmonicCertificate.fibreDegree {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) (z : H.V) : ℤ

Degree of one raw fibre, computed without constructing a divisor.

Equations

• c.fibreDegree z = ∑ x : G.V, if c.vertexMap x = z then ↑(c.localDegree x) else 0

def MarkedGraphs.IndexedHarmonicCertificate.HasDegree {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) (d : ℤ) : Prop

Every raw fibre has the advertised global degree.

Equations

• c.HasDegree d = ∀ (z : H.V), c.fibreDegree z = d

def MarkedGraphs.IndexedHarmonicCertificate.check {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) : Bool

Executable replay of all finite local conditions.

Equations

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

def MarkedGraphs.IndexedHarmonicCertificate.checkUnitIndexed {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) : Bool

Executable unit-index check, to be combined with check when the certificate is intended to act on the ordinary source Laplacian.

Equations

• c.checkUnitIndexed = decide (∀ (p : G.V × G.V), c.edgeIndex p.1 p.2 = numEdges G p.1 p.2)

def MarkedGraphs.IndexedHarmonicCertificate.checkDegree {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) (d : ℤ) : Bool

Executable constant-fibre-degree check.

Equations

• c.checkDegree d = decide (∀ (z : H.V), c.fibreDegree z = d)

def MarkedGraphs.IndexedHarmonicCertificate.checkDegreeAt {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) (z : H.V) (d : ℤ) : Bool

Executable degree check at one chosen target vertex. For a valid harmonic certificate into a connected target, this is equivalent to the otherwise redundant all-fibres check; see IndexedHarmonicData.hasDegree_toData_of_fibreDegree_at.

Equations

• c.checkDegreeAt z d = decide (c.fibreDegree z = d)

@[simp]

theorem MarkedGraphs.IndexedHarmonicCertificate.check_eq_true_iff {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) : c.check = true ↔ c.Valid

@[simp]

theorem MarkedGraphs.IndexedHarmonicCertificate.checkUnitIndexed_eq_true_iff {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) : c.checkUnitIndexed = true ↔ c.UnitIndexed

@[simp]

theorem MarkedGraphs.IndexedHarmonicCertificate.checkDegree_eq_true_iff {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) (d : ℤ) : c.checkDegree d = true ↔ c.HasDegree d

@[simp]

theorem MarkedGraphs.IndexedHarmonicCertificate.checkDegreeAt_eq_true_iff {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) (z : H.V) (d : ℤ) : c.checkDegreeAt z d = true ↔ c.fibreDegree z = d

def MarkedGraphs.IndexedHarmonicCertificate.toData {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) (h : c.Valid) : IndexedHarmonicData G H

A verified raw certificate becomes the mathematical harmonic-map object.

Equations

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

def MarkedGraphs.IndexedHarmonicData.fibre {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (z : H.V) : CFDiv G

The target-one-chip fibre, as a divisor on the source.

Equations

• f.fibre z x = if f.vertexMap x = z then ↑(f.localDegree x) else 0

def MarkedGraphs.IndexedHarmonicData.pullback {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (A : CFDiv H) : CFDiv G

Pullback of an arbitrary target divisor using the local degrees.

Equations

• f.pullback A x = ↑(f.localDegree x) * A (f.vertexMap x)

def MarkedGraphs.IndexedHarmonicData.pullbackScript {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (σ : firingScript H) : firingScript G

Pull a target firing script back along the vertex map.

Equations

• f.pullbackScript σ x = σ (f.vertexMap x)

def MarkedGraphs.IndexedHarmonicData.UnitIndexed {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) : Prop

The indexed data uses the ordinary unweighted source Laplacian.

Equations

• f.UnitIndexed = ∀ (x y : G.V), f.edgeIndex x y = numEdges G x y

theorem MarkedGraphs.IndexedHarmonicData.unitIndexed_toData {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) (hValid : c.Valid) (hUnit : c.UnitIndexed) : (c.toData hValid).UnitIndexed

A checked unit-index condition survives conversion from raw certificate data.

theorem MarkedGraphs.IndexedHarmonicData.pullback_sub {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (A B : CFDiv H) : f.pullback (A - B) = f.pullback A - f.pullback B

Pullback is additive on subtraction.

theorem MarkedGraphs.IndexedHarmonicData.pullback_prin_of_unitIndexed {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hUnit : f.UnitIndexed) (σ : firingScript H) : f.pullback ((prin H) σ) = (prin G) (f.pullbackScript σ)

The central Laplacian identity. For unit-indexed harmonic data, pulling back a target principal divisor is the principal divisor of the pulled-back script on the ordinary source graph.

def MarkedGraphs.IndexedHarmonicData.HasDegree {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (d : ℤ) : Prop

The (constant) degree of the map, expressed as the degree of every fibre. This is the one global numerical datum needed by the rank-one argument.

Equations

• f.HasDegree d = ∀ (z : H.V), CFDiv.degree (f.fibre z) = d

theorem MarkedGraphs.IndexedHarmonicData.fibre_degree_eq_of_target_edge {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) {z w : H.V} (hzw : numEdges H z w > 0) : CFDiv.degree (f.fibre z) = CFDiv.degree (f.fibre w)

The degrees of two fibres above adjacent target vertices agree. This is the finite double-counting identity behind the usual assertion that the degree of a harmonic map is independent of the target point.

theorem MarkedGraphs.IndexedHarmonicData.eq_of_graph_connected_of_eq_on_edges {H : CFGraph} {α : Type} (F : H.V → α) (hConnected : graphConnected H) (hEdge : ∀ (z w : H.V), numEdges H z w > 0 → F z = F w) (z₀ z : H.V) : F z = F z₀

A function on the vertices of a connected graph which is constant across every target edge is constant everywhere. The cut-based definition of graphConnected makes this a short finite proof.

theorem MarkedGraphs.IndexedHarmonicData.fibre_degree_eq_of_target_connected {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hConnected : graphConnected H) (z w : H.V) : CFDiv.degree (f.fibre z) = CFDiv.degree (f.fibre w)

Harmonicity makes the fibre degree locally constant on the target, and therefore constant on every connected target.

theorem MarkedGraphs.IndexedHarmonicData.hasDegree_of_fibre_degree_at {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hConnected : graphConnected H) (z₀ : H.V) {d : ℤ} (hDegree : CFDiv.degree (f.fibre z₀) = d) : f.HasDegree d

One fibre-degree calculation suffices for a harmonic map to a connected target.

theorem MarkedGraphs.IndexedHarmonicData.hasDegree_toData {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) (hValid : c.Valid) {d : ℤ} (hDegree : c.HasDegree d) : (c.toData hValid).HasDegree d

A checked raw fibre-degree equation is exactly the divisor-degree condition used by the rank-one soundness theorem.

theorem MarkedGraphs.IndexedHarmonicData.fibreDegree_toData {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) (hValid : c.Valid) (z : H.V) : CFDiv.degree ((c.toData hValid).fibre z) = c.fibreDegree z

The one raw fibre-degree computation transfers directly to the divisor fibre of validated data.

theorem MarkedGraphs.IndexedHarmonicData.hasDegree_toData_of_fibreDegree_at {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) (hValid : c.Valid) (hConnected : graphConnected H) (z₀ : H.V) {d : ℤ} (hDegree : c.fibreDegree z₀ = d) : (c.toData hValid).HasDegree d

The global degree field is redundant for valid harmonic data over a connected target: checking one raw fibre determines all of them.

theorem MarkedGraphs.IndexedHarmonicData.pullback_one_chip {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (z : H.V) : f.pullback (oneChip z) = f.fibre z

fibre really is pullback of a one-chip divisor.

theorem MarkedGraphs.IndexedHarmonicData.fibre_effective {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (z : H.V) : effective (f.fibre z)

A fibre is effective.

theorem MarkedGraphs.IndexedHarmonicData.fibre_sub_one_chip_effective {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (x : G.V) : effective (f.fibre (f.vertexMap x) - oneChip x)

Removing the chip at x from the fibre over its image remains effective. Nondegeneracy is exactly the needed fact here.

def MarkedGraphs.IndexedHarmonicData.TargetOneChipEquivalent (H : CFGraph) : Prop

The target condition actually used by the rank-one proof.

Equations

• MarkedGraphs.IndexedHarmonicData.TargetOneChipEquivalent H = ∀ (y z : H.V), linearEquiv H (oneChip y) (oneChip z)

theorem MarkedGraphs.IndexedHarmonicData.targetOneChipEquivalent_of_connected_genus_zero (H : CFGraph) (hConnected : graphConnected H) (hGenus : H.genus = 0) : TargetOneChipEquivalent H

A connected genus-zero target has trivial degree-zero chip-firing class group. This is the graph-theoretic content of the usual phrase “target is a tree”; it is stated in the invariant form available in CFGraph.

def MarkedGraphs.IndexedHarmonicData.PullbackPrincipalCompatible {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) : Prop

Mathematical pullback compatibility, deliberately separate from the raw finite data. The unit-indexed checker implies it below; non-unit metric dilations still need a future weighted-Laplacian development.

Equations

• f.PullbackPrincipalCompatible = ∀ (A B : CFDiv H), linearEquiv H A B → linearEquiv G (f.pullback A) (f.pullback B)

theorem MarkedGraphs.IndexedHarmonicData.pullbackPrincipalCompatible_of_unitIndexed {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hUnit : f.UnitIndexed) : f.PullbackPrincipalCompatible

The checked harmonicity equations plus unit edge indices imply the previously abstract pullback-principal compatibility hypothesis.

theorem MarkedGraphs.IndexedHarmonicData.pullbackPrincipalCompatible_of_checks {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) (hCheck : c.check = true) (hUnitCheck : c.checkUnitIndexed = true) : (c.toData ⋯).PullbackPrincipalCompatible

Boolean-check boundary for pullback compatibility: a raw certificate whose local equations and unit-index condition both replay successfully supplies the mathematical hypothesis used by the rank-one theorems.

theorem MarkedGraphs.IndexedHarmonicData.fibre_linear_equiv_of_target {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) (hPullback : f.PullbackPrincipalCompatible) {y z : H.V} (hyz : linearEquiv H (oneChip y) (oneChip z)) : linearEquiv G (f.fibre y) (f.fibre z)

Pullback transports equivalence of target one-chip divisors to equivalence of fibres.

theorem MarkedGraphs.IndexedHarmonicData.rank_ge_one_of_target_one_chip_equiv {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) {d : ℤ} (_hDegree : f.HasDegree d) (hPullback : f.PullbackPrincipalCompatible) (hTarget : TargetOneChipEquivalent H) (z : H.V) : rank G (f.fibre z) ≥ 1

A nondegenerate indexed harmonic map into a target with linearly equivalent one-chip divisors supplies a rank-one divisor of its map degree.

theorem MarkedGraphs.IndexedHarmonicData.bnExists_rank_one_of_target_one_chip_equiv {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) {d : ℤ} (hDegree : f.HasDegree d) (hPullback : f.PullbackPrincipalCompatible) (hTarget : TargetOneChipEquivalent H) (z : H.V) : Utilities.BNExists G 1 d

The resulting Brill--Noether witness.

theorem MarkedGraphs.IndexedHarmonicData.bnExists_rank_one_of_tree_target {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) {d : ℤ} (hDegree : f.HasDegree d) (hPullback : f.PullbackPrincipalCompatible) (hTreePicard : TargetOneChipEquivalent H) (z : H.V) : Utilities.BNExists G 1 d

Target-Picard form of the tree theorem, useful when one-chip equivalence is available directly without going through connectedness and genus.

theorem MarkedGraphs.IndexedHarmonicData.bnExists_rank_one_of_connected_genus_zero_target {G : CFGraph} {H : CFGraph} (f : IndexedHarmonicData G H) {d : ℤ} (hDegree : f.HasDegree d) (hPullback : f.PullbackPrincipalCompatible) (hConnected : graphConnected H) (hGenus : H.genus = 0) (z : H.V) : Utilities.BNExists G 1 d

The conventional tree-target corollary, using connectedness and genus zero instead of exposing the target Picard-group condition.

theorem MarkedGraphs.IndexedHarmonicData.bnExists_rank_one_of_checked_harmonic_tree {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) (d : ℤ) (hCheck : c.check = true) (hUnitCheck : c.checkUnitIndexed = true) (hDegreeCheck : c.checkDegree d = true) (hConnected : graphConnected H) (hGenus : H.genus = 0) (z : H.V) : Utilities.BNExists G 1 d

End-to-end kernel boundary for the compact certificate: local harmonicity, unit indexing, and constant fibre degree are all Boolean-replayed; only the structural target facts connected and genus = 0 are supplied as proofs.

theorem MarkedGraphs.IndexedHarmonicData.bnExists_rank_one_of_checked_harmonic_tree_one_degree {G : CFGraph} {H : CFGraph} (c : IndexedHarmonicCertificate G H) (d : ℤ) (z₀ : H.V) (hCheck : c.check = true) (hUnitCheck : c.checkUnitIndexed = true) (hDegreeCheck : c.checkDegreeAt z₀ d = true) (hConnected : graphConnected H) (hGenus : H.genus = 0) (z : H.V) : Utilities.BNExists G 1 d

Degree-reduced end-to-end kernel boundary. Unlike bnExists_rank_one_of_checked_harmonic_tree, this replays the fibre-degree equation only at z₀: the preceding harmonic double-counting theorem and target connectedness supply every other fibre equation.