All pull requests

Pull requests

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

  #210·fraware opened Oct 14, 2026Owner·

  ·
  2

• research: reconstruct patched historical Lean certificate and replay in changed targets

  #209·fraware opened Oct 14, 2026Owner·

  ·
  2

• research: patched Lean 4.35 source-text drift controls, no historical Expr transport claim

  #208·fraware opened Oct 14, 2026Owner·

  ·
  1

• research: reconstruct patched Lean historical proof and independently replay against target changes

  #207·fraware opened Oct 14, 2026Owner·

  ·
  1

• research: smoke-test patched Lean 4.35 paranoid checker suite in isolated CI

  #206·fraware opened Oct 13, 2026Owner·

  ·
  1

• research: formally delimit actual Lean Kernel transport by full-context identity

  #204·fraware opened Oct 13, 2026Owner·

  ·
  1

• research: cross-check Lean Expr constant references before certificate transport

  #203·fraware opened Oct 13, 2026Owner·

  ·
  2

• research: fail closed on native axiom support in zero-trust Lean pre-oracle

  #202·fraware opened Oct 13, 2026Owner·

  ·
  2

• research: validate exact Lean historical certificate and target contexts under --trust=0

  #201·fraware opened Oct 13, 2026Owner·

  ·
  1

• research: bind Lean native kernel-header state in pre-oracle reuse checks

  #200·fraware opened Oct 13, 2026Owner·

  ·
  1

• research: kernel-check bounded support preservation and exclude unmodeled projections

  #199·fraware opened Oct 13, 2026Owner·

  ·
  1

• research: close local-declaration escape from Lean imported-byte identity

  #198·fraware opened Oct 13, 2026Owner·

  ·
  1

• research: pre-oracle Lean byte-identity candidates sealed before native adjudication

  #197·fraware opened Oct 12, 2026Owner·

  ·
  1

• research: independent target-kernel replay of serialized historical Lean certificate

  #196·fraware opened Oct 12, 2026Owner·

  ·
  1

• research: fail-closed bounded Lean declaration reference closure with structural Name identities

  #194·fraware opened Oct 12, 2026Owner·

  ·
  1

• research: record Lean source and target axiom dependencies with target-only drift control

  #193·fraware opened Oct 12, 2026Owner·

  ·

• research: independently kernel-check serialized Lean source proof against source claim

  #192·fraware opened Oct 12, 2026Owner·

  ·

• research: native Lean Expr decoder with checked source-proof roundtrip

  #191·fraware opened Oct 12, 2026Owner·

  ·

• research: bind native Lean proof, structural AST and olean inventories into fail-closed preoracle evidence

  #190·fraware opened Oct 12, 2026Owner·

  ·

• research: native Lean structural Expr/Level AST identities before target proof replay

  #189·fraware opened Oct 12, 2026Owner·

  ·

• research: demonstrate old-proof invalidation under same-name imported Lean definition drift

  #188·fraware opened Oct 12, 2026Owner·

  ·

• research: compare separately provisioned Lean installations and imported .olean inventories

  #187·fraware opened Oct 12, 2026Owner·

  ·

• research: hash imported Lean .olean modules and inspect old-proof references without target replay

  #186·fraware opened Oct 12, 2026Owner·

  ·

• research: native Lean 4.14 constant-support extraction development probe

  #185·fraware opened Oct 12, 2026Owner·

  ·

• research: typed Lean evidence-applicability predictor with explicit support closure

  #184·fraware opened Oct 12, 2026Owner·

  ·