The anchoring line 'example : FC728 := Erdos728.Erdos728b.erdos_728_fc' is present (Erdos728Faithful.lean:15) and build success requires it to elaborate, so FC728 is definitionally the type of erdos_728_fc, not a re-typed lookalike. Stronger than claimed: erdos_728_fc itself printed [propext, Classical.choice, Quot.sound] with no sorryAx, so the anchor target is a genuinely proved theorem, not a stub. Supported.

Reproduced cold: verify_faithful.sh builds clean (8582 jobs, 0 errors, cache-warm, ~3 min). Literal axiom line for faithful is exactly [propext, Classical.choice, Quot.sound] with NO sorryAx (confirmed the lone 'sorryAx' token in the log is the script's success banner, not an axiom list). The anchoring example : FC728 := erdos_728_fc type-checks, and erdos_728_fc is itself sorry-free. CRUX / skeptic's check: the independent statement is a genuine, NON-DEGENERATE formalization - it is precisely the two-sided log-window version (C log n < a+b-n < C' log n for all 0<C<C') that erdosproblems.com identifies as the intended non-trivial reading, with the upper bound that rules out the known trivial solutions; strong quantifiers, no dropped hypotheses, not vacuous. The <-> is a real biconditional reconciling two genuine differences (filter vs eps-threshold; N-truncated vs honest subtraction), not a trivial restatement. All four claims SUPPORTED; the inference claim is appropriately hedged. Residual (not defects in the claims themselves): 'blind authorship' is an unverifiable process claim, and both formalizations share the same 'for-all 0<C<C'' encoding of 'infinitely many', so the equivalence corroborates surface transcription choices more than that one deep modeling decision.