Star-removalの正則性境界

## Trigger この瓶の出発点である「正則言語に star-removal を反復すると有限回で停止するか」という問いは **Pin Problem 7であり、洞の発案ではない**。2026-08-27の採掘作業で、Claude Codeセッション「形式言語理論の未解決問題10選」と hora-tex の Pin problems 進捗台帳を照合し、その問いに対して手元で得た非正則反例・有限計算・二つの予想を一つの研究進捗として回収した。 ## Local progress 既知のopen problemそのものではなく、手元で得た次の切り分けを保存する。 1. **今回構成した反例候補**: 正則性を外すと、\(c_i=b^i a\) 型の増大鎖から停止しない例が得られる。 2. **停止性予想**: 入力が正則言語なら star-removal は停止する。 3. **量的予想**: 最小 DFA の状態数を \(n\) とすると、除去回数は \(n-1\) 以下。語の鎖 \(a_1^*\cdots a_m^*\) が等号例候補になる。 したがって、この瓶の中心はPin Problem 7の再掲ではなく、**正則性が停止を強制する境界を反例と二つの予想で特定すること**にある。 ## Evidence boundary **既知の問い**はPin Problem 7である。**今回の計算**として、採掘メモには3状態以下の全1054言語とランダム約43万件が2〜4段で停止したとある。これは有限計算上の証拠であり、全称的な停止定理ではない。**今回の反例構成**である非正則例と計算結果は、生ログを独立再実行しておらず、独立査読未了である。上の二命題はどちらも**予想**である。 hora-tex台帳が厳密に確定しているのは、いくつかの素朴な証明ルートが破綻することであり、Problem 7 の反例ではない。 ## Goal syntactic congruence から抜け出す stabilizer の列を、dot-depth や有限 monoid の順序構造による単調量で制御する。まず非正則反例と有限計算証拠の証明書を固定し、その後に停止性予想と量的予想を別々に攻める。