leaf_sound: the row-proof leaf, lowered to Lean #
This is step B of the proof-data source. A LEAF node of a row proof carries a
local witness (spec §4.3); this file turns an accepted witness into
BNExists … 1 d on the degenerate subdivision determined by any length
vector whose vanishing set is a non-loopy forest.
Representation discipline #
Every generated form is a List ℤ addressed with List.getD, as in
the corresponding closed-row proof module. §1 below is the only place where a form is turned
into the Fin-indexed ExplicitPotential.AffineForm the existing certificate
layer speaks: toAffineForm reads the coefficients out of the list with
getD, so no ![…] and no Matrix.cons ever appears.
Where the soundness hazard is discharged #
RESULTS.md §9 records that on a core carrying a loop the core vertices are
not rank determining, so the strong-separator step is unsound there. In
this file that hazard is discharged in exactly one place: censusSpec's
rep_loopless field, which is supplied by the row obligation's own
¬ IsLoopy census hypothesis through
ContractionForestCensusGeneral.rep_loopless_of_not_isLoopy. Every
downstream separator fact (DegSpec.strongSeparatorCertificate) is
hypothesis-free precisely because a DegSpec cannot be built without that
field. Dropping hNotLoopy from leaf_sound is therefore not possible: the
conclusion does not typecheck without it.
What the checker accepts, and what it deliberately refuses #
Witness is the spec's §4.3 record verbatim (chips, a block list per slot,
head/tail slack). Witness.leafChecks is fail-closed on the parts of
that record whose Lean support does not exist yet:
- it requires
chips = [], and - it requires exactly one block per slot (
k_e = 1),
so that no named interior point ever arises. With k_e = 1 there are no
interior named points, W1's slack and W4's interior residual are vacuous, and
W5 collapses to the per-core-vertex integer test ValidClosed already makes.
This is not a toy restriction: it is exactly the leaf the implemented
generator emits. the proof-data source's verify_leaf checks precisely
lo_e ≤ hi_e, lo_e·ℓ_e ≤ F(head e) − F(tail e) ≤ hi_e·ℓ_e, and the core
residual, and all four leaves in the proof-data source (banana3,
g4row002, g4row010, g4row011) have (chips) empty and one (b …) per
slot. The multi-block half of §4.3 is unexercised by every accepted proof in
the catalog; see the note at the end of this file for what it would cost.
§1 From a List ℤ form to an AffineForm #
eval g x = dot g (1 :: x) truncates at the shorter list, which is what makes
the translation unconditional: a form longer than m + 1 has its tail ignored
on both sides.
A List ℤ form, read as an AffineForm m: the head is the constant and
entry i + 1 is the coefficient of coordinate i.
Equations
Instances For
A passive affine-cover cell supplies exactly the inequality half of a row-proof context. This is the generic bridge used by generated conditional rich-plan covers; no coordinate is assumed to be a graph length here.
The coordinate forms #
§2 The leaf witness, spec §4.3 #
The record is the specification's, verbatim; the checker is what refuses the half of it that has no Lean support (see the module docstring).
One block of a slot script: over the stretch ending at endForm the script
rises by rise, its first unit slope is at least lo and its last at most
hi. This is rowproof's (b end rise lo hi).
- endForm : Form
The affine form naming the right end of the stretch.
- rise : Form
The affine form naming the total rise across the stretch.
- lo : ℤ
Lower bound on the first unit slope.
- hi : ℤ
Upper bound on the last unit slope.
Instances For
The firing script attached to one anchor: a potential at each core vertex, a block list per slot, the declared endpoint slacks of W1, and the entailment certificates for the two realizability rows of §13.1.
One form per core vertex.
One nonempty block list per slot.
α_eof W1.ω_eof W1.Per slot, a certificate of
rise_e − lo_e·σ_e ≥ 0.Per slot, a certificate of
hi_e·σ_e − rise_e ≥ 0.
Instances For
Rich multi-block leaf data #
Witness below is retained for the already-generated one-block catalog. The
full RPF leaf has more receipts than that compact record can carry, so the
multi-block path uses a separate record rather than adding required fields to
AnchorPlan and invalidating every existing generated module. PTree will
gain the corresponding leaf constructor once richLeafChecks and its
soundness theorem are assembled below.
The three local entailment receipts for a block: its length is nonnegative, and its declared rise lies between the endpoint-slope bounds.
- monotone : Cert
Entailment receipt asserting that the block endpoint is no earlier than its starting point.
- lower : Cert
Entailment receipt for the lower realizability inequality: the declared rise is at least the lower slope bound times the block length.
- upper : Cert
Entailment receipt for the upper realizability inequality: the declared rise is at most the upper slope bound times the block length.
Instances For
Missing rich receipts fail closed because every constituent default has
k = 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A firing plan with all data required by RPF W1--W5. The outer list indices
are slots and inner indices are block numbers; separationCert e i j is the
strict W4 receipt for the run beginning at C-index i and ending at j.
The lowerer synthesises every receipt with the existing exact Farkas engine.
Affine potential values indexed by core vertex for this anchor firing plan.
The ordered interpolation blocks on each slot, with outer indices naming slots and inner indices naming blocks.
The per-slot W1 parameter α, bounding the initial named points allowed to coincide with the tail endpoint.
The per-slot W1 parameter ω, bounding the final named points allowed to coincide with the head endpoint.
- blockCert : List (List RichBlockCert)
Per-slot, per-block receipts for nonnegative block length and the two rise bounds.
Per-slot strict-positivity receipts placing the first point beyond the allowed tail slack after the tail.
Per-slot strict-positivity receipts placing the last point before the allowed head slack before the head.
Strict separation receipts indexed by slot and the first and last named-point indices of a W4 run.
Instances For
The empty fallback plan used when an anchor index is absent from a rich witness.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The full multi-block/chip RPF leaf. This is deliberately distinct from
the old Witness, so the existing single-block generated modules remain
byte-compatible while new lowering selects the rich soundness path.
The divisor coefficients at the original core vertices, indexed by vertex number.
Named slot chips as triples of slot index, affine position form, and signed integer coefficient.
- anchors : List RichAnchorPlan
One rich firing plan for each core-vertex anchor.
Per-slot entailment receipts establishing nonnegative slot length from the ambient context.
Instances For
Look up the rich firing plan for an anchor, returning the empty default plan for an absent entry.
Equations
Instances For
Read a specified interpolation block, using the default block with inconsistent slope bounds for a missing entry.
Equations
- w.block a e i = (w.blockList a e).getD i Utilities.Subdivision.ClosedRowProof.Block.dflt
Instances For
Read an anchor’s receipts for a slot and block, falling back to the default rich block certificate.
Equations
- w.blockReceipt a e i = ((w.plan a).blockCert.getD e []).getD i Utilities.Subdivision.ClosedRowProof.RichBlockCert.dflt
Instances For
Read the strict separation receipt for a run of named points, indexed by anchor, slot, and run endpoints.
Equations
- w.separationReceipt a e i j = (((w.plan a).separationCert.getD e []).getD i []).getD j Utilities.Subdivision.ClosedRowProof.Cert.dflt
Instances For
The local witness carried by a LEAF node.
The divisor's coefficient at each core vertex.
Chips in slot interiors:
(slot, position form, coefficient).- anchors : List AnchorPlan
One plan per core vertex, since the anchors are the core classes.
Per slot, a certificate of
σ_e ≥ 0from the ambient context.
Instances For
The plan of anchor a.
Equations
Instances For
The first (and, once leafChecks accepts, only) block of slot e.
Equations
- w.block a e = (w.blockList a e).getD 0 Utilities.Subdivision.ClosedRowProof.Block.dflt
Instances For
§3 The certificate a witness denotes #
ExplicitPotential.CertificateData is the existing arithmetic record; a
single-block leaf is exactly one, with α_e = lo_e and β_e = −hi_e. The
cone is synthesised here rather than transcribed: it holds precisely the
rows the semantics needs, and FormsHold for them is discharged by the
entailment layer of the corresponding closed-row proof module, not by cone membership.
The row rise_e − lo_e·σ_e ≥ 0, written so that it is definitionally
(leafCertificate …).lowerForm.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The row hi_e·σ_e − rise_e ≥ 0, written so that it is definitionally
(leafCertificate …).upperForm.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The synthesised cone: the slot lengths and, per anchor and slot, the two realizability rows.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The explicit-potential certificate a single-block leaf denotes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
§4 The Boolean leaf checker #
The leaf checker. Γ is the context the tree layer has accumulated at
this node; degree is the goal's degree.
Restrictions, both fail-closed and both deliberate: no chips, and exactly one block per slot. See the module docstring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
§5 The degenerate subdivision determined by a length vector #
This is where the soundness hazard of RESULTS.md §9 is discharged: the
rep_loopless field below is supplied by hNotLoopy and by nothing else.
The row obligation's target object. The degenerate subdivision of
core at lengths ℓ, given the two census hypotheses of spec §3.
hForest is genus preservation and hNotLoopy is looplessness of the
contracted core — which is exactly what the strong-separator step needs, and
is why DegSpec.strongSeparatorCertificate can be hypothesis-free.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Two degenerate specs with the same core, lengths and representative map are
equal; the remaining fields are Props.
§6 leaf_sound #
The leaf is sound.
If leafChecks accepts the witness against the context Γ, then at every
integral point of Γ the goal BNExists … 1 degree holds on the degenerate
subdivision determined by the induced length vector, for every length vector
whose vanishing set is a non-loopy forest.
Provenance of the hypotheses:
hp,hlen— the format's own convention that coordinateeis the length of slote(spec §4.1);hn— needed to state the conclusion at all (DegSpec.core_nonempty);hchk— the Boolean leaf checker;hΓ— the context holds at the point; supplied by the tree layer, and trivial at the closed root (seeleaf_sound_closed_root);hForest,hNotLoopy— the two census hypotheses of spec §3, inputs to the row obligation.hNotLoopyis the one that pays for the rank-determining-set step; seecensusSpec.
§7 The root of a (domain closed) proof #
Spec §4.1: the root context is the closed orthant [σ_0, …, σ_{p−1}] with no
equalities. Specialising leaf_sound there removes point, hΓ and hlen
and leaves exactly the row obligation of §3: for every ℓ : Fin p → ℕ whose
vanishing set is a non-loopy forest, the goal holds.
The closed-orthant root context.
Equations
Instances For
The row obligation, verbatim. An accepted single-block leaf at the
closed root proves the goal on every face of the closed length orthant whose
vanishing set is a non-loopy forest. Compare spec §3 and
AllMarksCoreCase.SolvedAllMarksClosedCensus.
§8 What the multi-block half of §4.3 would cost #
Spec §5.3 calls the leaf "composition, not new mathematics" and points at
Certificate/SlopeScript.lean and Certificate/AffinePositionMultiBreak.lean
for the multi-break script. That is only true on the open orthant: both
of those modules are stated for SubdivisionGraph.Spec, which carries
length_pos, whereas the leaf obligation of a (domain closed) proof lives
on Utilities.Certificate.DegenerateSpec.DegSpec, where lengths may vanish. The closed-orthant
script layer that exists is
Utilities.Certificate.DegenerateSpec.DegSpec.interpolatedScript — one affine interpolation per
slot, i.e. exactly k_e = 1.
So supporting k_e ≥ 2 needs a genuinely new construction: a piecewise-affine
script on DegSpec whose break positions are affine forms that may collide
with each other and with the two endpoints, plus its prin at interior and
core vertices, plus the α_e/ω_e slack reading of W5. That is the
DegSpec port of SlopeScript + AffinePositionMultiBreak, and it is where
W4 (which is vacuous here) starts doing work.
Nothing in the catalog needs it yet: the proof-data source only ever emits one block per slot, and §13.5 proves that a single whole-orthant leaf on a two-edge-connected core with more core vertices than degree cannot exist at all — those rows need a chamber split or an interior chip, which is the tree layer and the chips, not more blocks.