Auto sync: 2025-08-29 10:21:31 (9 files changed)

M  .obsidian/plugins/colored-tags/data.json

M  .sessions/nvim_config.vim

D  Projects/HX_PINN/HX_model.py

A  "Zettelkasten/Fleeting Notes/Daily/2025-08-27.md"

A  "Zettelkasten/Permanent Notes/20250826114550-heilmeier-catechism.md"

A  "Zettelkasten/Permanent Notes/Thesis/3100-erlm-quad-chart-template.odp"

A  "Zettelkasten/Permanent Notes/Thesis/DR-20250826144307-heilmeier-questions.md"

A  "Zettelkasten/Permanent Notes/Thesis/DR-20250826145452-title-ideas.md"

.obsidian/plugins/colored-tags/data.json

@@ -323,7 +323,8 @@
     "Formal-Methods": 311,
     "admin": 312,
     "hub": 313,
-    "daily": 314
+    "daily": 314,
+    "weekly": 315
   },
   "_version": 3
 }

.sessions/nvim_config.vim

@@ -18,11 +18,12 @@ badd +27 ~/.config/nvim/lua/custom/language_specific_commands/markdown_and_tex.l
 badd +37 ~/.config/nvim/lua/custom/configs/lspconfig.lua
 badd +2 custom/init.lua
 badd +11 custom/mappings.lua
+badd +385 custom/zk.lua
 argglobal
 %argdel
-edit ~/.config/nvim/lua/custom/configs/lspconfig.lua
+edit custom/zk.lua
 argglobal
-balt ~/.config/nvim/lua/custom/language_specific_commands/markdown_and_tex.lua
+balt ~/.config/nvim/lua/custom/plugins.lua
 setlocal foldmethod=manual
 setlocal foldexpr=v:lua.vim.treesitter.foldexpr()
 setlocal foldmarker={{{,}}}
@@ -33,12 +34,12 @@ setlocal foldnestmax=20
 setlocal foldenable
 silent! normal! zE
 let &fdl = &fdl
-let s:l = 37 - ((36 * winheight(0) + 28) / 57)
+let s:l = 375 - ((40 * winheight(0) + 30) / 60)
 if s:l < 1 | let s:l = 1 | endif
 keepjumps exe s:l
 normal! zt
-keepjumps 37
-normal! 059|
+keepjumps 375
+normal! 067|
 tabnext 1
 if exists('s:wipebuf') && len(win_findbuf(s:wipebuf)) == 0 && getbufvar(s:wipebuf, '&buftype') isnot# 'terminal'
   silent exe 'bwipe ' . s:wipebuf

Projects/HX_PINN/HX_model.py

@@ -1,235 +0,0 @@
-# PINN for a tube-in-tube heat exchanger (steady 2D xr)
-# - Uses automatic differentiation for PDE residuals
-# - Prescribes velocity fields u_h(x,r), u_c(x,r)
-# - Solves for Th, Tw, Tc
-
-import torch
-import torch.nn as nn
-
-# ====== User-configurable physical constants (nondimensional if you scaled) ======
-Pe_h = 100.0  # Peclet (hot side)  = u_h*L/alpha_h
-Pe_c = 120.0  # Peclet (cold side) = u_c*L/alpha_c
-alpha_w_ratio = 1.0  # wall alpha relative to hot-side alpha if nondim
-Ri = 1.0  # inner radius (nondim, after scaling)
-Ro = 1.3  # outer radius
-
-device = "cuda" if torch.cuda.is_available() else "cpu"
-dtype = torch.float32  # float32 is usually fine; use float64 if residuals are stiff
-
-
-# ====== Velocity profiles (nondim) ======
-def u_h(x, r):
-    # Poiseuille in a circular tube: u_max*(1 - (r/Ri)^2). Here Ri=1 in nondim.
-    return 2.0 * (1.0 - r**2)  # average=1 if scaled; adjust factor to match Pe_h
-
-
-def u_c(x, r):
-    # Simple plug profile in annulus as a first approximation
-    return torch.ones_like(r)
-
-
-# ====== Network ======
-class MLP(nn.Module):
-    def __init__(self, in_dim=2, hidden=128, depth=7, out_dim=3, act=nn.SiLU):
-        super().__init__()
-        layers = [nn.Linear(in_dim, hidden), act()]
-        for _ in range(depth - 1):
-            layers += [nn.Linear(hidden, hidden), act()]
-        # Separate heads for Th, Tw, Tc improves conditioning
-        self.backbone = nn.Sequential(*layers)
-        self.head_h = nn.Linear(hidden, 1)
-        self.head_w = nn.Linear(hidden, 1)
-        self.head_c = nn.Linear(hidden, 1)
-
-        # Xavier init helps with tanh/SiLU nets
-        def init(m):
-            if isinstance(m, nn.Linear):
-                nn.init.xavier_uniform_(m.weight)
-                nn.init.zeros_(m.bias)
-
-        self.apply(init)
-
-    def forward(self, x, r):
-        z = torch.stack([x, r], dim=-1)
-        f = self.backbone(z)
-        Th = self.head_h(f)
-        Tw = self.head_w(f)
-        Tc = self.head_c(f)
-        return Th, Tw, Tc
-
-
-net = MLP().to(device).to(dtype)
-
-
-# ====== Utility: gradients via autograd ======
-def grads(y, x):
-    return torch.autograd.grad(
-        y, x, grad_outputs=torch.ones_like(y), create_graph=True
-    )[0]
-
-
-# ====== Collocation samplers ======
-def sample_in_hot(N):
-    # x in [0,1], r in [0,Ri]
-    x = torch.rand(N, 1, device=device, dtype=dtype)
-    r = Ri * torch.sqrt(torch.rand(N, 1, device=device, dtype=dtype))  # area-uniform
-    return x.requires_grad_(True), r.requires_grad_(True)
-
-
-def sample_in_wall(N):
-    x = torch.rand(N, 1, device=device, dtype=dtype)
-    r = torch.sqrt(
-        (Ro**2 - Ri**2) * torch.rand(N, 1, device=device, dtype=dtype) + Ri**2
-    )
-    return x.requires_grad_(True), r.requires_grad_(True)
-
-
-def sample_in_cold(N):
-    x = torch.rand(N, 1, device=device, dtype=dtype)
-    r = (Ro + (Ro)) * 0.5 * 0 + (
-        torch.rand(N, 1, device=device, dtype=dtype) * (Ro - Ri) + Ri
-    )  # simple annulus
-    return x.requires_grad_(True), r.requires_grad_(True)
-
-
-def sample_interface_Ri(N):
-    x = torch.rand(N, 1, device=device, dtype=dtype)
-    r = torch.full_like(x, Ri, requires_grad=True)
-    return x, r
-
-
-def sample_interface_Ro(N):
-    x = torch.rand(N, 1, device=device, dtype=dtype)
-    r = torch.full_like(x, Ro, requires_grad=True)
-    return x, r
-
-
-def sample_inlet_hot(N):
-    x = torch.zeros(N, 1, device=device, dtype=dtype, requires_grad=True)
-    r = Ri * torch.sqrt(torch.rand(N, 1, device=device, dtype=dtype))
-    return x, r
-
-
-def sample_inlet_cold_counterflow(N):
-    x = torch.ones(N, 1, device=device, dtype=dtype, requires_grad=True)
-    r = torch.rand(N, 1, device=device, dtype=dtype) * (Ro - Ri) + Ri
-    return x, r
-
-
-def sample_outlet_hot(N):
-    x = torch.ones(N, 1, device=device, dtype=dtype, requires_grad=True)
-    r = Ri * torch.sqrt(torch.rand(N, 1, device=device, dtype=dtype))
-    return x, r
-
-
-def sample_outlet_cold(N):
-    x = torch.zeros(N, 1, device=device, dtype=dtype, requires_grad=True)
-    r = torch.rand(N, 1, device=device, dtype=dtype) * (Ro - Ri) + Ri
-    return x, r
-
-
-# ====== Boundary condition targets (nondim) ======
-T_h_in = 1.0  # scale so hot inlet is 1
-T_c_in = 0.0  # cold inlet is 0
-
-# ====== Training loop ======
-opt = torch.optim.Adam(net.parameters(), lr=1e-3)
-
-for it in range(20000):
-    opt.zero_grad()
-
-    # ----- Interior residuals -----
-    Nh = Nw = Nc = 512
-    xh, rh = sample_in_hot(Nh)
-    xw, rw = sample_in_wall(Nw)
-    xc, rc = sample_in_cold(Nc)
-
-    Th, Tw, Tc = net(xh, rh)
-    Th_x = grads(Th, xh)
-    Th_r = grads(Th, rh)
-    Th_xx = grads(Th_x, xh)
-    Th_rr = grads(Th_r, rh)
-    # Hot PDE: u_h dTh/dx = (1/Pe_h)*(Th_rr + (1/r) Th_r + Th_xx)  (choose to keep xx or drop)
-    uh = u_h(xh, rh)
-    hot_res = uh * Th_x - (1.0 / Pe_h) * (Th_rr + (1.0 / rh) * Th_r + Th_xx)
-
-    (Tw_,) = net(xw, rw)[1:2]  # only Tw
-    Tw_x = grads(Tw_, xw)
-    Tw_r = grads(Tw_, rw)
-    Tw_xx = grads(Tw_x, xw)
-    Tw_rr = grads(Tw_r, rw)
-    wall_res = Tw_rr + (1.0 / rw) * Tw_r + Tw_xx  # alpha_w absorbed in scaling
-
-    Tc = net(xc, rc)[2]
-    Tc_x = grads(Tc, xc)
-    Tc_r = grads(Tc, rc)
-    Tc_xx = grads(Tc_x, xc)
-    Tc_rr = grads(Tc_r, rc)
-    uc = u_c(xc, rc)
-    cold_res = uc * Tc_x - (1.0 / Pe_c) * (Tc_rr + (1.0 / rc) * Tc_r + Tc_xx)
-
-    L_pde = hot_res.pow(2).mean() + wall_res.pow(2).mean() + cold_res.pow(2).mean()
-
-    # ----- Interface continuity (temperature + flux) -----
-    Ni = 256
-    xi, rRi = sample_interface_Ri(Ni)
-    Th_i, Tw_i, _ = net(xi, rRi)
-    # fluxes: -k dT/dr. With nondim, use ratios; set k_w/k_h = kw_rel, etc.
-    dTh_dr = grads(Th_i, rRi)
-    dTw_dr = grads(Tw_i, rRi)
-    kw_over_kh = 1.0
-    L_int_Ri = (Th_i - Tw_i).pow(2).mean() + (dTh_dr - kw_over_kh * dTw_dr).pow(
-        2
-    ).mean()
-
-    xo, rRo = sample_interface_Ro(Ni)
-    _, Tw_o, Tc_o = net(xo, rRo)
-    dTw_dr_o = grads(Tw_o, rRo)
-    dTc_dr_o = grads(Tc_o, rRo)
-    kc_over_kw = 1.0
-    L_int_Ro = (Tc_o - Tw_o).pow(2).mean() + (kc_over_kw * dTc_dr_o - dTw_dr_o).pow(
-        2
-    ).mean()
-
-    # ----- Boundary conditions -----
-    Nb = 256
-    x_in_h, r_in_h = sample_inlet_hot(Nb)
-    Th_in_pred = net(x_in_h, r_in_h)[0]
-    L_in_h = (Th_in_pred - T_h_in).pow(2).mean()
-
-    x_in_c, r_in_c = sample_inlet_cold_counterflow(Nb)
-    Tc_in_pred = net(x_in_c, r_in_c)[2]
-    L_in_c = (Tc_in_pred - T_c_in).pow(2).mean()
-
-    # Outlets: convective (∂T/∂x ≈ 0)
-    x_out_h, r_out_h = sample_outlet_hot(Nb)
-    Th_out = net(x_out_h, r_out_h)[0]
-    L_out_h = grads(Th_out, x_out_h).pow(2).mean()
-
-    x_out_c, r_out_c = sample_outlet_cold(Nb)
-    Tc_out = net(x_out_c, r_out_c)[2]
-    L_out_c = grads(Tc_out, x_out_c).pow(2).mean()
-
-    # Symmetry at r=0: dTh/dr = 0
-    Ns = 128
-    xs = torch.rand(Ns, 1, device=device, dtype=dtype, requires_grad=True)
-    rs0 = torch.zeros_like(xs, requires_grad=True)
-    Th_axis = net(xs, rs0)[0]
-    L_sym = grads(Th_axis, rs0).pow(2).mean()
-
-    # ----- Total loss with simple weights (tune these!) -----
-    L = (
-        1.0 * L_pde
-        + 5.0 * (L_int_Ri + L_int_Ro)
-        + 2.0 * (L_in_h + L_in_c)
-        + 1.0 * (L_out_h + L_out_c)
-        + 1.0 * L_sym
-    )
-
-    L.backward()
-    opt.step()
-
-    if it % 1000 == 0:
-        print(
-            f"it={it}  L={L.item():.3e}  PDE={L_pde.item():.3e}  IF={L_int_Ri.item()+L_int_Ro.item():.3e}"
-        )

Zettelkasten/Fleeting Notes/Daily/2025-08-27.md

@@ -0,0 +1,32 @@
+---
+id: 2025-08-27
+title: Daily — 2025-08-27
+type: daily
+created: 2025-08-27T18:33:33Z
+modified: 2025-08-28T17:57:53Z
+tags: [daily]
+---
+
+# Daily — 2025-08-27
+
+## Quick capture
+
+COLE GROUP MEETING
+Accomplishments:
+- Quad chart
+- writing more about LTL and building out some notes from
+papers
+- Found resources about temporal logic
+- first nuce class has happened. Codes and standards were
+cancelled
+
+to do:
+- Write goals and outcomes
+- Write more about approach. This is squishtastic
+- Actually finalize some outcomes. How do i navigate the
+fact that within switching mechanisms there is dynamics
+happening
+- I didn't say anything about what a hybrid system is.
+That's kind of the whole point of the thing.
+
+## Notes

Zettelkasten/Permanent Notes/20250826114550-heilmeier-catechism.md

@@ -0,0 +1,40 @@
+---
+id: 20250826114550
+title: Heilmeier Catechism
+type: permanent
+created: 2025-08-26T15:45:50Z
+modified: 2025-08-26T16:02:59Z
+tags: []
+---
+
+# Heilmeier Catechism
+
+George Heilmeier was a program manager at the Defense
+Advanced Research Projects Administration (DARPA) who was
+flummoxed with research proposals for artificial
+intelligence. In order to quickly sort through the
+proposals, he developed an 8 question system to quickly cut
+through the muck.
+
+This is the Heilmeier Catechism:
+
+1. What are you trying to do? Articulate your research with
+   absolutely no jargon.
+
+2. How is it done today and what are the limits of current
+   practice?
+
+3. What's new in your approach and why will you be
+   successful?
+
+4. Who cares? If you're successful, what difference will it
+   make?
+
+5. What are the risks?
+
+6. How long will it take?
+
+7. How much will it cost?
+
+8. What are the midterm and final exams? How will you
+   measure success?

Zettelkasten/Permanent Notes/Thesis/DR-20250826144307-heilmeier-questions.md

@@ -0,0 +1,39 @@
+---
+id: DR-20250826144307
+title: Heilmeier Questions
+type: thesis
+created: 2025-08-26T18:43:07Z
+modified: 2025-08-28T20:42:41Z
+tags: []
+---
+
+# Heilmeier Questions for my Thesis Topic
+
+**TITLE** 
+[[Thesis Title Ideas]]
+
+***High-Assurance Hybrid Controller Synthesis from Logical
+Specifications*** 
+
+## **What am I trying to do? No jargon!** 
+
+The goal of this research is to use formal methods to create
+hybrid controllers with provable guarantees of performance
+and safety. Hybrid control systems are control systems that
+have distinct changes in system dynamics under different
+conditions, which are often called modes. Modes are often
+defined by design requirements, and as such can be easily
+translated into formal specifications. This research will
+will eliminate the possible introduction of accidental
+errors while building controllers by automatically
+synthesizing the mode switching behavior from design
+requirements. Controller behavior within modes will be
+verified using reachability analysis.
+
+## **How is it done today?** 
+    
+## **What's new in my approach?** 
+
+## **Who cares?** 
+
+

Zettelkasten/Permanent Notes/Thesis/DR-20250826145452-title-ideas.md

@@ -0,0 +1,33 @@
+---
+id: DR-20250826145452
+title: Title Ideas
+type: thesis
+created: 2025-08-26T18:54:52Z
+modified: 2025-08-26T19:03:19Z
+tags: []
+---
+
+# Thesis Title Ideas
+
+## August 26th
+1. Hybrid Controller Synthesis from Logical Specifications
+
+2. Hybrid Mode Switching Controller Synthesis from
+   Regulatory Requirements as Logical Specifications
+
+3. Formally Verified Autonomous Hybrid Controller
+   Implementations Synthesized from Regulatory Requirements
+
+Okay so mixing these:
+
+*Formally Tractable Hybrid Controller Synthesis from Logical
+Specifications of Regulatory Requirements* 
+
+It's long. But Hybrid controller synthesis from logical
+specifications might not be enough? Also 'logical
+specifications of regulatory requirements' might not make
+much sense either. Y'know what, I think I like the first one
+best. I'm going with:
+
+***High-Assurance Hybrid Controller Synthesis from Logical
+Specifications***