{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R616",
  "content_hash": null,
  "slug": "q12ns794-artifact-fourier-edge-verifier",
  "type": "artifact",
  "title": "Exact pair-sum, Walsh-transform, and edge-bound verifier",
  "summary": "A standard-library Python program checks both families by two exact methods and reproduces the rational universal upper bound.",
  "relevance": "For Maximum half-noise stability of a 794-set in the twelve cube, record q12ns794-artifact-fourier-edge-verifier (“Exact pair-sum, Walsh-transform, and edge-bound verifier”) supplies evidence or a replay used to check the packet. The record states: A standard-library Python program checks both families by two exact methods and reproduces the rational universal upper bound.",
  "relevance_source": "recorded",
  "body": "The program constructs the initial segment and Hamming ball from their definitions. For each family it evaluates all ordered pairs directly. It then performs an unnormalized fast Walsh transform and applies the exact kernel eigenvalues \\(4^{12-k}2^k\\). Equality of the two answers catches distance-counting and normalization errors.\n\nThe program counts internal edges, evaluates Harper's extremal count \\(\\sum_{j=0}^{793}\\operatorname{popcount}(j)=3693\\), and carries the secant calculation with rational arithmetic. The printed upper integer incorporates the divisibility-by-four argument given in the interval claim. The verifier checks a calculation derived from Harper's theorem. It does not enumerate all subsets of size 794.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the explicit binary initial segment and radius-four Hamming ball in Q_12, together with the universal Fourier and edge-isoperimetric upper-bound calculation at cardinality 794",
    "bounds": {
      "dimension": {
        "min": 12,
        "max": 12
      },
      "cardinality": {
        "min": 794,
        "max": 794
      },
      "cube_vertices": {
        "min": 4096,
        "max": 4096
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_deterministic_verifier",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "Python 3.10 or later, standard library only",
    "citation": {
      "url": "https://doi.org/10.1016/S0021-9800(66)80059-5",
      "locator": "Inline Python 3 verifier prepared on 2026-07-25"
    },
    "outputs": "lex_size=794 lex_energy=6456734424 ball_energy=5884957476 lex_edges=3693 boundary_min=2142 upper_rational=83855552164/11 upper_integer=7623232012 bitset_sha256=4f55e719c472514a6f2b2e657127780a0740471a7038205203f403f17988ba8a\n24994e94135e70f273ab4b05d05cbec8f025cc2dfad73df117d060e4b7ef3b0d\n",
    "inline_source": [
      "from fractions import Fraction",
      "from hashlib import sha256",
      "",
      "N_BITS=12",
      "N=1<<N_BITS",
      "M=794",
      "",
      "def popcount(x):",
      "    return bin(x).count('1')",
      "",
      "def energy(family):",
      "    return sum(3**(N_BITS-popcount(x^y)) for x in family for y in family)",
      "",
      "def fwht(values):",
      "    values=values[:]",
      "    width=1",
      "    while width<len(values):",
      "        for start in range(0,len(values),2*width):",
      "            for offset in range(width):",
      "                left=values[start+offset]",
      "                right=values[start+width+offset]",
      "                values[start+offset]=left+right",
      "                values[start+width+offset]=left-right",
      "        width*=2",
      "    return values",
      "",
      "def fourier_energy(family):",
      "    members=set(family)",
      "    walsh=fwht([int(x in members) for x in range(N)])",
      "    numerator=sum((4**N_BITS//2**popcount(s))*value*value for s,value in enumerate(walsh))",
      "    assert numerator%N==0",
      "    return numerator//N",
      "",
      "def internal_edges(family):",
      "    members=set(family)",
      "    return sum((x^(1<<i)) in members for x in members for i in range(N_BITS))//2",
      "",
      "lex=list(range(M))",
      "ball=[x for x in range(N) if popcount(x)<=4]",
      "assert len(lex)==len(ball)==M",
      "lex_energy=energy(lex)",
      "ball_energy=energy(ball)",
      "assert lex_energy==fourier_energy(lex)==6456734424",
      "assert ball_energy==fourier_energy(ball)==5884957476",
      "assert internal_edges(lex)==3693",
      "assert internal_edges(ball)==2784",
      "",
      "lex_bitset=(1<<M)-1",
      "bitset_digest=sha256(lex_bitset.to_bytes(512,'little')).hexdigest()",
      "assert bitset_digest=='4f55e719c472514a6f2b2e657127780a0740471a7038205203f403f17988ba8a'",
      "",
      "harper_edges=sum(popcount(x) for x in range(M))",
      "assert harper_edges==3693",
      "boundary_min=N_BITS*M-2*harper_edges",
      "mu=Fraction(M,N)",
      "nonconstant_mass=mu-mu*mu",
      "degree_moment_min=Fraction(boundary_min,2*N)",
      "secant_bound=mu*mu+((N_BITS*nonconstant_mass-degree_moment_min)/2+(degree_moment_min-nonconstant_mass)/2**N_BITS)/(N_BITS-1)",
      "upper_rational=8**N_BITS*secant_bound",
      "assert upper_rational==Fraction(83855552164,11)",
      "upper_integer=(upper_rational.numerator//upper_rational.denominator)//4*4",
      "assert upper_integer==7623232012",
      "",
      "report=f'lex_size={len(lex)} lex_energy={lex_energy} ball_energy={ball_energy} lex_edges={harper_edges} boundary_min={boundary_min} upper_rational={upper_rational} upper_integer={upper_integer} bitset_sha256={bitset_digest}'",
      "print(report)",
      "print(sha256((report+'\\n').encode()).hexdigest())"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1016/S0021-9800(66)80059-5",
    "locator": "Inline Python 3 verifier prepared on 2026-07-25"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R618",
      "title": "The maximum lies between 6,456,734,424 and 7,623,232,012",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "R620",
      "title": "The binary initial segment has objective 6,456,734,424",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "R619",
      "title": "The radius-four Hamming ball has objective 5,884,957,476",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "q12-noise-stability-794",
      "title": "q12 noise stability 794",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}