mu eq pi

Stream: general

[Jinu Jang]

Hi everyone, I'm new here :wave:

I've been exploring Lean 4 through a small formalization project.
Specifically, I tried to reinterpret monadic multiplication μ as an idempotent projection π,
based on the idea that nested μ (like in the state monad) behaves similarly to projection-based flattening in linear algebra.

The Lean proof builds successfully using lake, and I’m still learning a lot.

---

:brain: GitHub repo:
https://github.com/Kairose-master/mu_eq_pi

---

I'd really appreciate any thoughts or feedback.
Also, if anyone here happens to be an arXiv endorser in cs.LO or math.CT,
I'd be very grateful for help submitting this.

My arXiv ID is RUA_jinu

I’ve also put together a draft PDF on the GitHub repo if you’re curious about the bigger idea.

Thanks so much!
– Jinu

[Justin Asher]

@Jinu Jang I can't endorse you (and maybe this is the wrong place to post your project, I would try general to get more feedback), but I wanted to point out that if you use mathjax properly the LaTeX for your README.md will render on GitHub (I believe you need to use dollar signs).

Example README.md

# Flattening the State Monad: A Vector-Space Interpretation

This repository contains the full formalisation and supporting materials for the paper:

> **"Flattening the State Monad via Idempotent Projection in Vector Spaces"** > ∎ All proofs are verified in **Lean 4** using `mathlib4`
>
> ∎ Formal DSL application structure for **ETC** and **Kairosé DSL** > ∎ Research focus: **Monadic collapse ≈ geometric projection**

## 📚 Abstract

We present a vector-space semantics for the state monad $T_S(X) = S \\to (X \\times S)$ that flattens nested layers of state into a linear form. The central construction interprets the monadic multiplication

$$
\\mu : T_S T_S(X) \\to T_S(X)
$$

as an **idempotent projection** $P : V \\to V$ such that $P^2 = P$, via a functor

$$
F : \\text{Kleis}(T_S) \\to \\text{Vect}_{\mathbb{R}}
$$

that maps computations to real vector spaces.

## 🧮 Core Contributions

1. Defines a functor $F$ from the Kleisli category to $\\text{Vect}_{\mathbb{R}}$

2. Constructs a concrete linear map $P$ realizing monadic flattening

3. Machine-checks the identity $P^2 = P$ in Lean 4

4. Connects the result to Kairosé DSL and GPT tensor collapse

## 🛠 Build Instructions

### Requirements

* Lean 4 (v4.2 or later)

* `lake` build system

...

[Jinu Jang]

@Justin Asher
Thanks so much for checking it out and for the MathJax tip!
I didn't realize GitHub markdown required dollar signs explicitly.
I’ll fix that and maybe repost or follow up in #general as you suggested.

Really appreciate the feedback :)

[Jinu Jang]

Hi all — I previously posted this in #new to Lean, and someone suggested I share it here for broader feedback.

I've been exploring a formalization of monadic multiplication (μ) as a kind of idempotent projection (π),
specifically in the context of the state monad.

The idea is that nested state (T²X) flattens in a way that resembles a linear projection
on vector tensors like ℝ^S ⊗ ℝ^S ⊗ F(X) → ℝ^S ⊗ F(X), satisfying P ∘ P = P.
So we interpret μ ≡ π under this transformation.

The full proof builds in Lean 4 (no sorrys) and is hosted here, along with a short PDF write-up:
:organize: https://github.com/Kairose-master/mu_eq_pi

---

I'm curious whether this kind of flattening-as-projection idea has been explored before,
or if it might be generalizable to other monads or tensor structures.

Also — if anyone here happens to be an arXiv endorser in cs.LO or math.CT,
I’d be really grateful for any help submitting this project.
(ArXiv ID: RUA_jinu)

Thanks in advance for any thoughts!
– Jinu

[Jinu Jang]

Hi all — reposting this here in #proofs (previously sent to the wrong stream by accident).

I've been exploring a formalization of monadic multiplication (μ) as a kind of idempotent projection (π),
specifically in the context of the state monad.

The idea is that nested state (T²X) flattens in a way that resembles a linear projection
on vector tensors like ℝ^S ⊗ ℝ^S ⊗ F(X) → ℝ^S ⊗ F(X), satisfying P ∘ P = P.
So we interpret μ ≡ π under this transformation.

The full proof builds in Lean 4 (no sorrys) and is hosted here, along with a short PDF write-up:
:organize: https://github.com/Kairose-master/mu_eq_pi

---

I'm curious whether this kind of flattening-as-projection idea has been explored before,
or if it might be generalizable to other monads or tensor structures.

Also — if anyone here happens to be an arXiv endorser in cs.LO or math.CT,
I’d be really grateful for any help submitting this project.
(ArXiv ID: RUA_jinu)

Thanks in advance for any thoughts!
– Jinu

[Notification Bot]

3 messages were moved here from #lean4 > New to Lean by Mario Carneiro.

[Notification Bot]

2 messages were moved here from #lean4 > proofs by Mario Carneiro.

[Mario Carneiro]

@Jinu Jang Your attempted reposts were still in the wrong stream (you changed the topic name, not the stream). I've moved your posts to #general as suggested. Please continue discussion on this thread.

[Jinu Jang]

@Mario Carneiro oh I’m so sorry :cry: thank you for letting me know the system :smiling_face_with_hearts:

[Adam Topaz]

@Jinu Jang I can’t find any PDF. Is there actually a PDF writeup?

[Jinu Jang]

@Adam Topaz https://kairose-master.github.io/mu_eq_pi/pdf/mu_eq_pi.pdf here take this!
2.pdf

[Jinu Jang]

I’ve been exploring a potential generalization that I’d appreciate your input on.

Instead of treating a matrix A : V → V as an operator on vectors,

what if we interpret it as deforming the entire ambient space in which vectors reside?

That is, under a functorial view:

T(X) = \text{“space where } X \text{ lives is geometrically twisted by some effect”}

Then:

• η_X embeds X into a deformed context
• μ_X collapses nested ambient deformations
• The identity μ = π becomes the collapse of geometric nesting into a single semantic effect

This seems to extend monadic reasoning to linear algebraic structures —

not just state monads, but any context where operators act on ambient geometries (e.g., SVD, projections, eigen decompositions).

My questions:

1. Has this kind of space-centric monad interpretation been formally explored?
2. Would this require a shift toward enriched categories or structured fibrations?
3. How might one formalize such monads as “ambient deformation functors” on Vect or similar?

Any pointers, references, or counterexamples would be greatly appreciated —

thank you again for the discussion and insights so far.

– J.