Generated proof data for g4row100 #
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: 18 leaf/leaves, 34 split(s), 0 cutvertex node(s),
38 use citation(s) of 21 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 g4row100.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 100: core divisor [0, 0, 0, 1, 1, 0], 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 100: core divisor [0, 0, 0, 1, 1, 0], 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 100: core divisor [0, 0, 0, 1, 1, 0], 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 100: core divisor [0, 0, 0, 1, 1, 0], 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 100: core divisor [0, 0, 0, 1, 1, 0], 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 100: core divisor [0, 0, 0, 1, 1, 0], 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 100: core divisor [0, 0, 0, 1, 1, 0], 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 100: core divisor [0, 0, 0, 1, 1, 0], 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 100: core divisor [0, 0, 0, 1, 1, 0], 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 100: core divisor [0, 0, 0, 1, 1, 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 100: core divisor [0, 0, 0, 1, 1, 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 100: core divisor [0, 0, 0, 1, 1, 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 100: core divisor [0, 0, 0, 1, 1, 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 100: core divisor [0, 0, 0, 1, 1, 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 100: core divisor [0, 0, 0, 1, 1, 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 100: core divisor [0, 0, 0, 1, 1, 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 100: core divisor [0, 0, 0, 1, 1, 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 100: core divisor [0, 0, 0, 1, 1, 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 100; its entry inequalities occupy position 0 in
proof.subs.
Equations
Instances For
Named chamber leaf using rw1 for row 100; its entry inequalities occupy position 1 in
proof.subs.
Equations
Instances For
Named chamber leaf using rw2 for row 100; its entry inequalities occupy position 2 in
proof.subs.
Equations
Instances For
Named chamber leaf using rw3 for row 100; its entry inequalities occupy position 3 in
proof.subs.
Equations
Instances For
Named chamber leaf using rw4 for row 100; its entry inequalities occupy position 4 in
proof.subs.
Equations
Instances For
Named chamber leaf using rw5 for row 100; its entry inequalities occupy position 5 in
proof.subs.
Equations
Instances For
Named chamber leaf using rw6 for row 100; its entry inequalities occupy position 6 in
proof.subs.
Equations
Instances For
Named chamber leaf using rw7 for row 100; its entry inequalities occupy position 7 in
proof.subs.
Equations
Instances For
Named chamber leaf using rw8 for row 100; its entry inequalities occupy position 8 in
proof.subs.
Equations
Instances For
Named chamber leaf using w9 for row 100; its entry inequalities occupy position 9 in
proof.subs.
Equations
Instances For
Named chamber leaf using w10 for row 100; its entry inequalities occupy position 10 in
proof.subs.
Equations
Instances For
Named chamber leaf using w11 for row 100; its entry inequalities occupy position 11 in
proof.subs.
Equations
Instances For
Named chamber leaf using w12 for row 100; its entry inequalities occupy position 12 in
proof.subs.
Equations
Instances For
Named chamber leaf using w13 for row 100; its entry inequalities occupy position 13 in
proof.subs.
Equations
Instances For
Named chamber leaf using w14 for row 100; its entry inequalities occupy position 14 in
proof.subs.
Equations
Instances For
Named chamber leaf using w15 for row 100; its entry inequalities occupy position 15 in
proof.subs.
Equations
Instances For
Named chamber leaf using w16 for row 100; its entry inequalities occupy position 16 in
proof.subs.
Equations
Instances For
Named chamber leaf using w17 for row 100; its entry inequalities occupy position 17 in
proof.subs.
Equations
Instances For
Chamber subtree for row 100, first splitting on length[0] - length[2] + length[6] ≥ 0, then
citing earlier subtree indices 0, 1, 2, 3, 4, 5, 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 100, first splitting on length[0] - length[2] + length[6] ≥ 0, then
citing earlier subtree indices 9, 10, 11, 12, 13, 14, 15, 16, 17. 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 100, first splitting on -1 + length[6] ≥ 0, then citing earlier
subtree indices 18, 19. 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 g4row100, 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.