Martinez-Rivillas and de Queiroz gave extensional Kan semantics for the untyped lambda-calculus and later constructed the concrete K-infinity homotopy-model. The two main mathematical results of the present paper are these. First, we show that a smaller front-seed coherence package (WL, WR) together with an inner-right-front pentagon contraction already suffices to recover the associator comparison, semantic pentagon, and bridge theorems used in the later semantic arguments. Second, we prove explicit global reify, reflect, and application formulas for K-infinity, with exact coordinatewise identities at every finite stage. We also record two structural clarifications: the recursive all-dimensional continuation of the explicit low-dimensional tower is obtained by a finite packaging phase followed by a uniform equality-generated recursion; and, on a deliberately fixed forward witness language for the classical separation span, the canonical identity-type higher tower on K-infinity forces all higher non-connection once the two witness classes land at distinct points. The paper is fully formalized in Lean 4, and the project sources contain no local uses of sorry, admit, or axiom.