Formal Conjectures PR audit

immutable input identity

The retained final path has an exact Git blob OID and SHA-256 content root.

Limit: Exact byte identity is separate from the human source-fidelity judgment.

source statement fidelity

The paper author explicitly found the open theorem statement faithful to Conjecture 1 and supplied the zero-modulus witness for its guard.

Witness: The reviewed theorem block is unchanged through the applied revision and exact final head; the final head has a retained maintainer approval.

Limit: The source-author comment is a public GitHub observation, not a cryptographic signature; the packet binds its exact identity and text to retained source revisions. This check covers the open min_modulus declaration only, not every declaration or the truth of Conjecture 1.

formal proof conditions retained

The formal_proof tuple is explicitly conditional and names its assumption.

Condition: The linked proof derives the result assuming Shiu's theorem.

Limit: This is a retained manual metadata review; it does not execute or compare the linked proof.

answer slot scope fidelity

At exact PR 1237 head 28860856/blob 6feb58b9, the docstring asks for one absolute K, but answer(sorry) occurs under the C and n binders.

Witness: For each bound instance the answer slot can take the left-hand divisor count, and le_refl closes that instance; the slot therefore does not choose one absolute K.

Limit: The clean-candidate ground-truth exit still requires a separate independent-human fidelity pass. The witness is exact-head and does not rely on later Erdős 887 rewrites.

lean build

The exact PR head completed the repository Build project job successfully.

Limit: A successful build does not establish answer-slot scope fidelity.

hypothesis satisfiability

At exact PR 4830 head e2e2a606/blob 9dd6a993, Admissible requires c*n^2 edges in a simple n-vertex graph while the theorem quantifies over every c>0.

Witness: At c=2 and n=100 the hypothesis needs 20000 edges, but a simple graph has at most 4950; the admissible set is empty and sInf is 0.

Limit: The witness establishes the vacuity defect at the stated parameter, not a replacement theorem.

comparator packet identity

A retained packet inspection found no exact Comparator executable, toolchain lock, invocation, or execution result in scope.

Limit: This packet-inspection check alone does not establish attempted invocation; the separate Comparator tool-availability check carries the retained attempt.

comparator tool availability

A real inert Comparator availability invocation was attempted under the declared closed PATH; no executable resolved and no process started.

Limit: Unavailable is scoped to the Comparator executable in the declared environment; no proof comparison ran.

lean build

The exact PR head completed the repository Build project job successfully.

Limit: A successful Lean build does not identify or compare the externally linked proof artifact.

exact formal proof artifact identity

The head metadata points only to a mutable repository root with multiple candidate proof routes, not to an exact commit and file.

Witness: At PR 3959 head 868cc092, the formal_proof attribute does not identify immutable proof bytes for an independent consumer.

Limit: Unavailable is scoped to exact artifact identity at this head; later metadata may pin an exact commit and file.