Generated proof data for g4row096 #
This checked payload is a deep-embedded proof tree.
The module is passive: it carries the proof tree of the .rpf as data, one
decide that the public deep-embedded checker under
Utilities/Subdivision/ClosedRowProof/ accepts it, and the row obligation its theorems
then give. Nothing here asserts acceptance on its own authority.
Shape: 9 leaf/leaves, 13 split(s), 0 cutvertex node(s),
19 use citation(s) of 14 named subtree(s),
core n = 6, p = 9, goal BNExists _ 1 3 on the closed length
orthant.
Everything is List ℤ read with List.getD; the representation keeps kernel reduction compact.
The entailment certificates were synthesised by exact rational Farkas and
re-verified over ℤ before emission; the kernel re-checks them anyway.
The public atlas core named by g4row096.rpf.
Equations
Instances For
The node data #
One def per LEAF witness and per REDUCE CUTVERTEX node of the .rpf, in
depth-first order. They are split out rather than inlined into tree because
maxHeartbeats is charged per declaration..
Multiple-block leaf data for row 096: core divisor [1, 0, 0, 0, 0, 1], 1 positioned chip
terms, and six anchor firing plans with exact entailment receipts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Single-block leaf data for row 096: core divisor [1, 0, 0, 1, 0, 1], 0 positioned chip
terms, and six anchor firing plans with exact entailment receipts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Multiple-block leaf data for row 096: core divisor [1, 0, 0, 0, 0, 1], 1 positioned chip
terms, and six anchor firing plans with exact entailment receipts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Multiple-block leaf data for row 096: core divisor [1, 0, 0, 0, 0, 1], 1 positioned chip
terms, and six anchor firing plans with exact entailment receipts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Multiple-block leaf data for row 096: core divisor [1, 0, 0, 0, 0, 1], 1 positioned chip
terms, and six anchor firing plans with exact entailment receipts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Multiple-block leaf data for row 096: core divisor [1, 0, 0, 0, 0, 1], 1 positioned chip
terms, and six anchor firing plans with exact entailment receipts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Single-block leaf data for row 096: core divisor [1, 0, 0, 1, 0, 1], 0 positioned chip
terms, and six anchor firing plans with exact entailment receipts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Single-block leaf data for row 096: core divisor [1, 0, 0, 1, 0, 1], 0 positioned chip
terms, and six anchor firing plans with exact entailment receipts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Single-block leaf data for row 096: core divisor [1, 0, 0, 1, 0, 1], 0 positioned chip
terms, and six anchor firing plans with exact entailment receipts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The named subtrees #
One def per (sub k (entry ...) body) of the .rpf. Each is checked once,
in the closed root domain extended by its entry forms; the use citations in
main re-derive those forms from their own chamber. The entry forms are
listed alongside the body in proof.subs below.
Named chamber leaf using rw0 for row 096; its entry inequalities occupy position 0 in
proof.subs.
Equations
Instances For
Named chamber leaf using w1 for row 096; its entry inequalities occupy position 1 in
proof.subs.
Equations
Instances For
Named chamber leaf using rw2 for row 096; its entry inequalities occupy position 2 in
proof.subs.
Equations
Instances For
Named chamber leaf using rw3 for row 096; its entry inequalities occupy position 3 in
proof.subs.
Equations
Instances For
Named chamber leaf using rw4 for row 096; its entry inequalities occupy position 4 in
proof.subs.
Equations
Instances For
Named chamber leaf using rw5 for row 096; its entry inequalities occupy position 5 in
proof.subs.
Equations
Instances For
Named chamber leaf using w6 for row 096; its entry inequalities occupy position 6 in
proof.subs.
Equations
Instances For
Named chamber leaf using w7 for row 096; its entry inequalities occupy position 7 in
proof.subs.
Equations
Instances For
Named chamber leaf using w8 for row 096; its entry inequalities occupy position 8 in
proof.subs.
Equations
Instances For
Chamber subtree for row 096, first splitting on length[0] - 2*length[3] - length[7] - length[8] ≥ 0, then citing earlier subtree indices 3, 4, 5. The other branch uses the integer
complement of the split inequality.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Chamber subtree for row 096, first splitting on length[0] - 2*length[3] - length[7] - length[8] ≥ 0, then citing earlier subtree indices 6, 7, 8. The other branch uses the integer
complement of the split inequality.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Chamber subtree for row 096, first splitting on -1 + length[7] ≥ 0, then citing earlier
subtree indices 9, 10. The other branch uses the integer complement of the split inequality.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Chamber subtree for row 096, first splitting on length[0] - length[3] - length[7] - length[8] ≥ 0, then citing earlier subtree indices 2, 11. The other branch uses the integer complement
of the split inequality.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Chamber subtree for row 096, first splitting on -length[0] + length[3] + length[8] ≥ 0, then
citing earlier subtree indices 0, 1, 12. The other branch uses the integer complement of the
split inequality.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The proof of the .rpf, verbatim: the named subtrees with their entry
contexts, in declaration order, and the main tree. A use node carries one
entailment certificate per entry form of the subtree it cites.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The deep-embedded checker accepts, by kernel reduction.
decide +kernel uses ordinary kernel reduction and avoids duplicate evaluation by the elaborator.
BNExists … 1 3 for catalog row g4row096, from its .rpf and nothing
else. Quantified over every length vector whose vanishing set is a non-loopy
forest -- every subdivision of the core, and every equal-genus contraction of
one.
The object the conclusion speaks about has the row's genus at every face.