From a closed-orthant explicit-potential record to rank one #
This is the DegSpec/ValidClosed counterpart of the assembly half of
Certificate/ExplicitPotentialRankOne.lean: the divisor extended over the
contracted subdivision, the anchor firing script, effectivity of the removed-chip
residual, core reachability, and the rank-one conclusion under a strong-separator
certificate. Nothing existing is modified; subdivisionSpec,
subdivisionDivisor and bnExists_of_valid_of_strongSeparator keep working
verbatim on the open orthant.
The two shape changes a consumer sees #
degenerateDivisor, notsubdivisionDivisor.DegSpec.coreVertexis not injective, so aFin n-indexed divisor is ill-posed on a face: two named core vertices can be the same graph vertex. The extended divisor therefore gives a class the sum of its members' chips, which is exactly what keepsCFDiv.degreeequal to the checked core degree (deg_degenerateDivisor).Class-level endpoint bookkeeping.
lowerEndpointContribution_le_endpointContributionis false vertex by vertex at a face: on a collapsed slot the certificate boundsα_e ≤ stepandβ_e ≤ -stepare unavailable (they need a unit step). What is true, and what the Laplacian actually needs, is the inequality at a contracted class, where the collapsed slot contributesα_e + β_e ≤ 0on the left and exactly0on the right because its two endpoint terms are equal and opposite. That isclassLowerEndpointContribution_le_classEndpointContribution, andclass_core_balance_nonnegativeis the corresponding balance. On the interior the class is a singleton and both collapse to the existing statements.
The one input the certificate does not determine #
DegSpec.RepInvariant — that the anchor potential is constant on each
contracted class. ValidClosed gives it along each individual collapsed slot
for free (potential_eq_of_segment_eval_zero); what it cannot give is that
rep merges only vertices joined by chains of collapsed slots, because rep
names the face and the certificate does not. ZeroReach and
repInvariant_evaluatedPotential_of_zeroReach below discharge it from such a
chain; that is the exact join with the contraction census.
Fibre regrouping for an arbitrary endpoint map #
Utilities.Certificate.DegenerateSpec.DegSpec.sum_tail_class / sum_head_class are the same
statement for d.core.tail / d.core.head; this is the version used by the
certificate-level bookkeeping, where no DegSpec is in scope yet.
Endpoint bookkeeping at a contracted class #
Conservative endpoint bookkeeping, summed over a contracted class.
Equations
- certificate.classLowerEndpointContribution rep anchor r = ∑ vertex : Fin n with rep vertex = rep r, certificate.lowerEndpointContribution anchor vertex
Instances For
Actual interpolated endpoint contribution, summed over a contracted class.
Equations
- certificate.classEndpointContribution rep anchor point r = ∑ vertex : Fin n with rep vertex = rep r, certificate.endpointContribution anchor point vertex
Instances For
Target coefficient after removing the anchor chip, summed over a contracted class.
Equations
- certificate.classTargetCoefficient rep anchor r = ∑ vertex : Fin n with rep vertex = rep r, certificate.targetCoefficient anchor vertex
Instances For
Gap 2, the comparison. The conservative endpoint bound is still
conservative at a contracted class. On a surviving slot this is the existing
interpolated_endpoint_bounds argument, recovered from ValidClosed by
interpolated_endpoint_bounds_of_validClosed. On a collapsed slot the actual
contribution is exactly 0, because the two endpoint terms lie in the same
class and are equal and opposite, while the bound contributes
α_e + β_e ≤ 0 — Valid's third conjunct, unchanged.
Gap 2, the balance. At every contracted class the target plus the actual interpolated contributions is non-negative.
On the interior the class is a singleton, so the class-level statements are literally the existing per-vertex ones.
Rep-invariance of the anchor potential #
Two core vertices joined by one collapsed slot.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Joined by a chain of collapsed slots. This is the relation a contraction
census decides; rep is meant to be its component map.
Equations
- certificate.ZeroReach point = Relation.ReflTransGen (certificate.ZeroLink point)
Instances For
The face named by a contraction datum #
The rep-invariance obligation, discharged from a chain of collapsed slots.
This is the exact join with a contraction census: the census produces rep
together with the reachability witness.
On the interior of the orthant the obligation is free.
The degenerate rise is the certificate's numerical rise, verbatim: no rep
enters DegSpec.coreRise.
The extended divisor #
The atlas divisor, pushed to the contracted core: a class carries the total of its members' chips, and every interior vertex carries none.
This is the shape change forced by non-injectivity of coreVertex.
Equations
- certificate.degenerateDivisor d = d.coreClassDivisor certificate.divisor
Instances For
Agreement with the strictly positive layer: on the interior each class is a
singleton, so the extended divisor is literally subdivisionDivisor's value.
The extended divisor has exactly the degree checked on the core: no chip is lost when two named core vertices are merged.
The anchor script and its residual #
The firing script attached to a core anchor, assembled on the contracted subdivision by canonical integral interpolation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Laplacian of the anchor script at a contracted class is the class-level endpoint contribution. This is the bridge between the graph layer and the class-level bookkeeping of gap 2.
The rank-one input. The removed-chip residual of a checked closed-orthant record is effective at every vertex of the contracted subdivision.
Every core class is reached by the divisor assembled from a checked closed-orthant record.
The embedded core classes #
The embedded core classes of a contracted subdivision. coreVertex is not
injective, so this image can be strictly smaller than n.
Equations
Instances For
End-to-end local soundness on the closed orthant #
The closed-orthant counterpart of bnExists_of_valid_of_strongSeparator.
An accepted closed-orthant record, at one integral length point together with a
contraction datum naming a face, proves BNExists for the contracted
subdivision — which, by DegSpec.Contraction.laplacianEquiv, is the strictly
positive subdivision of the contracted core. On the interior (rep = id,
hInv free by repInvariant_evaluatedPotential_of_pos) this is the existing
statement.