A genuinely shared proof ingredient

L1 · public-dev · structural QA, not a theorem proof

Read the source mathematical proof and optional Lean. This is context linkage, not an equivalent mathematical question.

List the selected theorem constants occurring directly in every listed target proof body in this supplied induced slice. Are these necessarily indispensable mathematical premises?

Targets: Pair (1,2) cost, Pair (2,3) cost

Scroll horizontally on a small screen. Solid arrows: selected theorem constants occur in the compiled proof bodies, including proof-term annotations. Other constants and private auxiliaries are omitted; a missing path is not full-closure independence. Neutral colours make no proof-status claim.

Independent structural review and limits

Current editorial status: accepted. This is AI review of structural QA, not a theorem or calibrated difficulty.

Edges are selected constant occurrences in compiled proof bodies, including annotations, not minimal or indispensable premises. Other public constants, private auxiliaries and Mathlib parents are omitted.
Empty whitelist profiles say only that these five exact constants do not occur directly in the unexpanded elaborated statements; they are neither a binder-role analysis nor an absence/necessity claim after unfolding. Fresh compiler agreement is not mathematical necessity.

Exact review bindings and report hashes · Current independent review and explicit historical supersession

Evidence kind and source scope

This is a recorded source-bound compiler snapshot. CI separately replays the trusted extractor. It is not a fresh Lean run in this browser, a full proof closure or a minimal-premise certificate. Unique proof constants do not count runtime invocations, recursive calls or oracle queries.

Recorded compiler slice and provenance

An edge records constant occurrence in this compiled proof body, including proof-term annotations. Statement profiles record only whitelisted direct type-constant occurrences, not logical requirements. Neither certifies mathematical necessity or a full dependency closure. No path in an induced slice does not imply no path in the full closure.

Exact JSON snapshot and response schema

{
  "id": "sogb-g004",
  "core_id": "sogb-018",
  "family": "coupling-gluing-triangle",
  "title": "A genuinely shared proof ingredient",
  "library_domains": [
    "statistical-optimal-transport",
    "log-concave-sampling"
  ],
  "track": "graph-json",
  "level": "L1",
  "split": "public-dev",
  "skills": [
    "graph-reading",
    "semantic-boundary"
  ],
  "targets": [
    "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.l2Seminorm_edge12_eq_pairCost",
    "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.l2Seminorm_edge23_eq_pairCost"
  ],
  "question": "List the selected theorem constants occurring directly in every listed target proof body in this supplied induced slice. Are these necessarily indispensable mathematical premises?",
  "context": {
    "direction": "theorem-to-selected-constant-in-compiled-proof-body",
    "edges": [
      [
        "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.l2Seminorm_edge12_eq_pairCost",
        "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.measurable_quadraticCost"
      ],
      [
        "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.l2Seminorm_edge23_eq_pairCost",
        "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.measurable_quadraticCost"
      ]
    ],
    "kind": "compiled-proof-body-constant-occurrences",
    "node_labels": {
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.l2Seminorm_edge12_eq_pairCost": "Pair (1,2) cost",
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.l2Seminorm_edge23_eq_pairCost": "Pair (2,3) cost",
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.measurable_quadraticCost": "Cost measurability"
    },
    "nodes": [
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.l2Seminorm_edge12_eq_pairCost",
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.l2Seminorm_edge23_eq_pairCost",
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.measurable_quadraticCost"
    ],
    "scope": "induced public-theorem slice; unselected constants, private auxiliaries and Mathlib parents are omitted",
    "source_sha256_lf": {
      "AutoSamplingTheory/TechnicalLemmas/Measure/Transport.lean": "d3eff4916a04ab9473ee86b839fa13b8447fa1c4d162874a4ceddbce4003e414",
      "AutoSamplingTheory/TechnicalLemmas/Measure/TransportGluing.lean": "df336ce4f6047441b52d075272f31b6e7d3f56e6bbeb1c8c9eb6a6e54e3cc062",
      "AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinSpace.lean": "943f06c49f3e8e182ab731f9c8e4e5372b65b2eae81001c781a2f6bbc69998b5",
      "AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinTriangle.lean": "70734431850472a3a175858173dfbff49e469fb23384a5e927bbd718456193e0",
      "AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinTriangleCore.lean": "182ab3f1827a46647810263ece9f118e0bc2f84f26c66873b463a90e62a33084",
      "AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinTriangleMarginals.lean": "b899bd0ea5739e82e453a8e0300f701db85ec623cd12f09ef864e69bdb2e905b"
    },
    "statement_constant_whitelist": [
      "CompleteSpace",
      "Differentiable",
      "HasDerivAt",
      "HasDerivWithinAt",
      "HasGradientAt"
    ],
    "statement_profile_scope": "Direct constant occurrences in the unexpanded elaborated statement; not a binder-role analysis, inferred hypothesis list or full type dependency closure.",
    "statement_profiles": {
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.l2Seminorm_edge12_eq_pairCost": [],
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.l2Seminorm_edge23_eq_pairCost": [],
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.measurable_quadraticCost": []
    },
    "truth_boundary": "An edge records constant occurrence in this compiled proof body, including proof-term annotations. Statement profiles record only whitelisted direct type-constant occurrences, not logical requirements. Neither certifies mathematical necessity or a full dependency closure. No path in an induced slice does not imply no path in the full closure.",
    "snapshot_sha256": "5acc8ce2fd312ac2bff83b8a593893fa4e29177f1f07d4686967705113ca9004",
    "provenance": {
      "context_sha256": "52014c740e6c7ba03a84e97de3eb322233e19220d92074ad394f989c62e9cd6d",
      "core_binding_sha256": "237b6a126e4672415b58ea7f7621fe69ef5d541dac41fb1b42336f828922a1e2",
      "core_id": "sogb-018",
      "generator_sha256_lf": "2f570810651543df28853b31847a0ba5b676675231febca78269a67cb13a9229",
      "lakefile_sha256_lf": "1757b85b37f0a68972791443e3a8da33fd97ede414732fabb8e7d747b070c51c",
      "local_import_closure_sha256_lf": {
        "AutoSamplingTheory/TechnicalLemmas/Measure/Transport.lean": "d3eff4916a04ab9473ee86b839fa13b8447fa1c4d162874a4ceddbce4003e414",
        "AutoSamplingTheory/TechnicalLemmas/Measure/TransportGluing.lean": "df336ce4f6047441b52d075272f31b6e7d3f56e6bbeb1c8c9eb6a6e54e3cc062",
        "AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinSpace.lean": "943f06c49f3e8e182ab731f9c8e4e5372b65b2eae81001c781a2f6bbc69998b5",
        "AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinTriangle.lean": "70734431850472a3a175858173dfbff49e469fb23384a5e927bbd718456193e0",
        "AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinTriangleCore.lean": "182ab3f1827a46647810263ece9f118e0bc2f84f26c66873b463a90e62a33084",
        "AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinTriangleMarginals.lean": "b899bd0ea5739e82e453a8e0300f701db85ec623cd12f09ef864e69bdb2e905b"
      },
      "mathlib_manifest_sha256_lf": "b83ca83b9cf7caa85fa8b023c2ff9a3fb7a7cce7e1c332e810c348535ec49c37",
      "selection_sha256": "be6d4d3982a77f7a479a358458cda8004ef7b42669ce7506fafe00ff14f7d659",
      "source_sha256_lf": {
        "AutoSamplingTheory/TechnicalLemmas/Measure/Transport.lean": "d3eff4916a04ab9473ee86b839fa13b8447fa1c4d162874a4ceddbce4003e414",
        "AutoSamplingTheory/TechnicalLemmas/Measure/TransportGluing.lean": "df336ce4f6047441b52d075272f31b6e7d3f56e6bbeb1c8c9eb6a6e54e3cc062",
        "AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinSpace.lean": "943f06c49f3e8e182ab731f9c8e4e5372b65b2eae81001c781a2f6bbc69998b5",
        "AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinTriangle.lean": "70734431850472a3a175858173dfbff49e469fb23384a5e927bbd718456193e0",
        "AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinTriangleCore.lean": "182ab3f1827a46647810263ece9f118e0bc2f84f26c66873b463a90e62a33084",
        "AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinTriangleMarginals.lean": "b899bd0ea5739e82e453a8e0300f701db85ec623cd12f09ef864e69bdb2e905b"
      },
      "toolchain": "leanprover/lean4:v4.33.0"
    }
  },
  "graph_sha256": "5c5fc8dc93c4cf0d3f4b4d5501ea8198b1b0c157f8f905ccfc52dd26575da9db",
  "answer_schema": {
    "nodes": "list of distinct declaration ids; order ignored by scorer",
    "entails_mathematical_necessity": "boolean; whether this evidence certifies mathematical necessity"
  },
  "binding_sha256": "ac008b7c0850ba630b626f60fd16d7bf252a4985face61a9a9fc34e52a418db4"
}

Reference structural answer · 2 checks, 1 point

{
  "nodes": [
    "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals.measurable_quadraticCost"
  ],
  "entails_mathematical_necessity": false
}

One point requires both the exact structural node set and a false mathematical-necessity certification. The constant boundary answer earns no standalone credit. Edges have only the stated evidence kind. Neither a positive path nor an absent induced path proves mathematical necessity or full-closure independence.

No model score, theorem-equivalence certificate or calibrated difficulty is asserted.