Which selected proof branch reaches normalization?

L2 · 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 target proofs with a directed path to the indicated interface in this supplied compiled-body slice. Does such a path prove mathematical necessity? A missing path here is not a full-closure independence certificate.

Targets: Strict transport join, Joint-law L2 triangle

Queried interface: Joint probability mass

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.

Related exercises about selected statements: Recovering joint probability mass from one marginal.

Independent structural review and limits

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

No selected path from l2_edge_triangle is not absence in the full proof/declaration closure. Conversely the positive gluing path does not make this normalization theorem mathematically indispensable.
Only selected body constants and direct unexpanded type-whitelist occurrences were inspected; private intermediates, unselected constants, definition-expanded profiles and binder-role/necessary-hypothesis classification are outside the evidence.

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-g005",
  "core_id": "sogb-018",
  "family": "coupling-gluing-triangle",
  "title": "Which selected proof branch reaches normalization?",
  "library_domains": [
    "statistical-optimal-transport",
    "log-concave-sampling"
  ],
  "track": "graph-json",
  "level": "L2",
  "split": "public-dev",
  "skills": [
    "graph-reading",
    "semantic-boundary"
  ],
  "targets": [
    "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangle.wassersteinDistance_lt_add_of_lt",
    "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2_edge_triangle"
  ],
  "question": "List the target proofs with a directed path to the indicated interface in this supplied compiled-body slice. Does such a path prove mathematical necessity? A missing path here is not a full-closure independence certificate.",
  "context": {
    "direction": "theorem-to-selected-constant-in-compiled-proof-body",
    "edges": [
      [
        "AutoSamplingTheory.TechnicalLemmas.Measure.TransportGluing.exists_gluing_of_isCoupling",
        "AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isProbabilityMeasure_of_isCoupling_left"
      ],
      [
        "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangle.wassersteinDistance_lt_add_of_lt",
        "AutoSamplingTheory.TechnicalLemmas.Measure.TransportGluing.exists_gluing_of_isCoupling"
      ],
      [
        "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangle.wassersteinDistance_lt_add_of_lt",
        "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2_edge_triangle"
      ],
      [
        "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2_edge_triangle",
        "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2Seminorm_add_le"
      ],
      [
        "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2_edge_triangle",
        "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2Seminorm_mono"
      ]
    ],
    "kind": "compiled-proof-body-constant-occurrences",
    "node_labels": {
      "AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isProbabilityMeasure_of_isCoupling_left": "Joint probability mass",
      "AutoSamplingTheory.TechnicalLemmas.Measure.TransportGluing.exists_gluing_of_isCoupling": "Shared-middle gluing",
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangle.wassersteinDistance_lt_add_of_lt": "Strict transport join",
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2Seminorm_add_le": "L2 Minkowski",
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2Seminorm_mono": "L2 monotonicity",
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2_edge_triangle": "Joint-law L2 triangle"
    },
    "nodes": [
      "AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isProbabilityMeasure_of_isCoupling_left",
      "AutoSamplingTheory.TechnicalLemmas.Measure.TransportGluing.exists_gluing_of_isCoupling",
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangle.wassersteinDistance_lt_add_of_lt",
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2Seminorm_add_le",
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2Seminorm_mono",
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2_edge_triangle"
    ],
    "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.Transport.isProbabilityMeasure_of_isCoupling_left": [],
      "AutoSamplingTheory.TechnicalLemmas.Measure.TransportGluing.exists_gluing_of_isCoupling": [],
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangle.wassersteinDistance_lt_add_of_lt": [],
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2Seminorm_add_le": [],
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2Seminorm_mono": [],
      "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore.l2_edge_triangle": []
    },
    "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": "88ba32cab62a4cd1d4e3a607af6509ebc35678b5d0fdfb2158fc2e2e812231ad",
  "answer_schema": {
    "nodes": "list of distinct declaration ids; order ignored by scorer",
    "entails_mathematical_necessity": "boolean; whether this evidence certifies mathematical necessity"
  },
  "remove": "AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isProbabilityMeasure_of_isCoupling_left",
  "binding_sha256": "cfc51fa334e6652839cffd5e4a30f69e0319ed02bc92c64daf8d8ff54eff065f"
}

Reference structural answer · 2 checks, 1 point

{
  "nodes": [
    "AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangle.wassersteinDistance_lt_add_of_lt"
  ],
  "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.