For the order-line schema in artifacts/instances/dbdesign/orders-schema.dbd, the candidate keys are EXACTLY {line_uuid} and {order_id, line_no}: the application's surrogate key and the natural key are both keys, neither is redundant, and there are no others. The schema is not in BCNF -- five of its seven dependencies have a determinant that is not a superkey -- and it is not in 3NF either, because `f_order` puts the non-prime attributes customer_id and warehouse on the right of a dependency whose determinant is not a superkey. The prime attributes are exactly line_uuid, order_id and line_no.
The completeness of the key list is established by sweeping all 2^10 = 1024 subsets of the attributes. Each subset either contains one of the two reported keys (640 of them) or is issued a two-row relation over the schema that satisfies all seven dependencies while its rows agree on the subset and differ elsewhere -- 384 such relations, every one of them checked. The 3520 removal tests behind the minimality claim were ALL decided, so the minimality is absolute in the sense of ADR-0455 rather than budget-relative.
The graph shows direct ledger edges. Follow a node to open its artifact page.
1 direct dependencies0 direct dependents
Evidence
orders-candidate-key-sweep
Kind
exhaustive-enumeration
Status
checked
Supports: The candidate keys are EXACTLY {line_uuid} and {order_id, line_no}: all 1024 subsets of the ten attributes were examined and each non-superkey was issued a checked two-row relation.
Measured 2026-08-15: 1024 subsets swept, 640 containing a reported key, 384 issued a counterexample relation and 384 of those checked. 3520 removal tests, ALL DECIDED -- attribute closure is a total function on a finite lattice, so no budget can make one `unknown`, and the minimality claim is therefore ABSOLUTE in the sense of ADR-0455 rather than budget-relative. The sweep also fails if a subset containing a reported key turns out not to be a superkey, or if a subset containing none turns out to be one, which is what makes the list COMPLETE rather than merely correct. Each reported key additionally carries a replayed Armstrong derivation of key -> R.
orders-normal-form-violation-witnesses
Kind
witness-replay
Status
checked
Supports: The schema is in neither BCNF nor 3NF, each violation carrying the offending dependency plus a two-row relation showing its determinant is not a superkey.
Five of the seven dependencies violate BCNF; the same five violate 3NF because each has a non-prime attribute on the right. The prime attributes -- line_uuid, order_id, line_no -- come from the exhaustive sweep above, so the 3NF verdict inherits its completeness. The BCNF verdict examines only the dependencies IN F, which is sufficient by an argument recorded in the module documentation and carried in the axiom footprint as the one assumption here that is a theorem rather than a measurement.
dbdesign-checkers-fail-closed
Kind
instance-pin
Status
checked
Supports: The checkers backing this fact REJECT a false claim of every kind it makes, so a passing run is evidence rather than a report that a tool finished.
Checker command
scripts/check-dbdesign-negative-controls.sh
Evidence notes
22 assertions, 2.1 s warm. 13 committed instance files each pin exactly ONE false answer -- an unimplied dependency declared implied, a candidate-key list with a key missing, a list with a non-key added, a BCNF verdict flipped, a 3NF verdict flipped (which a checker conflating the two normal forms would accept), a lossy split declared lossless and the reverse, a preserved dependency set declared lost and the reverse, and a query containment in each direction -- and every one must exit non-zero. Four more assertions cover the shape of the gate itself: a wrong --expect-checks count, an instance run through the wrong checker, a --verify-formal script whose negation is SATISFIABLE, and a --verify-formal target that asserts nothing. One further control, no-expectations.dbd, pins nothing at all and must be REFUSED rather than swept -- the `40 of 162 checker runs exit 0 on completion alone` failure this ledger measured on 2026-08-15. Finally three assertions require the TRUE instances to still be accepted, without which a checker that rejected everything would pass the whole sweep. Measured this run: 22 of 22.
Provenance
{
"date": "2026-08-15",
"established_by": "axeyum lane `db-design`, 2026-08-15: crates/axeyum-scenarios/src/dbdesign/normal_forms.rs over the committed instance",
"source": "schema authored by this lane; not extracted from any corpus",
"prior_art": [
{
"who": "C. L. Lucchesi and S. L. Osborn",
"what": "All candidate keys of a schema can be enumerated in time polynomial in the SIZE OF THE OUTPUT as well as the input, deciding whether a key of cardinality at most k exists is NP-complete, and deciding whether a specified attribute is prime is NP-complete. The exhaustive 2^n sweep used here is the brute-force alternative, affordable only because the instance is small -- and the fact says 1024 rather than implying a clever algorithm.",
"where": "Candidate keys for relations, Journal of Computer and System Sciences 17(2):270-279",
"year": 1978,
"attribution": "citation from the AHV bibliography p. 645; the three results read from the paper's abstract via a publisher landing page and corroborated by Maier, The Theory of Relational Databases (1983), Ch. 6 p. 122. This lane did not read the paper."
},
{
"who": "E. F. Codd",
"what": "Boyce-Codd normal form: every non-trivial dependency has a superkey determinant. Both AHV (Ch. 11 notes, p. 265) and Maier (Ch. 6, p. 122) attribute BCNF to this paper, of which Codd is the sole author as cited; the popular attribution to Boyce and Codd jointly, and C. J. Date's claim that Heath (1971) has the definition first, are textbook lore this lane could not verify to a primary source.",
"where": "Recent investigations in relational data base systems, Information Processing 74 (Proc. IFIP Congress, Stockholm), North-Holland, pp. 1017-1021",
"year": 1974,
"attribution": "citation read on the AHV bibliography p. 630 and the attribution sentence at AHV p. 265 and Maier p. 122; primary source not consulted."
},
{
"who": "Catriel Beeri and Philip A. Bernstein",
"what": "Testing whether a schema (R, F) is in BCNF is polynomial (in fact linear) when F is given explicitly -- it suffices to check the dependencies IN F, which is what this run does. Testing whether a SUBSCHEMA (V, pi_V(F)) is in BCNF is co-NP-complete (equivalently, deciding that it violates BCNF is NP-complete, which is how Maier and most textbooks phrase it).",
"where": "Computational Problems Related to the Design of Normal Form Relational Schemas, ACM Transactions on Database Systems 4(1):30-59",
"year": 1979,
"attribution": "the easy half read at AHV Exercise 11.12(a) p. 267, the hard half at AHV Exercise 11.12(b) p. 267 (tagged [BB79]) and in the running text at AHV p. 256; Maier p. 122 states the same result with the opposite polarity. Primary source not consulted."
}
]
}
