GFRTU Toy Model

This example instantiates the core GFRTU data on a tiny trace site.

Trace Site

• Objects: $t_0$, $t_1$
• Morphisms: ${\mathrm{id}}_{t_0}$, ${\mathrm{id}}_{t_1}$, $n:t_0\to t_1$
• Topology: trivial

Recognition Fibers

Both fibers are the chain $\{\perp <m<\top \}$ with the standard Heyting structure.

Reindexing $H(n)$ is the identity.

Stabilizer and Drift

• ${\sigma }_{t_0}={\sigma }_{t_1}=\mathrm{id}$
• ${\Delta }_{t_0}(m)=\top$, others fixed
• ${\Delta }_{t_1}=\mathrm{id}$

Fixed Fibers

• $H_{t_0}^{\ast }=\{\perp ,\top \}$
• $H_{t_1}^{\ast }=\{\perp ,m,\top \}$

Closure Sequence

See goldens/toy-trace-universe-closure.md for expected $U_0,U_1,U_2$.