Lean proof typecheck never compiles MinPlusPwa.lean — 8 theorems and 8 of 12 sorries sit outside the build graph

[avrabe]

Proofs/Network/MinPlusPwa.lean is not reachable from any Lake root, so the
required Lean proof typecheck (lake build) context never compiles it. It
holds 8 theorems and 8 sorrys — two thirds of the repo's sorries — and none of
it is typechecked.

Found while cross-checking the new sorry ratchet (#385, PR #396) against an
independent measurement of the same number, which is the point: the gate's count
and the compiler's count disagreed, and the disagreement was real.

Evidence

1. Nothing imports it. proofs/Proofs.lean imports ten modules:

Proofs.Scheduling.{RTACore,RTA,RMBound,EDF,RTAJitteredCore,RTAJittered,
                   ArincSupply,Latency,Arinc653Isolation}
Proofs.Network.MinPlus

MinPlusPwa is not among them. A grep for MinPlusPwa across proofs/
(*.lean, *.toml) returns only its own namespace and end lines — no
import anywhere, and it is not a Lake root either:

[[lean_lib]]  name = "Proofs"      # globs defaults to the root module alone
[[lean_exe]]  name = "proofs"      root = "Main"
[[lean_exe]]  name = "codegen"     root = "Codegen"

2. Reachability, mechanically. Transitive closure of import from the three
roots (Proofs, Main, Codegen), excluding .lake/packages:

first-party .lean modules:                14
reachable from Proofs/Main/Codegen roots: 13
NOT typechecked by `lake build`:           1
    Proofs.Network.MinPlusPwa: 8 theorems, 8 sorries

3. The compiler confirms it, independently. In the Lean proof typecheck
job on PR #396 (job 92727468467), Lean emitted declaration uses 'sorry'
warnings for exactly 4 declarations, all in MinPlus.lean — matching the sorry
gate's count of 4 for that file. For MinPlusPwa.lean's 8, it emitted zero,
because it never compiled the file.

file	sorry gate	Lean compiler
Proofs/Network/MinPlus.lean	4	4
Proofs/Network/MinPlusPwa.lean	8	0

The two measurements agree exactly where the file is compiled and disagree
exactly where it is not.

Why this matters

Lean proof typecheck (lake build) is one of the 18 required status checks. For
MinPlusPwa.lean it is vacuous: the file could contain a syntax error, a
malformed proof, or a theorem that does not typecheck, and the required context
would stay green. Nothing anywhere reports that a first-party proof module was
skipped — this is the same shape as #381, #384, #385 and #388, where the
shortfall renders identically to the ideal reading.

It also qualifies the new sorry floor. --max-sorries 12 is honest about the
text of the tree, but 8 of those 12 sit in a file that is never checked, so
"12 sorries" understates the gap: an unchecked file's proofs are not merely
incomplete, they are unverified. The ratchet is still correct and should stay;
this is a second, separate hole.

Suggested fix

A reachability assertion, in the same family as check_fuzz_targets.py
(declared vs run) and check_fmt_workspaces.py (discovered vs default scope):
every first-party *.lean under proofs/ must be reachable from a declared
Lake root, or the gate fails naming the orphans. Empty scan exits non-zero, as
usual — zero-orphans-because-nothing-was-scanned is the failure mode being
guarded against.

Then either import MinPlusPwa from Proofs.lean (and deal with whatever it
reports), or delete it if it is abandoned. Which of those is right is not
obvious from outside — it may be deliberate WIP for REQ-PROOF-NC-MINPLUS-001
(v0.38.0). Wiring it in could turn the required Lean context red, so that is a
deliberate call, not a drive-by.

Candidate as a further obligation under REQ-GUARD-GATE-EVIDENCE-002, or its
v0.37.0 successor.

NOT claimed: that MinPlusPwa.lean is wrong. Only that nothing has checked it.

🤖 Generated with Claude Code