arxiv: 2604.12981 · v1 · submitted 2026-04-14 · 💻 cs.LO

Recognition: unknown

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

Daniel O. Martinez-Rivillas , Arthur F. Ramos , Ruy J. G. B. de Queiroz

Authors on Pith no claims yet

Pith reviewed 2026-05-10 14:13 UTC · model grok-4.3

classification 💻 cs.LO

keywords untyped lambda calculusKan semanticsK-infinity modelhomotopy modelsfront-seed coherenceproof-relevant witnessesrecursive completionLean formalization

0 comments

The pith

A smaller front-seed coherence package with pentagon contraction recovers the key semantic theorems for the K-infinity homotopy model of the lambda calculus.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper demonstrates that the minimal coherence conditions WL and WR, together with an inner-right-front pentagon contraction, are sufficient to derive the associator comparison, semantic pentagon, and bridge theorems that support later semantic arguments. It also supplies explicit global formulas for reify, reflect, and application operations on the K-infinity model, each satisfying exact coordinatewise identities at every finite stage. These results rest on a recursive construction that packages low-dimensional data finitely and then extends uniformly via equality-generated recursion. The work further clarifies that the identity-type tower on K-infinity forces all higher non-connections once the two witness classes reach distinct points. All statements are formalized in Lean 4 with no local uses of sorry, admit, or axiom.

Core claim

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. Explicit global reify, reflect, and application formulas for K-infinity are proved, with exact coordinatewise identities at every finite stage. 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 the canonical identity-type higher tower on K-infinity forces all higher non-connection once the two witness classes land at distinct points.

What carries the argument

The front-seed coherence package (WL, WR) together with the inner-right-front pentagon contraction, which together recover the associator comparison and semantic pentagon theorems for the K-infinity model.

If this is right

The associator comparison theorem holds from the reduced coherence package alone.
The semantic pentagon theorem is recovered without larger coherence data.
Bridge theorems required for later semantic arguments become available from the same minimal conditions.
Explicit reify, reflect, and application formulas apply coordinatewise at every finite stage of K-infinity.
The higher identity-type tower forces non-connections between witness classes that land at distinct points.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The reduction in required coherence data could lower the overhead of formalizing higher homotopy models of the lambda calculus in proof assistants.
The coordinatewise explicit formulas open the possibility of direct computational checks of semantic equalities inside the model.
The forced non-connection result may clarify how proof-relevant witnesses behave in separation spans for classical logic.
The finite-packaging-plus-recursion pattern suggests a general template for building higher-dimensional models from low-dimensional data.

Load-bearing premise

The prior extensional Kan semantics and concrete K-infinity homotopy-model construction are taken as given, with the front-seed package and pentagon contraction assumed definable without additional hidden coherence data.

What would settle it

An explicit counter-derivation showing that WL, WR and the inner-right-front pentagon contraction fail to imply the associator comparison theorem would falsify the main reduction claim.

Figures

Figures reproduced from arXiv: 2604.12981 by Arthur F. Ramos, Daniel O. Martinez-Rivillas, Ruy J. G. B. de Queiroz.

**Figure 2.** Figure 2: The witness-separation span of Example 8.1. The same source and target admit a [PITH_FULL_IMAGE:figures/full_fig_p022_2.png] view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper shrinks the front-seed coherence package for K-infinity models and supplies explicit reify/reflect formulas, all backed by a full Lean 4 formalization.

read the letter

The key advance is that a minimal front-seed package consisting of just WL and WR, together with one inner-right-front pentagon contraction, already recovers the associator comparison, the semantic pentagon, and the bridge theorems. The authors also give explicit global formulas for reify, reflect, and application on the K-infinity model that hold with exact coordinatewise identities at every finite stage. Both results are presented as new and are supported by a complete Lean 4 formalization that contains no local uses of sorry, admit, or axiom. That machine-checked grounding is the strongest part of the submission and makes the reductions reproducible in principle. The structural clarifications about recursive continuation via finite packaging followed by uniform recursion are also cleanly stated. The work sits squarely on the authors' own earlier extensional Kan semantics and concrete K-infinity construction, so the novelty is incremental rather than foundational. The scope remains narrow, limited to specialists in homotopy type theory who care about coherence data for untyped lambda-calculus models. A reader already working on similar higher-dimensional constructions would find the smaller package and the coordinatewise formulas practically useful for avoiding unnecessary coherence overhead. The formalization claim is the main reason this deserves referee time; without it the reductions would be harder to trust on first reading. I would bring it to a reading group focused on formal semantics or HoTT model constructions, but I would not cite it in my own work unless I were actively extending these models. Overall the paper is coherent on its own terms and the evidence from the formalization supports sending it to peer review.

Referee Report

1 major / 2 minor

Summary. The paper claims that a smaller front-seed coherence package (WL, WR) together with an inner-right-front pentagon contraction suffices to recover the associator comparison, semantic pentagon, and bridge theorems in higher K-models for extensional Kan semantics of the untyped lambda-calculus. It also proves explicit global reify, reflect, and application formulas for the K-infinity model with exact coordinatewise identities at every finite stage. Additional clarifications are provided on the recursive all-dimensional continuation of the explicit low-dimensional tower via finite packaging and uniform equality-generated recursion, and on how the canonical identity-type higher tower forces higher non-connection on a fixed forward witness language. The work is fully formalized in Lean 4 with no uses of sorry, admit, or axiom.

Significance. If the results hold, this contributes to the field by reducing the coherence data needed for semantic arguments in homotopy models of the lambda-calculus, while providing constructive explicit formulas. The complete machine-checked formalization in Lean 4 is a strong point, as it offers independent verification of the derivations from the reduced package and supports the claims about recursive completion and proof-relevant witnesses.

major comments (1)

[front-seed semantics section] The sufficiency of the (WL, WR) package plus pentagon contraction for recovering the key theorems is load-bearing; the manuscript should make explicit which parts of the prior Martinez-Rivillas and de Queiroz K-infinity construction are used as base, to confirm no additional hidden coherence is required.

minor comments (2)

The abstract refers to 'two structural clarifications' without indicating their location in the paper; adding section references would improve navigation.
[K-infinity formulas section] Ensure that the explicit reify, reflect, and application formulas are presented with clear numbering and perhaps a table summarizing the coordinatewise identities at finite stages for better readability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful review and the recommendation of minor revision. The single major comment is addressed below; we agree that the requested clarification will strengthen the manuscript and will incorporate it in the revision.

read point-by-point responses

Referee: [front-seed semantics section] The sufficiency of the (WL, WR) package plus pentagon contraction for recovering the key theorems is load-bearing; the manuscript should make explicit which parts of the prior Martinez-Rivillas and de Queiroz K-infinity construction are used as base, to confirm no additional hidden coherence is required.

Authors: We agree that an explicit enumeration of retained base components improves clarity. In the revised manuscript we will add a short paragraph at the opening of the front-seed semantics section (Section 3) that lists the precise elements taken from Martinez-Rivillas and de Queiroz: (i) the underlying Kan-complex structure for the untyped lambda-calculus, (ii) the extensionality axioms governing the interpretation of application and abstraction, and (iii) the low-dimensional coherence data (dimensions 0–2) that initiate the recursive completion. All subsequent derivations of the associator comparison, semantic pentagon, and bridge theorems rely exclusively on the reduced (WL, WR) package together with the inner-right-front pentagon contraction; no further coherence conditions are invoked. The Lean 4 formalization already encodes this separation via the imported base modules and the isolated proofs of the new theorems, thereby providing machine-checked confirmation that no hidden coherence is required. revision: yes

Circularity Check

0 steps flagged

Minor self-citation to prior model; new derivations independent via Lean formalization

full rationale

The paper explicitly takes the prior extensional Kan semantics and K-infinity construction by Martinez-Rivillas and de Queiroz as given, but derives its central claims—the sufficiency of the reduced (WL, WR) front-seed package plus inner-right-front pentagon contraction for recovering associator comparison, semantic pentagon, and bridge theorems, plus explicit global reify/reflect/application formulas with coordinatewise identities—from this smaller package. These derivations are supported by a complete Lean 4 formalization containing no sorry, admit, or axiom, providing machine-checked grounding independent of the prior inputs. The self-citation is present but not load-bearing for the novel results, which do not reduce by construction to the base model.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on the authors' prior construction of extensional Kan semantics and the K-infinity model as background. No new free parameters are introduced, no new entities are postulated, and the Lean formalization claims to avoid any additional axioms beyond standard type theory.

axioms (1)

domain assumption Prior extensional Kan semantics and K-infinity homotopy-model construction by Martinez-Rivillas and de Queiroz
The current results are stated to recover theorems used in the later semantic arguments of that prior work.

pith-pipeline@v0.9.0 · 5521 in / 1562 out tokens · 83521 ms · 2026-05-10T14:13:35.922827+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

13 extracted references · 9 canonical work pages · 1 internal anchor

[1]

Functions of Bounded Variation and Free Discontinuity Problems

S. Abramsky and A. Jung, Domain theory, in:Handbook of Logic in Computer Science, Vol. 3, Oxford University Press, 1995, pp. 1–168.doi: 10.1093/oso/9780198537625.003.0001

work page doi:10.1093/oso/9780198537625.003.0001 1995
[2]

H. P. Barendregt,The Lambda Calculus: Its Syntax and Semantics, revised edition, Studies in Logic and the Foundations of Mathematics 103, North-Holland, 1984

1984
[3]

M. A. Batanin, Monoidal globular categories as a natural environment for the theory of weakn-categories,Advances in Mathematics136(1):39–103, 1998.doi: 10.1006/aima.1998.1724

work page doi:10.1006/aima.1998.1724 1998
[4]

T. M. L. de Veras, A. F. Ramos, R. J. G. B. de Queiroz, and A. G. de Oliveira, Computational paths—a weak groupoid,Journal of Logic and Computation35(5):exad071, 2025.doi: 10.1093/logcom/exad071. Also available as arXiv:2007.07769

work page doi:10.1093/logcom/exad071 2025
[5]

Grothendieck,Pursuing Stacks, edited by G

A. Grothendieck,Pursuing Stacks, edited by G. Maltsiniotis, Documents math´ ematiques 20, Soci´ et´ e Math´ ematique de France, 2022. (Original manuscript, 1983.)

2022
[6]

The Univalent Foundations Program,Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013

2013
[7]

The lean 4 theorem prover and programming language

L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language, in:Automated Deduction— CADE 28, LNCS 12699, Springer, 2021, pp. 625–635.doi: 10.1007/978-3-030-79876-5 37

work page doi:10.1007/978-3-030-79876-5 2021
[8]

2009 , PAGES =

J. Lurie,Higher Topos Theory, Princeton University Press, 2009.doi: 10.1515/9781400830558

work page doi:10.1515/9781400830558 2009
[9]

D. O. Mart´ ınez-Rivillas and R. J. G. B. de Queiroz, Towards a homotopy domain theory,Archive for Mathematical Logic62:559–579, 2023.doi: 10.1007/s00153-022-00856-0. Preprint: arXiv:2007.15082

work page doi:10.1007/s00153-022-00856-0 2023
[10]

D. O. Mart´ ınez-Rivillas and R. J. G. B. de Queiroz, TheK ∞ homotopyλ-model, to appear inLogic Journal of the IGPL.doi: 10.48550/arXiv.2505.07103. Preprint: arXiv:2505.07103 [cs.LO], 2025

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2505.07103 2025
[11]

D. O. Mart´ ınez-Rivillas and R. J. G. B. de Queiroz, The theory of an arbitrary higherλ-model,Bulletin of the Section of Logic52(1):39–58, 2023.doi: 10.18778/0138-0680.2023.11. Also available as arXiv:2111.07092

work page doi:10.18778/0138-0680.2023.11 2023
[12]

D. O. Mart´ ınez-Rivillas and R. J. G. B. de Queiroz, The∞-groupoid generated by an arbitrary topologicalλ-model, Logic Journal of the IGPL30:465–488, 2022.doi: 10.1093/jigpal/jzab015

work page doi:10.1093/jigpal/jzab015 2022
[13]

D. S. Scott, Continuous lattices, in:Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics 274, Springer, 1972, pp. 97–136. Originally circulated as PRG-7, Oxford University Computing Laboratory, Programming Research Group, 1971

1972