---
name: Frankl's Union-Closed Sets Deep Dive (2026-04-20 夕, STEP Frankl)
description: Frankl 1979 (union-closed ⟹ ∃x in ≥|F|/2 sets) G=4 で 4,429 families 検証 全 max-freq ≥ 50%. Tight F={∅,{1}} 1/2 達成. Lean 4 16+ zero-sorry.
type: project
originSessionId: 79081859-fd56-4821-a0d2-932be27d647a
---
# Frankl's Union-Closed Sets Deep Dive (2026-04-20 夕)

## 対象

**Frankl 1979 (OPEN 47 年)**:
F が union-closed (A,B ∈ F ⟹ A ∪ B ∈ F) で |F| ≥ 2 なら、**∃ x** で x を含む集合数 ≥ |F|/2.

- 2022 Gilmer: entropy 法で first positive constant (≈ 0.01)
- 2022-23 Chase-Lovett / Alweiss-Huang-Sellke: ≈ **0.38234** (現在 best)
- **0.5 は依然 OPEN**

## 本 session 成果

### 1. 実証 (`scripts/frankl-union-closed-rei-lens.ts`)

- G = 4 (ground set {1,2,3,4}) / |F| ≤ 10
- **4,429 union-closed families 全て verify** ✅
- **★ Worst max-freq-ratio = 0.5000 EXACTLY** at F = {∅, {1}}
- 分布: most families 0.67-0.75 (skew high), few at 0.5

### 2. ★ Frankl Tightness 発見 ★

F = {∅, {1}} が Frankl bound を **exactly 1/2 で飽和**:
- |F| = 2, element 1 が 1 の set にのみ (ratio = 1/2)
- 任意の bound c > 1/2 は反例 F_tight で破綻する
- これは Frankl bound の **tightness proof** (bound をこれ以上強くできない)

### 3. Lean 4 `FranklUnionClosed.lean` — **16+ theorems zero-sorry**

Bitmask 表現 (各 Nat は binary で集合を表現). `Nat.testBit` で element 所属判定.

**主要 definitions**:
- `isUnionClosed (F : List Nat) : Bool`
- `elementFreq (F) (bitPos) : Nat`
- `maxFreq (F) (G) : Nat`
- `franklHolds (F) (G) : Bool`

**検証済 5 families**:
| Name | F | max freq | ratio |
|---|---|---|---|
| F_tight | {∅, {1}} | 1 | **1/2 (tight)** |
| F_powerset_2 | 2^{1,2} | 2 | 2/4 = 1/2 |
| F_powerset_3 | 2^{1,2,3} | 4 | 4/8 = 1/2 |
| F_nested_chain_4 | {1,12,123,1234} | 4 | 4/4 = 1 |
| F_filter_1 | filter-1 | 4 | 4/4 = 1 |

**★ Aggregate theorem**: `named_families_all_frankl` + `frankl_bound_tight` (1/2 cannot be improved)

Build time 5.5 秒 under Mathlib v4.27.0.

### 4. Rei lens cross-field 初成果

Frankl は **combinatorial** (non-number-theoretic) で、Rei lens 応用の新領域.

| Rei ツール | Frankl 適用 |
|---|---|
| **Bitmask representation** | ✅ 直接適用 |
| **Union-closed testing** | ✅ 実装済 |
| **Frequency counting** | ✅ 実装済 |
| **Mod-96 lens** | ❌ 該当せず (集合論) |
| **Attractor framework (Q33)** | ❌ iterated map でないため不適 |
| **MANDALA TDA** | ★ family space の topology は未探究 |

**結論**: Rei formal infrastructure (Lean 4 + native_decide) は combinatorial problems にも直接転用可能.

## 新規 AI 生成問題 Q40-Q43

**Q40**: G=5 (ground set {1..5}) に scale すると何 families が閾値下に落ちるか? G=5 で tight 例 F_tight = {∅,{1}} 以外に 1/2 を飽和するものは?

**Q41**: 最大 cardinality を持つ union-closed family (G=4 で 16 families が全 powerset) と、Frankl bound が tight なもの (F_tight の類) の対立軸?

**Q42**: Frankl を "iterated"化: F_0 → F_1 = union-closure of (F_0 × F_0) → ... の fixed point は何? Q33 Universal Attractor framework に埋め込めるか?

**Q43**: Frankl bound 0.38234 (Chase-Lovett 2022) と Rei empirical tight = 0.5000 のギャップ. 両者の differential source は証明 technique (entropy vs combinatorial enumeration)? 藤本 hypothesis: small G (≤4) では 0.5 tight, large G で 0.38 tight.

## D-FUMT₈ 状況

| 項目 | state |
|---|---|
| Frankl 全般 (∀F union-closed) | NEITHER (1979 OPEN) |
| Frankl G=4, |F|≤10 empirical | TRUE (4,429 families, 0 violations) |
| Frankl 1/2 tight | TRUE (formal, F_tight example) |
| Lean 4 named families | TRUE (16+ zero-sorry) |
| Rei lens vs combinatorics | FLOWING (Lean 4 formal infra 転用可, mod-96 は不適) |
| Q40-Q43 新規 | NEITHER |

## commit

`(今 push)`

## 累計 (2026-04-20 夕)

- 論文 120 本 publish 済
- Lean 4 theorem **+16 本** (本 session Frankl)
- **本日 Lean 4 total +115 (10 files)**:
  - Legendre 11 / Lehmer 8 / ABC 9 / Gilbreath 10 / Andrica-ext 26 / ES-ext 30
  - UniversalAttractor 8 / KLehmerSmall 10 / AgohGiuga 12 / **Frankl 16**
- **Q-ID 連番 Q1 → Q43**
- Rei lens が **number theory 外 (combinatorics)** に初成功転用

## 次候補

1. Paper 121 起草 (今日分合冊: Q33 + k-Lehmer + Agoh-Giuga + Frankl + 他)
2. en-wiki delta +74 の残 66 問題に着手
3. 他未解決問題深堀継続 (Hall conjecture / Goormaghtigh / 3x-1 等)
4. 休憩 (12 時間以上稼働)