{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R376",
  "content_hash": null,
  "slug": "heilbronn10-claim-symmetric-family-exact",
  "type": "claim",
  "title": "The Comellas–Yebra three-parameter family has exact maximum 0.0465374195825...",
  "summary": "Within the ordered boundary family with parameters 0 ≤ x ≤ y ≤ z ≤ 1/2, exact algebra gives maximum minimum triangle area A = 5z₀²/8 - z₀³/2, where 12z₀³ - 27z₀² + 20z₀ - 4 = 0. The unrestricted ten-point upper bound remains open.",
  "relevance": "For Exact ten-point Heilbronn number in the unit square, record heilbronn10-claim-symmetric-family-exact (“The Comellas–Yebra three-parameter family has exact maximum 0.0465374195825...”) records a bound, answer, status fact, or structural consequence. The record states: Within the ordered boundary family with parameters 0 ≤ x ≤ y ≤ z ≤ 1/2, exact algebra gives maximum minimum triangle area A = 5z₀²/8 - z₀³/2, where 12z₀³ - 27z₀² + 20z₀ - 4 = 0.",
  "relevance_source": "recorded",
  "body": "Consider the ten points\n\n\\[(x,0),(1-y,0),(0,x),(1,y),(1-z,z),(z,1-z),(0,1-y),(1,1-x),(y,1),(1-x,1)\\]\n\nwith \\(0\\le x\\le y\\le z\\le 1/2\\). This ansatz has diagonal-reflection and half-turn symmetry. It is a proper subclass of all ten-point configurations.\n\nThree doubled triangle areas are\n\n\\[P=x(1-x-y),\\qquad Q=y(1-2z),\\qquad R=z(1-x+y)-y.\\]\n\nThey come from triples 012, 145, and 058. The ordering makes all three nonnegative. Let \\(t=\\min(P,Q,R)\\), let \\(z_0\\) be the unique real root of \\(f(z)=12z^3-27z^2+20z-4\\), and set \\(t_0=(5z_0^2-4z_0^3)/4=2A\\).\n\nAssume \\(t\\ge t_0\\). Then \\(d=1-2z>0\\), and \\(Q\\ge t\\) gives \\(L=t/d\\le y\\). Substituting \\(L\\) for \\(y\\) can only increase \\(P\\) and \\(R\\). The inequality \\(R(x,L,z)\\ge t\\) gives\n\n\\[x\\le U=1-\\frac{t+(1-z)L}{z}.\\]\n\nThe vertex of \\(P(x,L)=x(1-x-L)\\) is \\((1-L)/2\\), and\n\n\\[\\frac{1-L}{2}-U=\\frac{N}{2z(1-2z)},\\qquad N=t(4-7z)+2z^2-z.\\]\n\nSince \\(4-7z>0\\), it is enough to check \\(t=t_0\\). The resulting quadratic in \\(z\\) has discriminant \\(49t_0^2-18t_0+1<0\\), using the exact brackets \\(31/100<z_0<8/25\\) and \\(9/100<t_0<1/10\\). Thus \\(U\\) lies at or before the vertex. From \\(P(x,L)\\ge t\\) and \\(x\\le U\\), we obtain \\(P(U,L)\\ge t\\). Direct simplification gives\n\n\\[P(U,L)-t=\\frac{tH}{z^2(1-2z)},\\qquad H=(6z-4)t+2z^3-5z^2+2z.\\]\n\nTherefore\n\n\\[t\\le h(z)=\\frac{2z^3-5z^2+2z}{4-6z}.\\]\n\nFinally, \\(h'(z)=-f(z)/(2(3z-2)^2)\\). The cubic has one real root, so \\(h\\) reaches its unique maximum on \\([0,1/2]\\) at \\(z_0\\), and \\(h(z_0)=t_0\\). Hence every configuration in this family has a triangle of area at most \\(A\\). The parameters \\(x=z_0/2\\) and \\(y=(1-z_0)(1-2z_0)\\) attain \\(A\\), proving the family result.",
  "status": "proposed",
  "evidence_grade": "self_reported",
  "scope": {
    "kind": "family",
    "statement": "all ordered parameters 0 <= x <= y <= z <= 1/2 in the listed ten-point affine boundary ansatz",
    "family": "Comellas-Yebra diagonal-reflection and half-turn symmetric three-parameter boundary family"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "locator": "Self-contained derivation recorded 2026-07-28; symbolic identities and root-sign checks replay in heilbronn10-artifact-exact-certificate"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Self-contained derivation recorded 2026-07-28; symbolic identities and root-sign checks replay in heilbronn10-artifact-exact-certificate"
  },
  "relations": [
    {
      "slug": "R369",
      "title": "Exact 120-triangle certificate and symbolic family checks",
      "object_type": "artifact",
      "relation": "tests",
      "direction": "incoming"
    },
    {
      "slug": "R374",
      "title": "The exact Comellas–Yebra construction has minimum area 0.0465374195825...",
      "object_type": "claim",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R373",
      "title": "Run the unrestricted Sudermann-Merx global model at n = 10",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "outgoing"
    },
    {
      "slug": "R370",
      "title": "Exact rational interval cover for the symmetric family",
      "object_type": "artifact",
      "relation": "tests",
      "direction": "incoming"
    },
    {
      "slug": "R372",
      "title": "Cover the symmetric family by exact determinant intervals",
      "object_type": "attempt",
      "relation": "tests",
      "direction": "incoming"
    },
    {
      "slug": "heilbronn-square-ten",
      "title": "heilbronn square ten",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}