The strong separator and connectivity on the CLOSED length orthant #
Certificate/DegenerateRankOne.lean ends at
bnExists_of_validClosed_of_strongSeparator, which still assumes graph
connectivity and a strong-separator certificate for the contracted core
classes. On the open orthant those two hypotheses are discharged uniformly by
SubdivisionSeparator.coreVertices_strongSeparatorCertificate and
SubdivisionConnectivity.graph_connected_of_coreConnected, and the resulting
convenience wrapper is bnExists_on_subdivision_of_valid. This file supplies
the closed-orthant analogue.
The route, and why not the other one #
The separator argument of Certificate/SubdivisionSeparator.lean rests on
Spec.pathVertex_injective. That is false at a face: when a slot
collapses, tail = head and coreVertex stops being injective, so a naive
port of those 954 lines to DegSpec would be porting an argument to a setting
where its central lemma fails.
Instead we exploit the fact already proved in Certificate/DegenerateSpec.lean:
a DegSpec with a contraction datum is LaplacianEquiv to the strictly
positive Spec on the contracted core, where the existing machinery applies
unchanged. Certificate/LaplacianEquivSeparator.lean transports an
ExpansionCell and a StrongSeparatorCertificate along a LaplacianEquiv;
here we pull both the separator and connectivity back through
DegSpec.Contraction.laplacianEquiv.
So SubdivisionSeparator is used, not reproved, and it is used only where its
hypotheses hold.
No contraction datum has to be supplied #
DegSpec.canonicalContraction builds the contracted target from the DegSpec
itself: its vertices are the rep-classes and its slots are the surviving
ones. Consequently the wrapper below takes no target, no vertex map and no
slot map — only the same core-connectivity check
ExplicitPotential.Core.Connected (decided by connectedCheck) that the open
orthant already uses, stated on the uncontracted core.
Hazard respected #
Nothing here indexes anything by Fin n through coreVertex. The separator
is the image Finset degenerateCoreVertices d, which is exactly the set of
rep-classes; degenerateCoreVertices_eq_image proves it is the relabeled
coreVertices of the contracted target without ever asserting injectivity.
The canonical contraction target #
Number of surviving slots.
Equations
Instances For
An indexing of the contracted classes. Any bijection will do; the statements below never depend on the choice.
Equations
Instances For
An indexing of the surviving slots.
Equations
Instances For
The contracted core: one vertex per rep-class, one slot per surviving
slot, endpoints taken rep-wise.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical contraction target. A genuinely positive
SubdivisionGraph.Spec, so every lemma of the open-orthant layer applies to
it verbatim.
Equations
- d.contractedSpec = { core := d.contractedCore, length := fun (e' : Fin d.slotCard) => d.length ↑(d.slotIndex.symm e'), core_nonempty := ⋯, core_loopless := ⋯, length_pos := ⋯ }
Instances For
The DegSpec is a contraction onto its canonical target. This is the
datum a row would otherwise have to produce by hand.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Separator and connectivity through a contraction #
The relabeled core vertices of the contracted target are exactly the
contracted core classes. Injectivity of coreVertex is never used: the
statement is an equality of images.
The separator, on the closed orthant. Pulled back from the contracted
positive target, where SubdivisionSeparator applies unchanged.
Cut connectedness passes from the uncontracted core to the contracted one.
A cut of the target pulls back to a rep-saturated cut of the core; a core
slot crossing it cannot be collapsed, so it is the image of a target slot.
Connectivity, on the closed orthant. The finite trust boundary is the
same Core.Connected cut certificate the open orthant uses, on the
uncontracted core.
Uniform statements, with no contraction datum supplied #
The strong separator for any degenerate spec. No hypothesis at all:
exactly as on the open orthant, where
coreVertices_strongSeparatorCertificate is also hypothesis-free.
Connectivity for any degenerate spec from the finite core cut certificate on the uncontracted core.
The contracted core classes determine rank one on a closed subdivision.
This is the closed-orthant counterpart of
SubdivisionGraph.Spec.rank_ge_one_of_reachesCoreVertices. Once a divisor
reaches every named core class, the canonical contraction transports the
ordinary strong-separator theorem from the positive contracted subdivision,
so no separate calculation is needed at subdivision-interior vertices.
The convenience wrapper a row calls #
The closed-orthant analogue of bnExists_on_subdivision_of_valid.
A checked closed-orthant record, at one integral length point together with the
face datum rep, proves rank-one existence on the contracted subdivision with
no separately supplied separator hypothesis and no contraction target: both
are discharged uniformly, the first through
DegSpec.strongSeparatorCertificate and the second through
DegSpec.canonicalContraction.
The remaining hypotheses are exactly the two the open orthant also needs
(ValidClosed in place of Valid, and FormsHold), the finite core
connectivity check on the uncontracted core, and the one genuinely new
face obligation RepInvariant — which is free on the interior
(repInvariant_evaluatedPotential_of_pos) and discharged from a chain of
collapsed slots at a face
(repInvariant_evaluatedPotential_of_zeroReach).
The census-facing form: the RepInvariant obligation is replaced by the
collapsed-slot reachability witness a contraction census already produces.
Every hypothesis is then either a Boolean check on the certificate
(checkClosed, connectedCheck), a cone membership, or census output.
On the interior of the length orthant the face datum is trivial and the statement is the existing one: this is the compatibility check that the closed layer does not weaken anything.
The closed wrapper subsumes the open one #
Nothing above weakens the existing statement: on the open orthant the closed
wrapper proves bnExists_on_subdivision_of_valid's conclusion, about the
very same subdivisionSpec. The only difference in the hypotheses is that
connectivity is asked for as the finite core cut certificate rather than as
graphConnected of the built graph — which is how the open orthant obtains
it anyway, through graph_connected_of_coreConnected.
At a strictly positive point the degenerate spec's toSpec is
subdivisionSpec: the two structures have the same core and the same lengths,
and their remaining fields are proofs.
The open-orthant conclusion, re-derived through the closed layer.
rep = id is a legal face datum at a strictly positive point (forest holds
because there are no vanishing slots), the RepInvariant obligation is free,
and DegSpec.bnExists_toSpec_iff carries the conclusion back to the ordinary
subdivisionSpec. So the closed-orthant route is a strict extension of the
open one, not an alternative to it.