mg-l4yaml-source-check-20261010

SOURCE_CHECK

L4YAML parser acceptance — pinned source check

Presentation projection · authority NONE · not a certificate, proof, or verifier

Canonical identity: mg-l4yaml-source-check-20261010@1#mg-l4yaml-source-check-20261010
Type: SOURCE_CHECK
Source identity: mg-l4yaml-source-check-20261010
Source pointer: "" (document root)

Six independent status axes

historical_result: WARRANTED_BOUNDED
lifecycle: CURRENT
research_maturity: UNKNOWN
current_applicability: UNKNOWN
freshness: NOT_CHECKED_AFTER_SNAPSHOT
action_authorization: NONE

Source pins

mg-l4yaml-source-check-20261010 · version 1

Contract, locator and digests

{
  "id": "mg-l4yaml-source-check-20261010",
  "contract": "mathgraph.public-consequence-record.v1",
  "version": "1",
  "locator": "https://mathgraph.org/evidence/mg-l4yaml-source-check-20261010/record.json",
  "content_sha256": "f0d092974d5d710fe9e17fb6759a894f2c28f2d3f5456439c071bd0a71c8d3cb",
  "transport_sha256": "7b59ee76a39995f35a0feb0f4d91a3c6ab1234393143480c4f3e361a79fee703"
}

mathgraph.record-index.v2 · version 2

Contract, locator and digests

{
  "id": "mathgraph.record-index.v2",
  "contract": "mathgraph.record-index.v2",
  "version": "2",
  "locator": "https://mathgraph.org/records/index.json",
  "content_sha256": "0447486945b79a84c22c10b250cd71b3ccbb84abedddd2a2d2552e0f7d849c31"
}

Attribution: UNKNOWN
Evidence: { "automatic_api_warrant_promotion": false, "mathematical_theorem_badge_issued": false, "source_archive_hashes_replayed": true, "source_fidelity_certified": false, "status": "WARRANTED_ON_PINNED_BOUNDED_CASES" }
Scope: { "match": "EXACT", "source_commit": "62bf7077910e888a0bc8adfc8e08a5f500ff3ca3", "external_suite_commit": "da267a5c4782e7361e82889e76c0dc7df0e1e870", "supported_goals": [ "finite_parser_acceptance" ], "mismatch_status": "UNKNOWN" }
Verifier authority: LEAN_GUARDS_AND_COMPILED_TRYPARSE
ORIGINAL_JPL_LEAN_PROOF_OBJECTS
Assumptions: Pinned YAML-suite examples after specified source decoding
Named executable factorization and scoped anchor-event lemmas only
Replay boundary: 62bf7077910e888a0bc8adfc8e08a5f500ff3ca3
da267a5c4782e7361e82889e76c0dc7df0e1e870
leanprover/lean4:v4.34.0
Unknowns: whole_language_correctness
statement_fidelity
generalization
current_requalification
Unsupported semantics: whole_language_correctness
statement_fidelity
generalization
current_requalification

Every value above is a display of the source object and the listed supporting pins. Missing fields are UNKNOWN. The complete projected fields remain available below.

Incoming relations

No declared incoming relations in this displayed projection.

Outgoing relations

No declared outgoing relations in this displayed projection.

Lineage

Source mg-l4yaml-source-check-20261010 · version 1 · pointer "" (document root). This locator declares no chronology, supersession or equivalence.

All projected source fields

{
  "axes": {
    "current_requalification": {
      "status": "NOT_CHECKED_AFTER_SNAPSHOT"
    },
    "finite_executable": {
      "authority": "LEAN_GUARDS_AND_COMPILED_TRYPARSE",
      "case_scope": "Pinned YAML-suite examples after specified source decoding",
      "expected_accept": 31,
      "expected_reject": 17,
      "extra_controls": 4,
      "matched_external_labels": 48,
      "source_cases": 48,
      "status": "PINNED_CASES_CHECKED",
      "total_lean_guards": 52
    },
    "formal_verification": {
      "authority": "ORIGINAL_JPL_LEAN_PROOF_OBJECTS",
      "scope": "Named executable factorization and scoped anchor-event lemmas only",
      "status": "PINNED_SOURCE_THEOREMS_REPLAYED",
      "universal_yaml_correctness": "UNKNOWN"
    },
    "generalization": {
      "status": "UNKNOWN",
      "truth_promoting": false
    },
    "global_truth_promotion": false,
    "human_digestion": {
      "status": "UNKNOWN",
      "truth_promoting": false
    },
    "statement_fidelity": {
      "status": "UNKNOWN",
      "truth_promoting": false
    }
  },
  "admission": {
    "automatic_api_warrant_promotion": false,
    "mathematical_theorem_badge_issued": false,
    "source_archive_hashes_replayed": true,
    "source_fidelity_certified": false,
    "status": "WARRANTED_ON_PINNED_BOUNDED_CASES"
  },
  "source": {
    "branch_at_pin": "fix-a-grammar-completeness",
    "commit": "62bf7077910e888a0bc8adfc8e08a5f500ff3ca3",
    "external_suite_commit": "da267a5c4782e7361e82889e76c0dc7df0e1e870",
    "external_suite_repo": "yaml/yaml-test-suite",
    "lean_toolchain": "leanprover/lean4:v4.34.0",
    "repo": "nasa-jpl/L4YAML"
  },
  "scope": {
    "match": "EXACT",
    "source_commit": "62bf7077910e888a0bc8adfc8e08a5f500ff3ca3",
    "external_suite_commit": "da267a5c4782e7361e82889e76c0dc7df0e1e870",
    "supported_goals": [
      "finite_parser_acceptance"
    ],
    "mismatch_status": "UNKNOWN"
  }
}

Permanent object view · Source / export JSON · Reproduction instructions and boundaries