着想 #210

ハッシュ対象の操作論的公理化 ## Trigger ハッシュ関数の「実質的単射性」（有限回・feasibleな試行では衝突が見つからない）が、構成的数学の「有限の手続きで区別できないものは区別しない」と類似しているという観察から。Blechschmidt的な surjection ℕ→ℝ の nontrivial classifying locale の確率的類似（probabilistic classifying locale）を探る議論を経て、逆向きの発想に到達：SDGがKock–Lawvere axiomで「無限小が存在する世界」を公理化したように、「理想的なハッシュ対象Hが存在する世界」を操作論的に公理化できないか。 ## Idea **目標**：hash object H の公理化。naiveには「H は他のすべての対象から mono を受ける」だが、m: P(H) ↪ H は intuitionistic な Cantor diagonal（Lawvere fixed point theorem の系）で任意のトポスで矛盾する。Effective topos の ℕ でも不可。ただし Eff では ℕ^ℕ が subcountable（subquotient of ℕ）であり、CZF では every set is subcountable が consistent（Rathjen）— 弱い論理が緩めるのは mono ではなく subquotient の側。 **転回**：SDGは古典論理と衝突したので論理を弱めた。ハッシュの場合、衝突相手は diagonal argument そのもの（構成的に有効）なので、弱めるべきは論理ではなく **equality/mono の概念**。射の equality を asymptotic measure algebra（事象 mod negligible、security parameter で添字づけ）に値を取るものに enrich し、「H は feasible なテスト族に対して mod negligible で mono を受ける」と公理化する。すると Cantor diagonal は矛盾ではなく **collision attack の構成**に化け、公理の consistency が「diagonalization is not feasible」＝ one-way性 の圏論的言い換えになる。「feasible diagonal structure の不在」を公理に据える手つきは、Kock–Lawvere axiom の設置と構造的に同型。 **技術的成分**： - 真理値側：Simpson "Measure, randomness and sublocales"（random sublocale、measure-1 quotient）＋ asymptotic measure algebra。ただし computational indistinguishability は hybrid argument で ε が加算的に積み上がるため厳密には equivalence でなく、frame ではなく graded/quantale-enriched な論理（apRHL, 差分プライバシー論理の形）になるはず。「poly-bounded meets」の公理化が本丸。 - 計算量側：Krajíček *Forcing with Random Variables and Proof Complexity*（measure algebra 上の Boolean-valued model ＋ random variables の計算量制限。weak PHP が破れ、generic hash が真理値1で injective になる）。bounded arithmetic における PHP 証明複雑性と one-wayness の接続。 - Random oracle model は「点を持たないが nontrivial」の確率的実例：CGH uninstantiability ＝ pointless locale の類似。 ## Survey（先行研究の状況） - **Pavlovic の系列が最も近い**："Chasing diagrams in cryptography" / "Towards categorical cryptography"：secrecy notions（IND-CPA等）は可換図式で特徴づけられるが、**one-way function と PRG は「図式が可換にならない」要求**に対応し、enriched category ＋ convolution が必要になると明言。この観察が Monoidal Computer プログラム（string diagrams による computability/complexity、one-way・trapdoor functions の高水準言語が最終目標）につながった。つまり「不可逆性の圏論的公理化」は Pavlovic 自身が open な目標として掲げたまま、monoidal (bi)category の路線で部分的にしか進んでいない。 - **トポス・realizability 路線での hash/one-wayness の公理化は見当たらない**。resource-bounded realizability（quantitative classical realizability, Brunel–Terui, Hofmann SLR系）や PPT の型システム（Mitchell–Scedrov系, session types for cryptographic experiments）は「adversary の feasibility」を言語側で縛る話で、hash object の対象としての公理化ではない。 - 形式検証系（EasyCrypt, CryptoVerif, Coq での ROM 形式化）は ROM を postulate するのみで、operational axiomatization とは別問題。 - 結論：**「hash object の SDG 流公理化」というピンポイントの先行研究は現時点で見当たらず**、Pavlovic の「非可換図式＋enrichment が要る」という指摘が最良の出発点。研究テーマとしての新規性はありそう。 ## Goal 「理想ハッシュが存在する圏/トポス」のモデルが一つでも構成できれば（候補：Krajíček 型 forcing、asymptotic measure algebra 上の enriched category）、暗号の security proof の意味論的基盤になる。Lawvere fixed point theorem のどの前提を壊すのが最小かの特定は独立に圏論的な問い。 ## Personal context - Simpson の random sublocale は Rogers との Stone space self-similar sublocale 研究（2^ℕ, Bernoulli measure）と直接接続。 - 「dense → measure 1」置換で Booleanization の類似物が出る構造は、quotient topoi / Lawvere–Tierney topology の自分の研究語彙と近い。 - Krajíček forcing は「classifying topos の確率的・feasible 版」という視点で読める（surjection ℕ→ℝ の classifying locale = collapse forcing との並行）。