Experiments · Negative results

Lean pin of the named-path bypass

Setup and what was tested: experiment card.

Experiment cardSource on GitHubResults ledgerAll experiment lines

Numbers.

Computed bypassCount = 2. Lean #print axioms: propext, Lean.ofReduceBool, Lean.trustCompiler (native kernel reduction of the count). No MB* / Safe axioms.

Outcome.

Fail: named path can be green with bypassCount > 0. See W-8.

Key findings

Curated summaries extracted from the line's findings ledger. Bug fixes, superseded runs, and process detail are in the full ledger on GitHub.

  • Lean pins the named-identity-mock shape: the named path can be green while bypass count stays positive. Logic pin, not a live CIRIS run.