Tier-S: #42 sub — Coq theorems (131 candidates, 0 admits remaining)

[hyperpolymath]

Scope (sub-issue of #42)

Split #42's 131 Coq theorems in proofs/coq/*.v (11 files) into a per-PR plan.

Current state

File	Theorems	Status
filesystem_composition.v	~25	0 admits remaining (#67 closed single_op_reversible via OpMkdirWithPerms)
filesystem_operations.v	~20	(no admits)
rmo_operations.v	~18	obliterate_not_injective keystone here
extraction.v	n/a	Extracts to OCaml; verify Rust correspondence via #45-Frontier-5
Remaining 7 .v files	~68	various

Resolution

1. Per-file PR or per-cluster PR (whichever fits owner cadence).
2. No Admitted. — register Print Assumptions axioms explicitly.
3. The verify-proofs CI job on coq-build.yml is the build oracle (per #244 ruleset gap).
4. Local make in proofs/coq/ clean before push.

References

• Parent: Proof inventory — 478 candidate theorems + 8-theorem foundation pack #42
• Closed: proofs(coq): close single_op_reversible OpRmdir branch via OpMkdirWithPerms variant #67 single_op_reversible
• Build oracle: .github/workflows/validation.yml verify-proofs job