MathGraph Discover — Source-grounded frontiers

Source-grounded frontier · exact Mathlib revision

Follow a real gap in the published source slice.

ADVISORY INCOMPLETE

Terminal form NONE. This is not a proof, countermodel, or named obstruction. It is one deterministic advisory view derived at build time from the exact public catalogue.

Source status SOURCE_INDEXED · Independent verification NOT_CHECKED · Current applicability NOT_CHECKED · Authority NONE · Authorization NONE

`Real.log_rpow` → omitted `Real.log`

The indexed statement for Real.log_rpow names Real.log, but that target occurrence is outside this selected catalogue. The same named omission appears for 42 distinct indexed declarations in this exact module shard.

The omission records a direct expression-constant reference whose target is outside the selected slice. It does not create a TYPE_REFERENCES relation, logical implication, semantic equivalence, or verification result.

Exact source occurrence: Mathlib/Analysis/SpecialFunctions/Pow/Real.lean:491–496 ↗
cbb5d6bc3ea24d4f3231fdcb221756eba154e15179f5529d3dc2ecad41dc6d88
Catalogue manifest: Open immutable manifest
5974ac4d68b1e090d511964cd61237565b80d39b5e47e9966171d4d8bcd2fe68
Module shard: Open content-addressed shard
6400eba377e910ff2ac4bea415657e6c84b546832d93808c9fcb9dce952d22c0

Next gate 1 — catalogue expansion

Status: NOT_RUN. Locate and index the exact Real.log source occurrence at the same pinned Mathlib revision, publish a new versioned catalogue projection preserving foundations-v1, and pass its independent offline consumer. This establishes source structure only.

A successful gate can return only SOURCE_INDEXED; it does not check a proof.

Later gate 2 — Lean proof qualification

Status: NOT_RUN. Separately replay Lean under the declared source and toolchain boundary and publish a qualified receipt before assigning a VERIFIED_PROOF terminal form. Catalogue expansion alone cannot establish proof validity.

Required result boundary: SEPARATE_EVIDENCE_RECEIPT_REQUIRED.

Recursive residual transfer · 2026-05-23 source pack

A historical advisory result with missing material.

PARTIAL

Verification status: NOT_CHECKED. The adapter checked available source bytes and produced the committed ranking. The historical experiment was not rerun or requalified.

advisory_only: true
can_promote_truth: false

Rank 1: `recursive_transfer_replay_candidate`

frozen evidence replay and route-memory comparison

Proposed target: replay_validation. Selected: true.

Attention allocation: 1. Heuristic score: 2.9801666674.

ALLOCATION_NOT_TRUTH_CONFIDENCE: attention is allocation, not truth confidence. A probability of 1 means all allocated attention goes to this one eligible candidate; it supplies no proof or truth score.

Reported historical metrics

Reported historical metrics are source observations, not new verification results. Zero reported contamination and passed historical gates do not promote a claim.

compact_transfer_gain_vs_generic_positive: 234.166667 · source metrics
compact_retains_recursive_gain: 0.989575 · source metrics
compact_prunes_recursive_memory: 0.53 · source metrics
generic_mean_recoveries: 11405.5 · source metrics
true_contamination_max: 0 · source metrics
all_gates_pass: true · source metrics
advisory_boundary_ok: true · source metrics

Full replay remains unavailable.

The full candidate-score CSV and SQLite ledger are missing locally. The ledger is required for full replay; original equations, matrix, and toolchain qualification are not supplied by this adapter.

Result reason: SOURCE_MATERIAL_INCOMPLETE

Exact source diagnostics

HISTORICAL_RESULTS_ADVISORY: experiment not rerun or authenticated; local hashes establish byte identity only.
MISSING_LOCAL_ARTIFACT: candidate_generation_scores_full
MISSING_LOCAL_ARTIFACT: sqlite_ledger
FULL_REPLAY_UNAVAILABLE: sqlite_ledger
MISSING_EXPECTED_ARTIFACT: codex_manifest.json
MISSING_EXPECTED_ARTIFACT: discovery_summary.json
MISSING_EXPECTED_ARTIFACT: loose README.md
MISSING_EXPECTED_ARTIFACT: compact_atlas_eval.csv
MISSING_EXPECTED_ARTIFACT: repo_vs_original_comparison.json
MISSING_EXPECTED_ARTIFACT: repo_vs_original_comparison.md
MISSING_EXPECTED_ARTIFACT: frozen_evidence_comparison.json
FULL_REPLAY_NOT_PERFORMED: original equations, matrix, toolchain and replay inputs are not qualified by this adapter.

Inspect the source identities.

Digests establish byte identity relative to a trusted pin, not publisher authenticity. Missing artifacts retain their source references and NOT_CHECKED state.

All 13 source references and digests

manifest: PRESENT · integrity MATCHED · 13149 bytes
449e9f9378a90ffb975f21cd5d534455f0d03bc393bf821daefdc000950509c5
Required for full replay: false
metrics: PRESENT · integrity MATCHED · 1483 bytes
83c9a568d2fc3f9c06bd4487c51a7a6af1ba44323a33e6b3e3b86e23d1bf0b2c
Required for full replay: false
source_summary: PRESENT · integrity MATCHED · 643 bytes
7c554b771261651a43b3b4dacd51e20bb63e6124c8130fe1f45f13453b48ac1a
Required for full replay: false
gate_results: PRESENT · integrity MATCHED · 530 bytes
195f17d394125df425b3cd8481d3121886534474996ea5943f83bbbb6fa78869
Required for full replay: false
route_summary: PRESENT · integrity MATCHED · 2508 bytes
b9c6b402297194dfa687361d8bb5171a311f291b77e0f56c59fe5bba693fab4e
Required for full replay: false
compact_atlas_selection: PRESENT · integrity MATCHED · 1585 bytes
3530b5667324d22154fdec43068c7104e8492ded5603f5d5bf66f37921750f5a
Required for full replay: false
generation_summary: PRESENT · integrity MATCHED · 2568 bytes
1c9630ada5634816005a95fedeeae4670e0c8a5a926770cf3a6c0233902bc65f
Required for full replay: false
constructor_manifest: PRESENT · integrity MATCHED · 20510 bytes
ba44a9ee9fad30069f193d81385f01a2d86b8d36e4568a32d3a2ccd15b68ea00
Required for full replay: false
constructor_attribution: PRESENT · integrity MATCHED · 30306 bytes
2cc344ddc9f33b9dc4ac69c830fd765fa59018c673d5a8a51fd85660ede93cc3
Required for full replay: false
route_eval_by_seed_split: PRESENT · integrity MATCHED · 18335 bytes
6f7e13a39b476c7a77c5df4a779e3c9c785ca937882955f633e84621d4e10918
Required for full replay: false
report: PRESENT · integrity MATCHED · 12200 bytes
05871b1154731a06b517eac618b6b43d24c564035ff56fd2ee39c08f789b7a56
Required for full replay: false
candidate_generation_scores_full: MISSING · integrity NOT_CHECKED · 349468 bytes
d89604377b4d7f2c939ae4e205c72dacb51c72b92bb3b5541458711ee3e63f0d
Required for full replay: false
sqlite_ledger: MISSING · integrity NOT_CHECKED · 458752 bytes
4f8e9ec5d88e80ccafa22efdf970c102fd29d18145a3d33abc62a45d68a264dd
Required for full replay: true

Exact request JSON ↗SHA-256 23d6d59eef4fd6ba7bdddd673d01b8f2e61e71412b1d7bc66d3fce68b728c25a Exact result JSON ↗SHA-256 6d9a24c7ffebe2288561e976a774f9d184f47b21e40572046e003b917cc939a5

Committed result and source revision ↗

Run locally with explicit inputs.

Hosted service: NOT_DEPLOYED. This page is a static projection. The CLI performs no solver call, route execution, or semantic verification.

From a repository checkout · Python standard library

python3 -I -S scripts/mathgraph_discover_v1.py --request conformance/discover_v1/fixtures/request.json

Request schema · Result schema · Full contract

Modules can be used separately. Develop and Capabilities expose different contracts; no autonomous loop or compulsory runtime sequence is provided.