{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R617",
  "content_hash": null,
  "slug": "q12ns794-attempt-literature-and-exact-optimization-audit",
  "type": "attempt",
  "title": "Classical inequalities give a certified gap; the exact weighted optimum was not located",
  "summary": "Harper settles the edge term, while average-distance and Boolean Fourier sources do not report this exact all-distance objective at size 794.",
  "relevance": "For Maximum half-noise stability of a 794-set in the twelve cube, record q12ns794-attempt-literature-and-exact-optimization-audit (“Classical inequalities give a certified gap; the exact weighted optimum was not located”) documents a concrete method, search boundary, or failed route. The record states: Harper settles the edge term, while average-distance and Boolean Fourier sources do not report this exact all-distance objective at size 794.",
  "relevance_source": "recorded",
  "body": "Harper's 1966 paper proves the binary-cube edge-isoperimetric theorem used here. Bonami's 1970 work and Beckner's 1975 paper provide the classical analytic setting for Fourier and noise inequalities on product spaces. Kündgen's 2002 paper studies minimum average Hamming distance, which is equivalent to maximizing the level-one Walsh weight. It records the broader Ahlswede-Katona problem and shows why controlling only a distance moment is a separate extremal question.\n\nThe audit searched these lines of work and exact finite noise-stability optimization. No located primary source states the maximum of \\(\\sum_{x,y\\in A}3^{12-d_H(x,y)}\\) for \\(|A|=794\\), and no source classifies its maximizers. This records the search outcome and makes no novelty claim.\n\nA complete continuation can encode \\(1_A\\) as 4,096 binary variables with the exact cardinality equation and optimize the positive quadratic form \\(x^TKx\\), where \\(K_{uv}=3^{12-d_H(u,v)}\\). A branch-and-bound result becomes a proof when every node carries a rational dual upper bound whose maximum is at most the incumbent, with the complete node log and solver-checkable dual data preserved. A symmetry-aware alternative uses the cardinality ideal \\(\\sum x_u=794\\), the Boolean equations \\(x_u^2=x_u\\), and cube-invariant semidefinite moment constraints. A rational sum-of-squares dual matching 6,456,734,424 would prove optimality. Once equality is certified, canonical labeling under the group \\(C_2^{12}\\rtimes S_{12}\\) can enumerate the maximizing orbits.",
  "status": "inconclusive",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "bounded",
    "statement": "a targeted literature audit for Boolean-cube edge isoperimetry, minimum average distance, Fourier noise stability, and the exact 12-cube cardinality-794 weighted optimization, completed on 2026-07-25",
    "bounds": {
      "dimension": {
        "min": 12,
        "max": 12
      },
      "cardinality": {
        "min": 794,
        "max": 794
      },
      "noise_correlation_numerator": {
        "min": 1,
        "max": 1
      },
      "noise_correlation_denominator": {
        "min": 2,
        "max": 2
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "url": "https://doi.org/10.1016/S0012-365X(01)00242-4",
      "locator": "Harper, J. Combinatorial Theory 1 (1966), 385-393, DOI 10.1016/S0021-9800(66)80059-5; Bonami, Ann. Inst. Fourier 20 (1970), 335-402, https://www.numdam.org/item/AIF_1970__20_2_335_0/; Beckner, Ann. Math. 102 (1975), 159-182, DOI 10.2307/1970980; Kündgen, Discrete Math. 249 (2002), 149-165, DOI 10.1016/S0012-365X(01)00242-4"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1016/S0012-365X(01)00242-4",
    "locator": "Harper, J. Combinatorial Theory 1 (1966), 385-393, DOI 10.1016/S0021-9800(66)80059-5; Bonami, Ann. Inst. Fourier 20 (1970), 335-402, https://www.numdam.org/item/AIF_1970__20_2_335_0/; Beckner, Ann. Math. 102 (1975), 159-182, DOI 10.2307/1970980; Kündgen, Discrete Math. 249 (2002), 149-165, DOI 10.1016/S0012-365X(01)00242-4"
  },
  "models": [],
  "relations": [
    {
      "slug": "R618",
      "title": "The maximum lies between 6,456,734,424 and 7,623,232,012",
      "object_type": "claim",
      "relation": "informs",
      "direction": "outgoing"
    },
    {
      "slug": "q12-noise-stability-794",
      "title": "q12 noise stability 794",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}