Subdivision graphs from finite edge slots #
This module turns a loopless finite core with positive integral edge lengths
into an actual CFGraph. Edge slots, rather than endpoint pairs, are the
primary objects. Consequently parallel core edges remain distinct throughout
the construction.
For an edge slot of length L, its interior vertices are indexed by
Fin (L - 1): index j denotes offset j + 1 from the tail. Its unit steps
are indexed by Fin L. The graph edge multiset is the image of the finite
type of all unit steps, so every unit edge is emitted exactly once even when
several emitted pairs coincide.
Complete input data for subdividing a finite loopless core.
- core : ExplicitPotential.Core n p
The finite nonempty loopless core whose slots are subdivided.
The positive number of unit edges replacing each core slot.
Instances For
Package a positive length assignment on a fixed finite loopless core as a subdivision specification, without repeating the structure fields.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An interior vertex remembers its edge slot. Its Fin (L - 1) coordinate
j represents path offset j + 1.
Instances For
Injection of a core vertex into the subdivision.
Equations
- spec.coreVertex vertex = Sum.inl vertex
Instances For
The left endpoint of a unit step.
Equations
- spec.stepLeft edge offset = if hzero : ↑offset = 0 then spec.coreVertex (spec.core.tail edge) else spec.interiorVertex edge ⟨↑offset - 1, ⋯⟩
Instances For
The ordered pair emitted by one unit step. Its orientation is only a
storage convention; numEdges treats it as undirected.
Instances For
The subdivided graph. The underlying multiset is the image of all unit steps, retaining multiplicity when distinct slots emit the same pair.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Exact multiplicity formula, expressed directly as a finite filter of unit steps. This is often the most convenient interface for executable proofs.
Expanded indicator-sum form of the exact edge multiplicity.
Positive multiplicity is equivalent to the existence of an emitted unit step with the requested unordered endpoints.
The preceding path vertex of an interior vertex.
Equations
- spec.previousVertex edge offset = spec.stepLeft edge (spec.previousStep edge offset)
Instances For
An interior vertex is the right endpoint of exactly its preceding unit step. Packaging the edge and offset as one sigma value avoids any transport ambiguity in the dependent indices.
A principal-divisor coefficient is the sum of the contributions of the individual emitted unit steps incident to the vertex.
A principal-divisor coefficient depends only on the oriented difference of the firing script along each emitted unit step. This form is convenient for scripts described by slopes rather than by vertex values.
Canonical integer interpolation on the constructed graph #
Extend an integral core potential over every subdivided slot by the
canonical convex interpolation from SubdivisionArithmetic.
Equations
- spec.interpolatedScript potential (Sum.inl vertex) = potential vertex
- spec.interpolatedScript potential (Sum.inr interior) = spec.pathValue potential interior.fst (↑interior.snd + 1)
Instances For
On the left endpoint of step i, the interpolated script has path value
at offset i.
On the right endpoint of step i, the interpolated script has path value
at offset i + 1.
The script difference across a unit edge is exactly the arithmetic interpolator's step slope.
Exact principal divisor of the interpolated script, written entirely in terms of the certified unit-step slopes. This is the direct bridge from the arithmetic certificate to the graph Laplacian.
Core-vertex specialization of the exact interpolated Laplacian formula.
Interior-vertex specialization of the exact interpolated Laplacian formula.