{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R33",
  "content_hash": null,
  "slug": "asser-artifact-monadic-spectrum-census",
  "type": "artifact",
  "title": "Exact bounded census for monadic spectra",
  "summary": "The replay checks every truncated count vector for up to three unary predicates and confirms the generator, count, complement, and sharp-rank formulas.",
  "relevance": "For Asser's complement problem for first-order spectra, record asser-artifact-monadic-spectrum-census (“Exact bounded census for monadic spectra”) supplies evidence or a replay used to check the packet. The record states: The replay checks every truncated count vector for up to three unary predicates and confirms the generator, count, complement, and sharp-rank formulas.",
  "relevance_source": "recorded",
  "body": "A spectrum signature records membership through cardinality 34 and a separate eventual-tail bit. With \\(r\\) unary predicates, the program enumerates all \\((q+1)^{2^r}-1\\) positive-domain truncated count vectors for \\(1\\le r,q\\le3\\). It converts every vector to an exact singleton or a tail and checks that the distinct contributions are precisely the generators in asser-claim-monadic-rank-classification. It then forms every union of those generators. The largest census covers 65,535 truncated vectors and 589,824 distinct spectra at \\(r=q=3\\).\n\nFor each bounded pair \\((r,q)\\), the replay verifies the formulas for finite, cofinite, and total spectra. It complements every enumerated signature, checks the same-rank failure count, and tests membership at rank \\(q+1\\) without assuming the enumerated family. It also constructs the sharp interval witness. The deeper one-unary run enumerates ranks one through nine, reports ranks one through eight, checks every subset of q-types through rank three, and reconstructs all q-types from labelled unary structures through rank four. A separate recursive solver plays 16,470 bounded Ehrenfeucht-Fraïssé games for one and two unary predicates and matches every result against the truncated-count criterion.\n\nSpectrum operations use finite integer bitsets. The game solver uses finite tuples and recursion. A supervisor enforces the wall-clock limit and polls the two-process resident set every 0.02 seconds. The worker enforces the CPU limit and requests an address-space limit where the platform supports it. The replay uses no network access or random choice.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "every collapsed spectrum generator for one through three unary predicates at ranks one through three, plus the one-unary census through rank nine",
    "bounds": {
      "unary_predicates": {
        "min": 1,
        "max": 3
      },
      "one_unary_quantifier_rank": {
        "min": 1,
        "max": 9
      },
      "one_unary_reported_quantifier_rank": {
        "min": 1,
        "max": 8
      },
      "general_census_quantifier_rank": {
        "min": 1,
        "max": 3
      },
      "largest_truncated_vector_census": {
        "min": 65535,
        "max": 65535
      },
      "largest_distinct_spectrum_census": {
        "min": 589824,
        "max": 589824
      },
      "direct_ef_game_pair_checks": {
        "min": 16470,
        "max": 16470
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "repository_python_exact_q_type_census",
    "command": "python3 tools/first_order_spectra_complement_replay.py",
    "entrypoint": "tools/first_order_spectra_complement_replay.py",
    "runtime": "CPython 3.9.6 standard library, macOS 26.2 arm64",
    "source": "tools/first_order_spectra_complement_replay.py",
    "citation": {
      "url": "https://doi.org/10.23638/LMCS-14(2:4)2018",
      "locator": "Internal repository replay tools/first_order_spectra_complement_replay.py, command python3 tools/first_order_spectra_complement_replay.py, executed under its stated resource bounds on 2026-07-28"
    },
    "dependencies": [
      {
        "name": "CPython standard library",
        "version": "3.9.6",
        "license": "Python-2.0"
      }
    ],
    "outputs": {
      "format": "one canonical compact JSON object followed by LF",
      "source_bytes": 20155,
      "source_line_count": 616,
      "source_sha256": "10e522fb7c6ec761194b45788aafaf4a2d1a4993a9322e5c0238cc63f3b7c74d",
      "stdout_bytes": 8666,
      "stdout_sha256": "5b44b485524bb5b81b13e475c4fb06e42258e92b23c468a3ea9289884043146a",
      "direct_ef_game_crosscheck": {
        "pair_checks": 16470,
        "unary_predicate_bounds": [
          1,
          2
        ],
        "quantifier_rank_bounds": [
          1,
          3
        ],
        "maximum_model_sizes": {
          "r1": 6,
          "r2": 4
        },
        "result": "all direct games matched the truncated-count criterion"
      },
      "direct_subset_crosscheck_ranks": [
        1,
        3
      ],
      "labelled_structure_crosscheck_ranks": [
        1,
        4
      ],
      "one_unary_enumerated_quantifier_ranks": [
        1,
        9
      ],
      "one_unary_reported_rows": [
        {
          "q": 1,
          "distinct_spectra": 3,
          "same_rank_complement_failures": 1,
          "signatures_sha256": "6b446971fc59edb8fc5b614a08fdd5525720218d838ae4239ded5bd0cecf5b2d"
        },
        {
          "q": 2,
          "distinct_spectra": 12,
          "same_rank_complement_failures": 4,
          "signatures_sha256": "03a7d4222e0da2d40c073a5b3b8ad1abe99bb9c45196953b82e632270fd93ecd"
        },
        {
          "q": 3,
          "distinct_spectra": 48,
          "same_rank_complement_failures": 16,
          "signatures_sha256": "e9d22ecbfcfe6422bd18a7e8e9b1b8e784e8743189738b0cdaafd163c41431e9"
        },
        {
          "q": 4,
          "distinct_spectra": 192,
          "same_rank_complement_failures": 64,
          "signatures_sha256": "98e35725fd40015c040e9e8e5839c4039e9c672c5f1046bf9f2b29a4a2c0e3aa"
        },
        {
          "q": 5,
          "distinct_spectra": 768,
          "same_rank_complement_failures": 256,
          "signatures_sha256": "99b5c9698a064003073e157a87beeec356f4fa17856dbd732bc4d4b39b903fee"
        },
        {
          "q": 6,
          "distinct_spectra": 3072,
          "same_rank_complement_failures": 1024,
          "signatures_sha256": "7805a4ec1ae07ad146152a729a6bf0394b03393d9dac756ff2c2df62e4a05eb7"
        },
        {
          "q": 7,
          "distinct_spectra": 12288,
          "same_rank_complement_failures": 4096,
          "signatures_sha256": "3478190088407430618799069ad85919b9f67a6f4664630a0ac99597ca1845b2"
        },
        {
          "q": 8,
          "distinct_spectra": 49152,
          "same_rank_complement_failures": 16384,
          "signatures_sha256": "deb098fd47056103a9eda126a8f4a5bd536e3a1b44db30fe90bcc7db48e8682c"
        }
      ],
      "general_reported_rows": [
        {
          "r": 2,
          "q": 1,
          "distinct_spectra": 5,
          "same_rank_complement_failures": 3,
          "signatures_sha256": "4f80731ae335b92e092ec8b665c20631d63512c228601bcc6bb36bf64029d364"
        },
        {
          "r": 2,
          "q": 2,
          "distinct_spectra": 80,
          "same_rank_complement_failures": 48,
          "signatures_sha256": "2b09da482f02e558ec96400b771dbe7c367bce2bb3db0fc210f958e540ceb468"
        },
        {
          "r": 2,
          "q": 3,
          "distinct_spectra": 1280,
          "same_rank_complement_failures": 768,
          "signatures_sha256": "8e33081a267794d146c8d94e2d9829d58c5fe00ee1039e6a57557681cb3a02a8"
        },
        {
          "r": 3,
          "q": 1,
          "distinct_spectra": 9,
          "same_rank_complement_failures": 7,
          "signatures_sha256": "2da9cc09cd429977e94c816cb76064981eddc9d6428f0e83f962622d2cdfae02"
        },
        {
          "r": 3,
          "q": 2,
          "distinct_spectra": 2304,
          "same_rank_complement_failures": 1792,
          "signatures_sha256": "f4953bb3f75de8607160ddcca07ec70eb764be8aeec1ec596f0a93a721c8a655"
        },
        {
          "r": 3,
          "q": 3,
          "distinct_spectra": 589824,
          "same_rank_complement_failures": 458752,
          "signatures_sha256": "026fe6d5a4c1ef6c121f77d1712683ae02f40bf1acbecc014138b60db5595a72"
        }
      ]
    },
    "runtime_seconds": 9.82
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.23638/LMCS-14(2:4)2018",
    "locator": "Internal repository replay tools/first_order_spectra_complement_replay.py, command python3 tools/first_order_spectra_complement_replay.py, executed under its stated resource bounds on 2026-07-28"
  },
  "models": [],
  "relations": [
    {
      "slug": "R39",
      "title": "Every fixed monadic vocabulary needs at most one extra rank",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R36",
      "title": "Sentence negation does not complement the spectrum",
      "object_type": "attempt",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "first-order-spectra-complement-closure",
      "title": "first order spectra complement closure",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}