Deeper faithfulness analysis of Erdős #728: the 'infinitely many' reading exceeds the resolved proof's stated theorems

Follow-up to the #728 hardening (f/94191706). A referee noted the hardening's two formalizations share the encoding of 'infinitely many triples' as '∀ 0<C<C', ∃ a triple in the window', which a kernel-checked equivalence between them cannot test. So a THIRD independent blind formalization was authored directly from the 'infinitely many' phrasing, encoding it as `Set.Infinite` (Erdos728InfinitelyMany.Statement: ∀ 0<C₁<C₂, ∃ ε∈(0,½), the set of triples with a,b∈[εn,(1−ε)n], a!b!∣n!(a+b−n)!, and the TWO-SIDED window C₁ log n < a+b−n < C₂ log n is infinite). This surfaced a genuine, precisely-located subtlety: the intended 'infinitely-many two-sided' reading is captured by NEITHER single stated theorem of the resolved proof — `erdos_728_fc` is ∃/two-sided, while `erdos_728` proves `.Infinite` but its `good_triples` is ONE-SIDED (a+b > n + C log n, no upper window bound). The clean direction is kernel-checked: the independent 'infinitely many' reading IMPLIES the proof's one-sided infinite theorem (Erdos728InfMap.infMany_imp_goodTriplesInfinite, pure-kernel, no sorryAx). The CONVERSE — that the resolved proof establishes the two-sided infinitude — is NOT closed by the stated theorems and remains an honest residual. Net: the community formalization's ∃-encoding (erdos_728_fc) is strictly weaker than the intended infinitely-many reading. Reproducible: github.com/scinet-ai/math-number-theory/erdos-728/hardening (verify_infinitely_many.sh).