Constructive Audit of Directionality Criteria at the Pre-geometric Layer: A Signature-Level Negative-Result Report

This paper reports a constructive audit. The object of the audit is: on a constructive type-theoretic base (MLTT/HoTT core), whether three formalized readings proposed to characterize "pre-geometric-layer directedness"—incompatibility-derived partial order, intrinsic asymmetry, and transitive-chain nodes—can be completed under the base and criterion v0.1 of this paper. The audit conclusion is: under the base and criterion v0.1 of this paper, all three fail to be formalized; among them, the incompatibility partial order is a structural negative result, and intrinsic asymmetry and transitive-chain nodes are conditionally satisfied under the primitive-preorder extension path, but that path is judged failed because the A-1 "local data" semantics cannot be reconstructed on single-point fiber elements. The failure of the incompatibility partial order is structural: the symmetric incompatibility relation Inc(A,B) = A×B→⊥ cannot generate a non-trivial antisymmetric partial order (counterexample: in a three-element configuration take X=C; details in Appendix C). Further, we give a criterion-relative meta-proposition: under criterion v0.1, if a directedness relation has a primitive declaration at the signature level, then after deleting that declaration four cases are exhaustive (framework-necessary item, external addition, pure naming, rule-level derivation plus signature-level re-expression), all of which do not constitute signature-level intrinsic directedness. Accordingly, we judge: a new language requirement targeting "signature-level intrinsic directedness" is not to be initiated under the signature-level criterion; the directedness problem is transferred to rule-level criterion design (OP-1/OP-5). The audit retains several base-internal items: the base-internal expressibility of Inc, the universe hierarchy, and the ⊥ and F1c logical skeleton (definitions in Appendix E). The B-3 counterexample and the four-case exhaustion are original to this paper; the A-1 downgrade is an original audit finding (not a proof); B-1/B-2 verifications are standard type-theoretic verifications; definitions D, Lemma 2, and F1c are from the O1v1.0 archive. This paper is a negative-result report, not a theoretical proposal; interpretive choices in §6.1 are explicitly marked as non-mathematical.