Generated proof data for g4row099 #
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: 27 leaf/leaves, 63 split(s), 0 cutvertex node(s),
64 use citation(s) of 27 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 g4row099.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..
Single-block leaf data for row 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 099: 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 w0 for row 099; its entry inequalities occupy position 0 in
proof.subs.
Equations
Instances For
Named chamber leaf using w1 for row 099; its entry inequalities occupy position 1 in
proof.subs.
Equations
Instances For
Named chamber leaf using w2 for row 099; its entry inequalities occupy position 2 in
proof.subs.
Equations
Instances For
Named chamber leaf using w3 for row 099; its entry inequalities occupy position 3 in
proof.subs.
Equations
Instances For
Named chamber leaf using w4 for row 099; its entry inequalities occupy position 4 in
proof.subs.
Equations
Instances For
Named chamber leaf using w5 for row 099; its entry inequalities occupy position 5 in
proof.subs.
Equations
Instances For
Named chamber leaf using w6 for row 099; its entry inequalities occupy position 6 in
proof.subs.
Equations
Instances For
Named chamber leaf using w7 for row 099; its entry inequalities occupy position 7 in
proof.subs.
Equations
Instances For
Named chamber leaf using w8 for row 099; its entry inequalities occupy position 8 in
proof.subs.
Equations
Instances For
Named chamber leaf using w9 for row 099; its entry inequalities occupy position 9 in
proof.subs.
Equations
Instances For
Named chamber leaf using w10 for row 099; its entry inequalities occupy position 10 in
proof.subs.
Equations
Instances For
Named chamber leaf using w11 for row 099; its entry inequalities occupy position 11 in
proof.subs.
Equations
Instances For
Named chamber leaf using w12 for row 099; its entry inequalities occupy position 12 in
proof.subs.
Equations
Instances For
Named chamber leaf using w13 for row 099; its entry inequalities occupy position 13 in
proof.subs.
Equations
Instances For
Named chamber leaf using w14 for row 099; its entry inequalities occupy position 14 in
proof.subs.
Equations
Instances For
Named chamber leaf using w15 for row 099; its entry inequalities occupy position 15 in
proof.subs.
Equations
Instances For
Named chamber leaf using w16 for row 099; its entry inequalities occupy position 16 in
proof.subs.
Equations
Instances For
Named chamber leaf using w17 for row 099; its entry inequalities occupy position 17 in
proof.subs.
Equations
Instances For
Named chamber leaf using w18 for row 099; its entry inequalities occupy position 18 in
proof.subs.
Equations
Instances For
Named chamber leaf using w19 for row 099; its entry inequalities occupy position 19 in
proof.subs.
Equations
Instances For
Named chamber leaf using w20 for row 099; its entry inequalities occupy position 20 in
proof.subs.
Equations
Instances For
Named chamber leaf using w21 for row 099; its entry inequalities occupy position 21 in
proof.subs.
Equations
Instances For
Named chamber leaf using w22 for row 099; its entry inequalities occupy position 22 in
proof.subs.
Equations
Instances For
Named chamber leaf using w23 for row 099; its entry inequalities occupy position 23 in
proof.subs.
Equations
Instances For
Named chamber leaf using w24 for row 099; its entry inequalities occupy position 24 in
proof.subs.
Equations
Instances For
Named chamber leaf using w25 for row 099; its entry inequalities occupy position 25 in
proof.subs.
Equations
Instances For
Named chamber leaf using w26 for row 099; its entry inequalities occupy position 26 in
proof.subs.
Equations
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 g4row099, 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.