Recursive Completion in Higher K-Models: Front-Seed Semantics, Proof-Relevant Witnesses, and the K-Infinity Model
2026-04-14 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors build on earlier work by Martinez-Rivillas and de Queiroz who gave a mathematical model (called K-infinity) for understanding the untyped lambda-calculus. They show that a simpler set of mathematical tools is enough to recover important structural properties used in the model's semantics. Additionally, they provide explicit formulas for key operations in the model and clarify its recursive structure. Their work is fully formalized in the Lean 4 proof assistant without relying on any unproven assumptions.
untyped lambda-calculusKan semanticsK-infinity homotopy modelassociatorpentagon identityreify and reflectformalizationLean 4higher category theory
Authors
Daniel O. Martinez-Rivillas, Arthur F. Ramos, Ruy J. G. B. de Queiroz
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.