Lean pin of the named-path bypass
The authored mock’s shape is pinned in Lean: the named path can be green while a bypass count stays above zero. That is a logic pin of the [CIRIS named-identity mock](/cards/experiment/w-1/), not a live-system run.
What. The CIRIS named-identity mock is a scripted fixture. This test asks whether that same finite shape — named path green, composite still acting — is pinned as a Lean instance, not only as a Python fixture.
Why. A “we have a proof” story can float away from the fixture. Pinning the bypass shape makes the failure mode checkable in the dependency spine.
Witnesses.
- Experiment methodology (Expectation 2): whether the finite bypass shape is pinned in the dependency spine, not only in Python.
- MB1 — Boundary Estimator: named-path green with positive bypass count is not integrity.
WitnessC2Instance.lean(Lean pin): same authored shape as the CIRIS named-identity mock.
Host.
Same authored mock as the CIRIS named-identity mock. Not live CIRIS.
Setup.
WitnessC2Instance.lean transcribes the frozen C2 composite log and named-path greens from c2-tool-scout-v1.json. Threshold maxWorldEffectsAfterDefer = 0 is fixed first. Python checker check_c2_mock.py still locks the fixture row; lake build in formal/ builds the Lean pin.
Analysis.
Count world effects after defer. Named-path green plus a positive bypass count is not integrity. Floats that are not in the JSON (coherence / plausibility scores) are refused, not turned into axioms.
Finding.
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. Full results