ValidClosed: the affine certificate grammar on the CLOSED length orthant #
ExplicitPotential.CertificateData.Valid has six conjuncts. Five of them are
already boundary-compatible; exactly one is not:
(∀ edge : Fin p,
AffineForm.positive (certificate.segment edge) = 0 ∨
AffineForm.positive (certificate.segment edge) ∈ certificate.cone)
AffineForm.positive f is the row f − 1 ≥ 0, so this conjunct says
ℓ_e ≥ 1 and it excludes every face of the orthant by construction. This
file relaxes exactly that row and nothing else.
Nothing existing is modified or weakened #
Valid is untouched, and ValidClosed is a strict weakening of it:
valid_toValidClosed : c.Valid degree → c.ValidClosed degree, andvalid_of_validClosed, the converse under the strict rows — so on the interior chamber, where the certificate does carryℓ_e ≥ 1,ValidClosedisValid, with the identical five other conjuncts.
Every existing certificate therefore satisfies ValidClosed for free, and no
consumer of Valid sees a different statement.
What the relaxed grammar still buys, and the structural surprise #
At a cone point ValidClosed gives 0 ≤ (segment e).eval point instead of
0 < …. Everything downstream that only needed non-negativity survives
verbatim (segmentNat_cast_eq_of_validClosed, rise_bounds_of_validClosed).
Everything that genuinely needed a unit step — interpolated_endpoint_bounds
— is recovered from the extra hypothesis 0 < segmentNat, which on the
degenerate graph is exactly the statement that the slot carries a unit step.
The structural surprise, and the reason this relaxation is cheap, is
rise_eq_zero_of_segment_eval_zero: the lowerForm/upperForm rows, which
Valid and ValidClosed share unchanged, read α_e·ℓ_e ≤ rise ≤ −β_e·ℓ_e,
so at ℓ_e = 0 they force rise = 0. In other words the anchor potential
is automatically constant across every collapsed slot — the rep-invariance a
DegSpec script needs is already implied by the existing cone rows, not an
extra obligation. potential_eq_of_segment_eval_zero states it in that form.
zeroSlotContribution_nonpos records the matching fact for the endpoint
bookkeeping: a collapsed slot contributes α_e + β_e ≤ 0 to
lowerEndpointContribution at the merged class and 0 to the actual
Laplacian, so the conservative bound is still conservative. That inequality
is Valid's third conjunct, unchanged.
The relaxed segment row #
The closed-orthant segment row. The first two disjuncts are exactly
Valid's row (ℓ_e ≥ 1); the last two are the relaxation (ℓ_e ≥ 0).
Any one of the four delivers 0 ≤ (segment e).eval point at a cone point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Point-independent validity on the closed length orthant. Identical to
Valid except that the segment row is SegmentRowClosed.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ValidClosed is a weakening of Valid, and equals it on the interior #
Every certificate that is Valid is ValidClosed. Nothing already proved
is weakened by moving a consumer to the closed grammar.
On the interior, ValidClosed is Valid. The two differ only in the
segment row, so supplying the strict rows recovers Valid outright.
The two grammars agree exactly on the interior chamber.
Executable checker #
Proof-free check of the relaxed segment row.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Executable closed-orthant validity checker.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Point-level consequences #
On the closed orthant every segment has non-negative integral length at
a cone point. This is the exact replacement for
segment_positive_of_valid.
The endpoint-rise bounds need no positivity at all: the lowerForm and
upperForm rows are shared verbatim with Valid.
The structural boundary-compatibility of the existing cone rows #
The surprise. At a face the shared lowerForm/upperForm rows pin
the rise to zero: they read α_e·ℓ_e ≤ rise ≤ −β_e·ℓ_e, and both bounds
collapse when ℓ_e = 0.
Restated as the rep-invariance a degenerate script needs: the anchor
potential takes the same value at the two ends of a collapsed slot. No extra
certificate field is required for this — it is already implied.
A collapsed slot contributes at most zero to the conservative endpoint
bookkeeping at the merged class, while contributing exactly zero to the
Laplacian. The inequality is Valid's third conjunct, unchanged.
Recovering the strictly positive conclusions slot by slot #
interpolated_endpoint_bounds needs a unit step, and on the closed orthant
that is precisely 0 < segmentNat. Otherwise the statement is unchanged.
The degenerate spec cut out by a closed certificate at a point #
The direct analogue of Certificate.subdivisionSpec. The contraction datum
rep is not determined by the certificate — it names which face is meant —
so it is supplied, exactly as in Utilities.Certificate.DegenerateSpec.DegSpec. Note that
core_loopless becomes rep_loopless, and that rep_zero is the only new
obligation beyond the census data.
Turn evaluated affine segment lengths and a checked idempotent contraction representative into a degenerate subdivision specification, retaining the supplied looplessness and forest-count guarantees.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Genus of the face cut out by a closed certificate: unchanged from the
core's p − n + 1, by DegSpec.genus_graph.
At a strictly positive point the degenerate spec is the ordinary
subdivisionSpec: same core, same lengths, and rep = id.