Recursive Completion in Higher K-Models: Front-Seed Semantics, Proof-Relevant Witnesses, and the K-Infinity Model

TL;DR

This paper advances the mathematical understanding of recursive completion in higher K-models, providing explicit formulas and structural insights, formalized in Lean 4.

Contribution

It introduces a simplified coherence package and explicit formulas for K-infinity, enhancing the semantic framework for higher lambda-calculus models.

Findings

Smaller coherence package suffices for key semantic theorems

Explicit global reify, reflect, and application formulas for K-infinity

Recursive all-dimensional continuation achieved with finite packaging and recursion

Abstract

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.