This study presents a focused case study of the explicit connective but in informal mathematical proofs. We propose an annotation scheme and analyze 261 occurrences found in 225 proofs from textbooks in logic, set theory, arithmetic, Boolean algebra, and formal semantics. The P-Label distinguishes proof-relevant content—material that forms an essential part of the proof—from metatextual comments on the proof, with contradiction-completing cases marked separately within the proof-relevant class. An optional R-Label records contrast or exception. Of the 261 occurrences, 221 (84.7%) were classified as proof-relevant. Three illustrative case studies with corresponding Lean formalizations show that informal transitions may align with formal operations but need not correspond to single proof lines, clarifying why proof relevance is not defined by line-level correspondence. In grouped five-fold prediction experiments, GPT-5.6 Terra attains 58.6% hierarchical accuracy from the target sentence. In these fixed runs, full-proof input yielded lower hierarchical accuracy in all four comparisons, with observed decreases of 15.3–26.1 points for Qwen3-8B. The study characterizes one connective rather than the full inventory of discourse relations in mathematics, providing a basis for future comparisons with other explicit connectives and implicit relations in informal mathematical proofs.