research: seal patched Lean replay-free identity screen and revalidation-cost control

[fraware]

Objective

Implement a replay-free applicability screen under patched Lean 4.35.0, independently of the historical-certificate reference oracle established in draft #209. The screen's strongest output is CONDITIONAL_IDENTITY_CANDIDATE; it cannot issue VALID or production reliance.

Research changes

• New lean_patched_preoracle_identity_v1.py validates the historical source proof AST against its native source observation, source-file bytes and a separate --trust=0 source recheck. It validates the independently observed unproved target claim against the exact historical statement AST and source payload, binds the source/target imported RTKPatchedSupport.olean bytes to the same pinned patched executable digest, and rejects missing/forged authority or inconsistent native definition ASTs.
• If imported-module bytes match and observed op definition ASTs agree, emit CONDITIONAL_IDENTITY_CANDIDATE. If imported-module bytes differ, emit REVALIDATION_REQUIRED regardless of whether the relevant observed declaration changed. No target replay log, target proof, target oracle verdict, or external success label is an input.
• The native workflow now reconstructs four unproved target contexts, computes and SHA-256 seals all predictions before the independent historical proof oracle, and compares the sealed development predictions with the actual patched Lean 4.35 target replay verdicts:

Target imported context	Replay-free prediction	Separate target certificate replay
Exact original source .olean imported as artifact in new target context	CONDITIONAL_IDENTITY_CANDIDATE	ADMISSIBLE
Same source independently rebuilt in target project	REVALIDATION_REQUIRED	ADMISSIBLE
op n := 0+n	REVALIDATION_REQUIRED	INADMISSIBLE
op n := n plus unrelated definition	REVALIDATION_REQUIRED	ADMISSIBLE

• The third fixture records unnecessary revalidation caused by whole-module byte identity. It is an intentional negative result motivating precisely justified dependency support and minimal repair, not a calibration success.
• Adversarial Python tests include checker-hash mismatch, missing/tampered source recheck, changed source input, changed target claim, unsupported expression, inconsistent source/target native op AST, and all four decisions. Scientific limits are recorded in docs/RTK_PATCHED_PREORACLE_IDENTITY_V1.md.

Nonclaims

Four public development fixtures establish neither a sound general kernel transport theorem nor a prospective false-reuse rate. A byte-equal imported module and a validated native source proof do not prove full Environment/LocalContext equivalence, semantic-support completeness, independently authenticated issuer/provenance, axiom or relying policy, or revocation. The patched source module was checked by independent checker suite #209, but the target oracle remains the patched native kernel. Issues #195, #205 and held-out #177 stay open. No production VALID; draft/unmerged.

Exact-head GitHub Actions qualification pending.

Empirical correction on first native run

The first hosted patched run failed its expected equal-build candidate assertion because separately built, source-identical Lean 4.35 .olean files were byte-different. All three preliminary predictions were REVALIDATION_REQUIRED, correctly reflecting the conservative predicate. This is an actual limitation of whole-module binary identity across independent build contexts. The revised four-control protocol adds a carefully identified reused variant importing the exact source .olean bytes into a distinct target-goal process, without importing the historical theorem. It preserves the independently rebuilt equal case as an unnecessary revalidation, not a false claim of binary reproducibility. The unrelated change is a second unnecessary revalidation. No target replay verdict was reached in the initially failing native run, and qualification of the revised protocol is pending.

[fraware]

Exact-head native development finding — patched replay-free identity and revalidation costs

PR #210 head: 874ef886e67af5d294d9043e240b87840ece7523, based on #209 fef2983a42cb80076a9a3cc10a6a2e596f499b0e. GitHub compare reports exactly four changed files: a new research-only patched pre-oracle Python module, its adversarial tests, a research document, and the dedicated native CI workflow. No production OVK reliance/ledger/authorization path changed. PR is draft, open and unmerged.

Hosted exact-head qualification:

• Pinned patched Lean 4.35 native run 38601962700: COMPLETED SUCCESS. Raw job logs independently inspected.
• Full CI 38601974706: COMPLETED SUCCESS, all six jobs (unit, package, gates, template-conformance, action_default_diff_dogfood, action_strict_dogfood).
• A same-head PR-triggered native duplicate 38601974639 was still running at the time of this entry. Do not infer completion from the duplicate; push run is independently green.

Actual execution sequence in successful raw native log:

1. Pinned Lean v4.35.0 executable digest checked, historical source theorem rebuilt and independently accepted by all six source checkers: Lean paranoid, Lean4Lean, nanoda, con-leche, con-ron, Lean default. The historical proof Expr was serialized and checked in a separate source process under --trust=0.
2. Four target claims were separately observed as unproved, with the same exact statement AST, with no original historical theorem loaded. The reused target imports the exact source support .olean binary into a new target-goal environment. The equal target uses independently compiled identical source, yielding different .olean bytes; changed modifies op n, and unrelated adds an unrelated definition.
3. The replay-free screen, given only the source certificate, native source-check witness, unproved target AST, exact imported-module bytes and pinned checker, emitted and sealed:
   • reused: CONDITIONAL_IDENTITY_CANDIDATE
   • equal: REVALIDATION_REQUIRED (whole-module bytes differ despite identical source and observed op AST)
   • changed: REVALIDATION_REQUIRED (observed op definition drift)
   • unrelated: REVALIDATION_REQUIRED (whole-module bytes differ; observed op AST unchanged)
     Log markers PATCHED_FOUR_PREORACLE_PREDICTIONS_SEALED_NO_ORACLE_LABELS and PATCHED_PREORACLE_CONTEXTS_AND_PREDICTIONS_SEALED_BEFORE_REPLAY precede every target historical proof replay.
4. The patched native target oracle replayed the same exact original patched source proof, never a fresh target proof, under same-process trust_level=0. It independently adjudicated reused ADMISSIBLE, equal ADMISSIBLE, changed INADMISSIBLE, and unrelated ADMISSIBLE. The original pre-oracle seals passed SHA-256 revalidation after replay.

Scientifically important negative result: There are two observed unnecessary revalidations among these four exposed developer controls: independent same-source rebuild and unrelated imported definition change. The very first three-control workflow failed because it incorrectly expected separately rebuilt equal-source .olean bytes to be identical; logs instead established a real byte inequality. This was not concealed or worked around by treating semantic equality as byte identity. The revised reused scenario is explicitly a copied source artifact, not an independently compiled target artifact.

Strict nonclaims: Four exposed fixtures are not prospective #177 data and establish no false-reuse rate or sound conditional kernel transport theorem. The candidate is conditional; no proven complete kernel semantic support or environment equivalence, no authenticated historical issuer, source/target authority, trusted axiom/policy, revocation or production VALID. The source theorem passed independent checkers; the transported target proof was adjudicated by patched Lean's native kernel only. Issue #195 remains unresolved; issue #205 remains open; PR remains draft and unmerged.

[fraware]

Final exact-head duplicate-run check: the PR-triggered pinned Lean native workflow 38601974639 has also COMPLETED SUCCESS at the same head 874ef886e67af5d294d9043e240b87840ece7523. Both native runs, and the full six-job CI 38601974706, are green. Research scope and non-authorization boundaries unchanged; PR remains draft/unmerged.