Non-academic needs architectural feedback -stochastic thermo

Stream: new members

[Jason Shroyer]

Hi everyone, I’m Jason.

Full disclosure first: I’m an independent researcher (Montana) with a background in music and self-taught dev, not an academic math/CS.

I’ve been working on formalizing some ideas in non-equilibrium thermodynamics (basically Assembly Theory meets Friston’s FEP). I’m using Lean as a falsification engine. I connect papers and intuitions, refine with different AI's, (including one I trained and built based on Graph-Preflexor MIT) have them write and refine the definitions, and then use the compiler to stop me from deluding myself. It seems to be working. I have some emperical results and the system recently disallowed a theorem I thought was true (regarding NCD spectral stability)... which forced me to correct some assumptions about validity horizons. Still a win.

I now have a repo (sgc-lean) with sorry-free proofs for things like the Doob-Meyer decomposition and spectral gap preservation under coarse-graining.

Since I'm steering via AI, I suspect I'm getting weird patterns or might be way off track but I am doing my best. For example, I implemented an explicit L2(π) geometry structure rather than using Mathlib's typeclasses to handle measure changes.

I’m looking for feedback. on whether these architectural choices paint me into a corner. I just want to learn how to audit the machine better and get closer to Mathlib standards. Brutal architecture roasts welcome!

I appreciate any feedback.
J.

https://github.com/JasonShroyer/sgc-lean

[Fengyang Wang]

Welcome! Have a look at the Lean Finder or let an AI agent screen your local source files, which would trim down a lot of what you currently have and you may find existing results in Mathlib to be helpful. Personally, I raise a red flag whenever a proof (generated by AI) exceeds 30 lines. Either breaking it down to lemmas or scrutinizing whether the current approach is optimal enough. I learnt a lot by merely optimizing an existing formalization.

[Matteo Cipollina]

Hi, it seems you are redefining from a specific axiomatic setting (embedded in the definitions) things that are either already in mathlib in a general setting (eg ## Mathlib.Probability.Kernel.Invariance instead of the definitions in this file; leveraging this and this discussion for Doob-Meyers etc). I'd also recommend you leverage mathlib for spectral API, QuantumInfo and PhysLean for most of the general physics and quantum info. Then you can try to show that your objects instantiate these general and semantically meaningful typeclasses and take it from there.

[A.]

Yes, one advantage of working within the Mathlib framework is that it reduces the burden for readers. Even if all your proofs typecheck, one still has to read the statements! And there are quite a lot here.

[A.]

I'm not sure that wanting to avoid the typeclass system is a valid excuse for not using Mathlib's MeasurableSpace. Indeed if you need to use different σ-algebras then you have no choice but to avoid it anyway.

[Jason Shroyer]

Thanks everyone, this is seriously fantastic
@A. you pinpointed exactly where I got stuck!
I actually started out trying to use the standard Mathlib typeclasses MeasurableSpace, InnerProductSpace, etc… that’s the point of Mathlib. But I kept running into typeclass hell with renormalization.
This project focuses on coarse-graining. The system flows through a sequence of partitions (P0 -> P1 -> P2...). The sigma-algebra is the dynamic variable changing at every step. The standard typeclass system which wants one static instance per type was really fighting against this. I couldn't figure out how to 'hot swap' the measurable space as the flow evolved without casting problems between different types every three lines.
That is where passing the structures explicitly became the pattern. The goal was to keep the proofs readable for a physicist (maybe a misled goal?) so they could could just read the flow from L to L_bar without wading through a bunch of type boilerplate.
My genuine question for you guys…
How is this kind of thing usually handled? I feel like I missed a big opportunity. When you have a process where the underlying algebra or measure is dynamic is there a standard design pattern?
Is the explicit structure approach accepted when the structure itself is the variable?

I am wondering if it would be useful/ permissible to build a bridge module?
If I could build a file proving that at any fixed snapshot in the flow, the custom areas instantiate the standard Mathlib.Probability.Kernel and PhysLean classes.
Would that reduce the friction… reader burden? While letting me keep the explicit logic for the renormalization steps?
Matteo, thanks for the links. I had no idea about the Probability.Kernel.Invariance work. I will definitely look at that!

And again, thank you so much for helping. I really needed human eyes on this!

[A.]

In docs#MeasureTheory.condExp you see an example from the library of a MeasurableSpace (m) being passed explicitly. Another one (m₀) is being passed implicitly. But neither comes from typeclass resolution.

[A.]

I guess it's less than ideal that in that docs link you can't see which MeasurableSpace is used for μ. (That is indeed because the doc generator is thinking typeclasses.) But if you look in the source you will see it made explicit: (μ : Measure[m₀] α).

[Jason Shroyer]

I see the explicit m now.

That’s awesome thank you! Does condExp let me work with it like a regular function where I can do pointwise algebra (ring) without issues, or should I still think of it as…almost everywhere?

Basically… I needed Martingale theorems but couldn’t lose the exact algebraic structure of the thermodynamic potential. Right? Do I still need to completely refactor?

If I switch to condExp, do I lose the ability to state it pointwise?

SGC/Thermodynamics/DoobMeyer.lean

theorem doob_decomposition (P : Matrix V V ℝ) (Φ : V → ℝ) (x y : V) : Φ y - Φ x = predictableIncrement P Φ x + martingaleIncrement P Φ x y := by simp only [predictableIncrement, martingaleIncrement] ring

[A.]

docs#MeasureTheory.condExp returns a regular function. But it is only essentially unique docs#MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq.

[A.]

Your theorem doob_decomposition has its parallel in docs#MeasureTheory.martingalePart_add_predictablePart. Like yours, this equality follows closely from the definitions and holds everywhere in Ω.

[A.]

If you don't mind me asking, what does it mean to say that you trained and built your own AI? Like, was there a set of weights you started from? And did it write most of this Lean code?

[Jason Shroyer]

@A.

The martingalePart_add_predictablePart is a huge relief. If it holds everywhere pointwise, then I probably didn't break anything, I just re-implemented the wheel. I can definitely live with that! That should mean that the thermo architecture holds. Right?

Regarding the AI, it’s a custom stack.

I initially built a system based on MIT’s Graph-PRefLexOR architecture, wanting to upgrade their backbone from a 3B model to a Qwen 2.5 7B Base (LoRA trained with two stages -ORPO and DRPO) and rebuilding their Critic model from scratch (on Llama 3) when I hit credential roadblocks. Still not happy about the odd gatekeeping on that… I also added "bayesian-MCTS" (ARISE) but rarely used.

The original goal was a symbolic research assistant to abstract and "dream up" science by recombining concepts. But in the process, I noticed the RL dynamics looked exactly like closed-system thermodynamics. Exactly. Then I got excited and decided to pivot. I went back to my college day fascination with emergence… Schrödinger's What is Life? Into the Cool… Then I learned about Chentsov’s Theorem, and the Fisher-Rao metric, trying to understand Friston and why in his theory Markov Blankets exist. I saw a critique of Friston that he assumes the blankets exist so I set out to see if I could find out why.

Currently, my workflow is: I use Windsurf (Opus 4.5) for the heavy lifting, with Gemini, Grok, and Perplexity in specialized roles. I get curious, cast a wide net, and connect the dots from what I have read. When I find a cool connection, I conduct the AI stack, read, build, and refine, refine, refine.

I've had a stack of little research papers and good experimental results for months, but I was terrified of coming across as a crackpot even to my local profs. I decided that IF I could get the core theory to a sorry-free state in Lean, then it would be worth showing to someone.

What I have now I regard as a mathematical artifact that I believe has value, but I need more eyes on it. I’m hoping you and others can help guide me on the professional refinement and interpretation from here.