Experiments · Negative results
Lean pin of the named-path bypass
Setup and what was tested: experiment card.
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
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.