Affine-positioned chips and break lists on a closed face

This is the closed-orthant companion to the affine-positioned portion of AffinePositionMultiBreak.lean. It deliberately takes a DegSpec and a proof that its numerical lengths agree with the affine certificate, rather than rebuilding a particular DegSpec from the certificate. This is the form needed by a row leaf: the contraction census chooses the representative map, while the leaf merely names positions and slopes.

There are two small, independent carriers.

• WeightedChip is one affine position with an integral coefficient. In contrast to the positive MultiCode format, a row witness may use an arbitrary integral coefficient before its residual checks prove effectiveness.
• BreakList is a per-slot ordered list of affine positions and their post-break slopes. The concrete list is fed directly to DegSpec.breakScript; its exact interior and core Laplacian formulae are consequently available on collapsed faces as well.

The only geometry carried by these definitions is LengthCompatible. Bound certificates remain the existing Code.BoundsCertified facts, so all affine arithmetic is shared with the positive decoder.

def MarkedGraphs.Certificate.AffinePosition.Closed.LengthCompatible {m n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (point : Fin m → ℤ) : Prop

The affine certificate and a closed-face DegSpec read the same concrete slot lengths at this point.

Equations

• MarkedGraphs.Certificate.AffinePosition.Closed.LengthCompatible d certificate point = ∀ (edge : Fin p), d.length edge = certificate.segmentNat point edge

def MarkedGraphs.Certificate.AffinePosition.Closed.Code.decodeClosedVertex {m n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) {degree : ℤ} (hValid : certificate.ValidClosed degree) (hLength : LengthCompatible d certificate point) (hBounds : Code.BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) : d.Vertex

Decode a cone-certified affine code into an arbitrary compatible closed face. Unlike Code.decodeDegenerateVertex, this does not require the face's representative map to have been constructed by the certificate census.

Equations

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

structure MarkedGraphs.Certificate.AffinePosition.Closed.WeightedChip (m p : ℕ) : Type

A possibly signed chip at an affine-described slot position.

• position : Code m p

  The affine code naming the chip’s slot and position on that slot.

• coefficient : ℤ

  The signed integer multiplicity of the chip; negative coefficients are permitted.

def MarkedGraphs.Certificate.AffinePosition.Closed.WeightedChip.BoundsCertified {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (chips : List (WeightedChip m p)) : Prop

Every named chip position has its two bounds certified by the local cone.

Equations

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

def MarkedGraphs.Certificate.AffinePosition.Closed.WeightedChip.divisorOf {m n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (chips : List (WeightedChip m p)) (point : Fin m → ℤ) {degree : ℤ} (hValid : certificate.ValidClosed degree) (hLength : LengthCompatible d certificate point) (hBounds : BoundsCertified certificate chips) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) : CFDiv d.graph

The divisor denoted by a list of weighted affine chips on a compatible closed face.

Equations

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

theorem MarkedGraphs.Certificate.AffinePosition.Closed.WeightedChip.deg_divisorOf {m n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (chips : List (WeightedChip m p)) (point : Fin m → ℤ) {degree : ℤ} (hValid : certificate.ValidClosed degree) (hLength : LengthCompatible d certificate point) (hBounds : BoundsCertified certificate chips) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) : CFDiv.degree (divisorOf d certificate chips point hValid hLength hBounds hCone) = (List.map coefficient chips).sum

The degree of a weighted affine-chip divisor is the sum of its declared coefficients, including negative coefficients.

structure MarkedGraphs.Certificate.AffinePosition.Closed.Break (m p : ℕ) : Type

One entry of a per-slot affine break list: its slope is in force beginning at position. List order is preserved, matching the C checker's override semantics and SubdivisionGraph.Spec.breakSlope.

• position : Code m p

  The affine slot-position code at which this break entry begins to prescribe a slope.

• slope : ℤ

  The integer slope in force from this break position, subject to the ordered list’s later overrides.

@[reducible, inline]

abbrev MarkedGraphs.Certificate.AffinePosition.Closed.BreakList (m p : ℕ) : Type

Ordered break data, grouped by slot. WellFormed prevents a code whose own slot differs from the list slot from silently being interpreted with the wrong length.

Equations

• MarkedGraphs.Certificate.AffinePosition.Closed.BreakList m p = (Fin p → List (MarkedGraphs.Certificate.AffinePosition.Closed.Break m p))

def MarkedGraphs.Certificate.AffinePosition.Closed.BreakList.WellFormed {m p : ℕ} (script : BreakList m p) : Prop

Every entry in a slot list genuinely names that slot.

Equations

• script.WellFormed = ∀ (edge : Fin p), ∀ entry ∈ script edge, entry.position.edge = edge

def MarkedGraphs.Certificate.AffinePosition.Closed.BreakList.BoundsCertified {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (script : BreakList m p) : Prop

All affine positions in the break lists have certified bounds.

Equations

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

def MarkedGraphs.Certificate.AffinePosition.Closed.BreakList.breaks {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (script : BreakList m p) (point : Fin m → ℤ) (edge : Fin p) : List (ℕ × ℤ)

Evaluate the ordered affine break list for one slot.

Equations

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

def MarkedGraphs.Certificate.AffinePosition.Closed.BreakList.firingScript {m n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (script : BreakList m p) (potential : Fin n → ℤ) (point : Fin m → ℤ) : _root_.firingScript d.graph

A concrete closed-face firing script from affine break lists.

Equations

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

def MarkedGraphs.Certificate.AffinePosition.Closed.BreakList.Balanced {m n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (script : BreakList m p) (potential : Fin n → ℤ) (point : Fin m → ℤ) : Prop

The sole closing condition for an affine break-list script on a closed face. In particular it forces equality of endpoint potentials on a collapsed slot.

Equations

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

theorem MarkedGraphs.Certificate.AffinePosition.Closed.BreakList.prin_firingScript_interiorVertex {m n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (script : BreakList m p) (potential : Fin n → ℤ) (point : Fin m → ℤ) (hInv : d.RepInvariant potential) (hBalanced : Balanced d certificate script potential point) (edge : Fin p) (offset : Fin (d.length edge - 1)) : (prin d.graph) (firingScript d certificate script potential point) (d.interiorVertex edge offset) = Utilities.Certificate.SubdivisionGraph.Spec.breakSlope (breaks certificate script point edge) (↑offset + 1) - Utilities.Certificate.SubdivisionGraph.Spec.breakSlope (breaks certificate script point edge) ↑offset

The interior Laplacian is the jump of the evaluated ordered break list.

theorem MarkedGraphs.Certificate.AffinePosition.Closed.BreakList.prin_firingScript_interiorVertex_eq_zero {m n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (script : BreakList m p) (potential : Fin n → ℤ) (point : Fin m → ℤ) (hInv : d.RepInvariant potential) (hBalanced : Balanced d certificate script potential point) (edge : Fin p) (offset : Fin (d.length edge - 1)) (hAvoid : ∀ entry ∈ script edge, Code.coordinate certificate entry.position point ≠ ↑offset + 1) : (prin d.graph) (firingScript d certificate script potential point) (d.interiorVertex edge offset) = 0

Away from every named affine break, the interior Laplacian vanishes.

theorem MarkedGraphs.Certificate.AffinePosition.Closed.BreakList.prin_firingScript_coreVertex {m n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (script : BreakList m p) (potential : Fin n → ℤ) (point : Fin m → ℤ) (hInv : d.RepInvariant potential) (hBalanced : Balanced d certificate script potential point) (vertex : Fin n) : (prin d.graph) (firingScript d certificate script potential point) (d.coreVertex vertex) = ∑ edge : Fin p, ((if d.rep (d.core.tail edge) = d.rep vertex then Utilities.Certificate.SubdivisionGraph.Spec.breakSlope (breaks certificate script point edge) 0 else 0) + if d.rep (d.core.head edge) = d.rep vertex then -Utilities.Certificate.SubdivisionGraph.Spec.breakSlope (breaks certificate script point edge) (d.length edge - 1) else 0)

The core Laplacian is the usual endpoint-slope sum over the contracted classes, including zero slots.