TheoremDB

Problem packetResearch packetR505

R505Sourced evidence

The SDP upper bound is 388, with an integer-only fallback of 394

View evidenceOpen source ↗
Link to a section

Authored summary

Heinlein and Ihringer prove A₂(7,4) ≤ 388 using semidefinite programming. Their separate integer-only computation gives an error-resilient fallback bound of 394.

The record cites sources for its explanation.

Recorded status: reported

Recorded scope: upper bounds for binary mixed-dimension subspace codes in ambient dimension 7 with minimum distance 4

Complete recorded scope and conditions
{
  "kind": "bounded",
  "statement": "upper bounds for binary mixed-dimension subspace codes in ambient dimension 7 with minimum distance 4",
  "bounds": {
    "field_order": {
      "min": 2,
      "max": 2
    },
    "ambient_dimension": {
      "min": 7,
      "max": 7
    },
    "minimum_subspace_distance": {
      "min": 4,
      "max": 4
    }
  },
  "exhaustive": false
}

Originating problem: Exact mixed-dimension subspace-code number A_2(7,4)

Recorded relationships: The dated interval is 334 ≤ A₂(7,4) ≤ 388

Authored record and scope
Authored title
The SDP upper bound is 388, with an integer-only fallback of 394
Record type
claim
Stored status
reported
Evidence grade
sourced
Recorded scope data
{ "kind": "bounded", "statement": "upper bounds for binary mixed-dimension subspace codes in ambient dimension 7 with minimum distance 4", "bounds": { "field_order": { "min": 2, "max": 2 }, "ambient_dimension": { "min": 7, "max": 7 }, "minimum_subspace_distance": { "min": 4, "max": 4 } }, "exhaustive": false }
Linked research record IDs
R502

2Authored explanation

Theorem 1.1 states the binary upper bound 388. Lemma 4.1 restricts the possible dimension distributions for code sizes 384 through 388. The paper later reports an exhaustive integer computation with objective value 393 and applies Corollary 4.6 to obtain A₂(7,4) ≤ 394. The integer route is weaker, while supplying a separate bound that does not depend on floating-point SDP output.

Continue this work
Replay material: source only

3Evidence

Replay package: source only

A verification source is cited. This record has no executable replay attached.

Verification source: arxiv.org ↗, Heinlein and Ihringer, arXiv:1809.09352v2, Theorems 1.1 and 1.2 on PDF pp. 2-3, Lemma 4.1 on p. 12, and the integer-computation paragraph immediately before Section 5 on p. 17

4What was measured

5How it connects

Recorded for

Machine-readable record

Copy the structured record when continuing this work with an agent.

json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R505",
  "content_hash": null,
  "slug": "mdsc-claim-sdp-upper-bound-and-integer-fallback",
  "type": "claim",
  "title": "The SDP upper bound is 388, with an integer-only fallback of 394",
  "summary": "Heinlein and Ihringer prove A₂(7,4) ≤ 388 using semidefinite programming. Their separate integer-only computation gives an error-resilient fallback bound of 394.",
  "relevance": "For Exact mixed-dimension subspace-code number A_2(7,4), record mdsc-claim-sdp-upper-bound-and-integer-fallback (“The SDP upper bound is 388, with an integer-only fallback of 394”) records a bound, answer, status fact, or structural consequence. The record states: Heinlein and Ihringer prove A₂(7,4) ≤ 388 using semidefinite programming.",
  "relevance_source": "recorded",
  "body": "Theorem 1.1 states the binary upper bound 388. Lemma 4.1 restricts the possible dimension distributions for code sizes 384 through 388. The paper later reports an exhaustive integer computation with objective value 393 and applies Corollary 4.6 to obtain A₂(7,4) ≤ 394. The integer route is weaker, while supplying a separate bound that does not depend on floating-point SDP output.",
  "status": "reported",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "bounded",
    "statement": "upper bounds for binary mixed-dimension subspace codes in ambient dimension 7 with minimum distance 4",
    "bounds": {
      "field_order": {
        "min": 2,
        "max": 2
      },
      "ambient_dimension": {
        "min": 7,
        "max": 7
      },
      "minimum_subspace_distance": {
        "min": 4,
        "max": 4
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://arxiv.org/abs/1809.09352",
      "locator": "Heinlein and Ihringer, arXiv:1809.09352v2, Theorems 1.1 and 1.2 on PDF pp. 2-3, Lemma 4.1 on p. 12, and the integer-computation paragraph immediately before Section 5 on p. 17"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/1809.09352",
    "locator": "Heinlein and Ihringer, arXiv:1809.09352v2, Theorems 1.1 and 1.2 on PDF pp. 2-3, Lemma 4.1 on p. 12, and the integer-computation paragraph immediately before Section 5 on p. 17"
  },
  "models": [],
  "relations": [
    {
      "slug": "R501",
      "title": "Audit the primary sources, current bounds table, and production record",
      "object_type": "attempt",
      "relation": "reports",
      "direction": "incoming"
    },
    {
      "slug": "R502",
      "title": "The dated interval is 334 ≤ A₂(7,4) ≤ 388",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "mixed-dimension-subspace-code-f2-7-d4",
      "title": "mixed dimension subspace code f2 7 d4",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

7Provenance

View source, identifiers, and projection details

A statement this project treats as settled at the recorded evidence grade, with the work that backs it.

Sign in to follow

Sign in in another tab, then return here.

Open sign-in in another tab

Report a problem

Report location:

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.