スケッチ #311

Weis L2の高さ分離 ## Trigger 対象となる言語L2とその高さ問題は、Pin–Straubing–Thérien 1992が提案し、Weis 2011が未解決として残したものであり、**洞の発案ではない**。この瓶が保存するのは問題そのものではなく、2026-08-27の `gsh_bootstrap` 採掘で回収した、repository内の高さ分離 `gsh=1<rsh=2` の計算証明である。 ## Result 対象は次の二文字正則言語である。 \[ L_2=L\bigl((ab^*a\cup ba^*b(ab^*a)^*ba^*b)^*\bigr). \] `gsh_bootstrap` の計算証明は、 \[ h_{\mathrm g}(L_2)=1<2=h_{\mathrm r}(L_2) \] を与える。すなわち、complement を許す generalized star height は1だが、complement を許さない restricted star height は2である。 generalized側の鍵は、六状態DFAのsyntactic groupから立方体の四本の対角線への商作用を取り、その上でanchorを回復することである。表現は star height 1 で、元の言語との同値性が有限DFAのproduct reachabilityで完全に検査されている。restricted側は対応するloop complexityの計算と既知定理を使う。 ## Evidence boundary **既知の問題**はL2の高さ決定である。**今回の計算結果**は `gsh=1<rsh=2` であり、repository内では原始文献の記述との同値性、別実装によるcertificate検査、負のcontrolを含む完全計算がある。しかし、これは現時点で repository の evidence label `COMPUTED` である。**プログラムを離れた人間の独立再導出と、L2固有の先行研究調査は未了**である。したがって、外部へはまだ査読済み定理として公表しない。 ## Goal review packet に沿って人間が計算から独立に証明を再構成し、先行研究調査と合わせて公表可能な小論文へ仕上げる。方法論としては「anchorが直接見えないとき、適切な商作用へ移す」という設計原理を他のGSH候補へ移植する。