Anomaly- and Tadpole-Compatible Fermion Completion of Six-Dimensional SU(4) Gauge-Higgs Unification

In gauge–Higgs unification the cancellation of gauge anomalies is necessary, but is it sufficient for a viable fermion sector? On an orbifold the answer involves genuinely local data — anomalies and tadpoles bound to the fixed points — that a bulk count misses. We make the question concrete for a colored quark block embedded in the dimension-60 representation (3,60) of SU(4) on T²/Z₂, built over the two-Higgs-doublet gauge sector of Akamatsu, Hirose, Maru and Nago (AHMN, arXiv:2603.05857); the fermion embedding is our own. We fix the unique unbroken hypercharge that reproduces the Standard-Model quark charges (Y = (-7q₈+4q₁₅)/18), show by an exhaustive scan that (3,60) is the minimal SU(4) representation able to host a full quark generation, and organize every consistency requirement into a reproducible hierarchy of exact conditions: the irreducible six- and four-dimensional anomalies, the localized non-Abelian cubic residues (certified axiom-free in the Lean 4 proof assistant), the localized tadpole, the global SU(2) (Witten) constraint, and the boundary-mass matching of exotic zero modes. We then exhibit — and independently verify in exact rational arithmetic — a 45-multiplet completion that cancels the eight anomaly coefficients and the localized tadpole together, with integral local cubic residues, so that here anomaly freedom and the tadpole condition are compatible. The decisive remaining test — whether the exotics can be given mass without lifting the Standard-Model quarks — is cast as an exact bipartite-matching gate and left open pending the full brane spectrum. Every step is a finite exact computation; the results reported are certificates, not estimates. English and Spanish versions are included, together with the Lean 4 certificate, the exact SageMath verification scripts, and the full spectrum. The exact computations were carried out and cross-checked with Claude (Anthropic) as an AI research assistant against a common machine-verifiable ground truth.