From explicit subdivision potentials to rank one

ExplicitPotential.CertificateData checks the arithmetic data attached to one affine length cone. This file assembles those data on the concrete subdivision graph from SubdivisionGraph.

The checked potentials make the degree-three divisor reach every core vertex. The final theorem deliberately takes a StrongSeparatorCertificate for the embedded core as a hypothesis: the sound strong-separator theorem then promotes core reachability to rank one. The remaining graph-theoretic input is the uniform statement that the core vertices form a strong separator in a subdivision.

Exact Laplacian formulas on a subdivision

theorem Utilities.Certificate.SubdivisionGraph.Spec.stepLeft_eq_coreVertex_iff {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : Fin (spec.length edge)) (vertex : Fin n) : spec.stepLeft edge offset = spec.coreVertex vertex ↔ ↑offset = 0 ∧ spec.core.tail edge = vertex

A unit step starts at a core vertex exactly when it is the first step of its edge slot and that slot has the requested tail.

theorem Utilities.Certificate.SubdivisionGraph.Spec.stepRight_eq_coreVertex_iff {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : Fin (spec.length edge)) (vertex : Fin n) : spec.stepRight edge offset = spec.coreVertex vertex ↔ ↑offset + 1 = spec.length edge ∧ spec.core.head edge = vertex

A unit step ends at a core vertex exactly when it is the final step of its edge slot and that slot has the requested head.

theorem Utilities.Certificate.SubdivisionGraph.Spec.prin_interpolatedScript_core_eq_endpointSum {n p : ℕ} (spec : Spec n p) (potential : Fin n → ℤ) (vertex : Fin n) : (prin spec.graph) (spec.interpolatedScript potential) (spec.coreVertex vertex) = ∑ edge : Fin p, ((if spec.core.tail edge = vertex then SubdivisionArithmetic.step (spec.length edge) (spec.coreRise potential edge) 0 else 0) + if spec.core.head edge = vertex then -SubdivisionArithmetic.step (spec.length edge) (spec.coreRise potential edge) (spec.length edge - 1) else 0)

At a core vertex, only the first and final unit steps of incident core slots contribute to the interpolated principal divisor.

theorem Utilities.Certificate.SubdivisionGraph.Spec.prin_interpolatedScript_interior_eq_stepDifference {n p : ℕ} (spec : Spec n p) (potential : Fin n → ℤ) (edge : Fin p) (offset : Fin (spec.length edge - 1)) : (prin spec.graph) (spec.interpolatedScript potential) (spec.interiorVertex edge offset) = SubdivisionArithmetic.step (spec.length edge) (spec.coreRise potential edge) (↑offset + 1) - SubdivisionArithmetic.step (spec.length edge) (spec.coreRise potential edge) ↑offset

At an interior vertex, the interpolated principal divisor is the next path slope minus the previous path slope.

theorem Utilities.Certificate.SubdivisionGraph.Spec.interior_num_edges_pos_iff {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : Fin (spec.length edge - 1)) (vertex : spec.Vertex) : 0 < numEdges spec.graph (spec.interiorVertex edge offset) vertex ↔ vertex = spec.previousVertex edge offset ∨ vertex = spec.nextVertex edge offset

The only neighbors of an interior subdivision vertex are its preceding and following path vertices. This positivity-level characterization is the basic local input for constructing the embedded core's separator cells.

Assembly of one checked explicit-potential cone

def Utilities.Certificate.ExplicitPotential.CertificateData.subdivisionSpec {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hCone : FormsHold certificate.cone point) : SubdivisionGraph.Spec n p

The concrete subdivision specified by an integral point of a checked local cone.

Equations

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

def Utilities.Certificate.ExplicitPotential.CertificateData.subdivisionDivisor {m n p : ℕ} (certificate : CertificateData m n p) (spec : SubdivisionGraph.Spec n p) : CFDiv spec.graph

The core divisor, extended by zero over all subdivision-interior vertices.

Equations

• certificate.subdivisionDivisor spec (Sum.inl vertex) = certificate.divisor vertex
• certificate.subdivisionDivisor spec (Sum.inr _interior) = 0

def Utilities.Certificate.ExplicitPotential.CertificateData.evaluatedPotential {m n p : ℕ} (certificate : CertificateData m n p) (anchor : Fin n) (point : Fin m → ℤ) (vertex : Fin n) : ℤ

Evaluate one affine core potential at the chosen integral length point.

Equations

• certificate.evaluatedPotential anchor point vertex = Utilities.Certificate.AffineCover.AffineForm.eval ((certificate.witness anchor).potential vertex) point

theorem Utilities.Certificate.ExplicitPotential.CertificateData.coreRise_evaluatedPotential {m n p : ℕ} (certificate : CertificateData m n p) (anchor : Fin n) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hCone : FormsHold certificate.cone point) (edge : Fin p) : (certificate.subdivisionSpec point core_nonempty hValid hCone).coreRise (certificate.evaluatedPotential anchor point) edge = certificate.riseValue anchor point edge

theorem Utilities.Certificate.ExplicitPotential.CertificateData.deg_subdivisionDivisor {m n p : ℕ} (certificate : CertificateData m n p) (spec : SubdivisionGraph.Spec n p) : CFDiv.degree (certificate.subdivisionDivisor spec) = ∑ vertex : Fin n, certificate.divisor vertex

The extended divisor has exactly the degree checked on the core.

def Utilities.Certificate.ExplicitPotential.CertificateData.coreAnchorScript {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hCone : FormsHold certificate.cone point) (anchor : Fin n) : firingScript (certificate.subdivisionSpec point core_nonempty hValid hCone).graph

The firing script attached to a core anchor, assembled on the concrete subdivision by canonical integral interpolation.

Equations

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

theorem Utilities.Certificate.ExplicitPotential.CertificateData.effective_coreAnchorResidual {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hCone : FormsHold certificate.cone point) (anchor : Fin n) : effective (certificate.subdivisionDivisor (certificate.subdivisionSpec point core_nonempty hValid hCone) - oneChip ((certificate.subdivisionSpec point core_nonempty hValid hCone).coreVertex anchor) + (prin (certificate.subdivisionSpec point core_nonempty hValid hCone).graph) (certificate.coreAnchorScript point core_nonempty hValid hCone anchor))

The checked explicit potential for a core anchor makes the corresponding removed-chip residual effective at every core and interior vertex.

theorem Utilities.Certificate.ExplicitPotential.CertificateData.reaches_coreVertex {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hCone : FormsHold certificate.cone point) (anchor : Fin n) : StrongSeparator.Reaches (certificate.subdivisionSpec point core_nonempty hValid hCone).graph (certificate.subdivisionDivisor (certificate.subdivisionSpec point core_nonempty hValid hCone)) ((certificate.subdivisionSpec point core_nonempty hValid hCone).coreVertex anchor)

Every core vertex is reached by the divisor assembled from a checked explicit-potential record.

def Utilities.Certificate.ExplicitPotential.CertificateData.coreVertices {n p : ℕ} (spec : SubdivisionGraph.Spec n p) : Finset spec.graph.V

The embedded core vertices of a subdivision.

Equations

• Utilities.Certificate.ExplicitPotential.CertificateData.coreVertices spec = Finset.image spec.coreVertex Finset.univ

theorem Utilities.Certificate.ExplicitPotential.CertificateData.coreVertices_nonempty {n p : ℕ} (spec : SubdivisionGraph.Spec n p) : (coreVertices spec).Nonempty

@[simp]

theorem Utilities.Certificate.ExplicitPotential.CertificateData.coreVertex_mem_coreVertices {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (vertex : Fin n) : spec.coreVertex vertex ∈ coreVertices spec

@[simp]

theorem Utilities.Certificate.ExplicitPotential.CertificateData.interiorVertex_not_mem_coreVertices {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (edge : Fin p) (offset : Fin (spec.length edge - 1)) : spec.interiorVertex edge offset ∉ coreVertices spec

theorem Utilities.Certificate.ExplicitPotential.CertificateData.bnExists_of_valid_of_strongSeparator {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (core_nonempty : 0 < n) (degree : ℤ) (hValid : certificate.Valid degree) (hCone : FormsHold certificate.cone point) (hConnected : graphConnected (certificate.subdivisionSpec point core_nonempty hValid hCone).graph) (hSeparator : StrongSeparator.StrongSeparatorCertificate (certificate.subdivisionSpec point core_nonempty hValid hCone).graph (coreVertices (certificate.subdivisionSpec point core_nonempty hValid hCone))) : BNExists (certificate.subdivisionSpec point core_nonempty hValid hCone).graph 1 degree

End-to-end local soundness theorem.

An accepted explicit-potential record on one integral length point proves BNExists for the resulting subdivision as soon as the embedded core is supplied with the graph-theoretic strong-separator certificate. No external search result occurs among the hypotheses: Valid, FormsHold, and the separator certificate are ordinary Lean propositions, and generated data can discharge the first two through their Boolean checkers.