Skip to content

Commit dc39d2c

Browse files
Xinze-Li-MoqianXinze-Li-Moqian
committed
refactor(poincare): merge statement+proof into main-net.json; rename folder to poincare-network/
- Rename poincare-conjecture/ -> poincare-network/. - Merge the statement (8 nodes) and proof (30 nodes) graphs into a single main-net.json (30-node union; statement is a subgraph of proof). - Keep the pre-merge two-file split under tmp/ as a progress snapshot.
1 parent 75346d3 commit dc39d2c

3 files changed

Lines changed: 326 additions & 0 deletions

File tree

‎poincare-network/main-net.json‎

Lines changed: 326 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,326 @@
1+
{
2+
"08f271887ce9": {
3+
"ref": [
4+
"08f271887ce9"
5+
],
6+
"statement": "M",
7+
"notes": {
8+
"title": "manifold M",
9+
"content": "The manifold M (Skolem constant for the universally quantified object)."
10+
}
11+
},
12+
"70fb700dcda1": {
13+
"ref": [
14+
"08f271887ce9"
15+
],
16+
"statement": "\\mathrm{manifold3}(⟦08f271887ce9⟧)",
17+
"notes": {
18+
"title": "3-manifold",
19+
"content": "M is a 3-dimensional manifold."
20+
}
21+
},
22+
"53e017a25873": {
23+
"ref": [
24+
"08f271887ce9"
25+
],
26+
"statement": "\\mathrm{closed}(⟦08f271887ce9⟧)",
27+
"notes": {
28+
"title": "closed",
29+
"content": "M is closed: compact and without boundary."
30+
}
31+
},
32+
"6b67d6146914": {
33+
"ref": [
34+
"08f271887ce9"
35+
],
36+
"statement": "\\pi_1(⟦08f271887ce9⟧) = 1",
37+
"notes": {
38+
"title": "simply connected",
39+
"content": "The fundamental group of M is trivial."
40+
}
41+
},
42+
"ddc5d8071d26": {
43+
"ref": [
44+
"70fb700dcda1",
45+
"53e017a25873",
46+
"6b67d6146914"
47+
],
48+
"statement": "⟦70fb700dcda1⟧ \\land ⟦53e017a25873⟧ \\land ⟦6b67d6146914⟧",
49+
"notes": {
50+
"title": "hypotheses",
51+
"content": "M is a simply connected, closed 3-manifold."
52+
}
53+
},
54+
"1e95f7258e4c": {
55+
"ref": [
56+
"1e95f7258e4c"
57+
],
58+
"statement": "S^3",
59+
"notes": {
60+
"title": "3-sphere",
61+
"content": "The 3-dimensional sphere S³."
62+
}
63+
},
64+
"b2cd37106ef5": {
65+
"ref": [
66+
"08f271887ce9",
67+
"1e95f7258e4c"
68+
],
69+
"statement": "\\mathrm{homeomorphic}(⟦08f271887ce9⟧, ⟦1e95f7258e4c⟧)",
70+
"notes": {
71+
"title": "homeomorphic to S³",
72+
"content": "M is homeomorphic to the 3-sphere S³."
73+
}
74+
},
75+
"3dad30a9ab71": {
76+
"ref": [
77+
"ddc5d8071d26",
78+
"b2cd37106ef5"
79+
],
80+
"statement": "⟦ddc5d8071d26⟧ \\to ⟦b2cd37106ef5⟧",
81+
"notes": {
82+
"title": "Poincaré Conjecture",
83+
"content": "Every simply connected, closed 3-manifold is homeomorphic to the 3-sphere S³."
84+
}
85+
},
86+
"5c62e091b8c0": {
87+
"ref": [
88+
"5c62e091b8c0"
89+
],
90+
"statement": "P",
91+
"notes": {
92+
"title": "standard piece P",
93+
"content": "A generic standard piece of the decomposition (free variable, implicitly universal)."
94+
}
95+
},
96+
"a09d21500b1b": {
97+
"ref": [
98+
"a09d21500b1b"
99+
],
100+
"statement": "S^2 \\times S^1",
101+
"notes": {
102+
"title": "S² × S¹",
103+
"content": "The product of the 2-sphere and the circle."
104+
}
105+
},
106+
"0a88a038bec0": {
107+
"ref": [
108+
"0a88a038bec0"
109+
],
110+
"statement": "\\mathbb{RP}^3 \\# \\mathbb{RP}^3",
111+
"notes": {
112+
"title": "ℝP³ # ℝP³",
113+
"content": "Connected sum of two real projective 3-spaces; π₁ = ℤ/2 * ℤ/2."
114+
}
115+
},
116+
"02b022ba06c5": {
117+
"ref": [
118+
"08f271887ce9"
119+
],
120+
"statement": "\\mathrm{connSumOfStandardPieces}(⟦08f271887ce9⟧)",
121+
"notes": {
122+
"title": "finite connected sum",
123+
"content": "M is homeomorphic to a finite connected sum of standard pieces."
124+
}
125+
},
126+
"4760ece6f4f6": {
127+
"ref": [
128+
"5c62e091b8c0",
129+
"08f271887ce9"
130+
],
131+
"statement": "\\mathrm{standardPiece}(⟦5c62e091b8c0⟧, ⟦08f271887ce9⟧)",
132+
"notes": {
133+
"title": "P is a standard piece",
134+
"content": "P occurs as a factor in the connected-sum decomposition of M."
135+
}
136+
},
137+
"dc5fe156b050": {
138+
"ref": [
139+
"5c62e091b8c0"
140+
],
141+
"statement": "\\mathrm{sphericalSpaceForm}(⟦5c62e091b8c0⟧)",
142+
"notes": {
143+
"title": "spherical space form",
144+
"content": "P is homeomorphic to S³/Γ for a finite group Γ acting freely by isometries."
145+
}
146+
},
147+
"dd50d5fdaccc": {
148+
"ref": [
149+
"5c62e091b8c0",
150+
"a09d21500b1b"
151+
],
152+
"statement": "\\mathrm{homeomorphic}(⟦5c62e091b8c0⟧, ⟦a09d21500b1b⟧)",
153+
"notes": {
154+
"title": "P ≅ S² × S¹",
155+
"content": ""
156+
}
157+
},
158+
"a27b9c9b9e3c": {
159+
"ref": [
160+
"5c62e091b8c0",
161+
"0a88a038bec0"
162+
],
163+
"statement": "\\mathrm{homeomorphic}(⟦5c62e091b8c0⟧, ⟦0a88a038bec0⟧)",
164+
"notes": {
165+
"title": "P ≅ ℝP³ # ℝP³",
166+
"content": ""
167+
}
168+
},
169+
"02abbe5cdbc6": {
170+
"ref": [
171+
"4760ece6f4f6",
172+
"dc5fe156b050",
173+
"dd50d5fdaccc",
174+
"a27b9c9b9e3c"
175+
],
176+
"statement": "⟦4760ece6f4f6⟧ \\to \\big(⟦dc5fe156b050⟧ \\lor ⟦dd50d5fdaccc⟧ \\lor ⟦a27b9c9b9e3c⟧\\big)",
177+
"notes": {
178+
"title": "classification of pieces",
179+
"content": "Every standard piece is a spherical space form, S² × S¹ (or its unorientable variant), or ℝP³ # ℝP³."
180+
}
181+
},
182+
"b56fc4173210": {
183+
"ref": [
184+
"5c62e091b8c0"
185+
],
186+
"statement": "\\pi_1(⟦5c62e091b8c0⟧) = 1",
187+
"notes": {
188+
"title": "P simply connected",
189+
"content": ""
190+
}
191+
},
192+
"18edb0114050": {
193+
"ref": [
194+
"4760ece6f4f6",
195+
"b56fc4173210"
196+
],
197+
"statement": "⟦4760ece6f4f6⟧ \\to ⟦b56fc4173210⟧",
198+
"notes": {
199+
"title": "pieces are simply connected",
200+
"content": "Every factor of the decomposition of M is simply connected."
201+
}
202+
},
203+
"01b190b8abde": {
204+
"ref": [
205+
"5c62e091b8c0",
206+
"1e95f7258e4c"
207+
],
208+
"statement": "\\mathrm{homeomorphic}(⟦5c62e091b8c0⟧, ⟦1e95f7258e4c⟧)",
209+
"notes": {
210+
"title": "P ≅ S³",
211+
"content": ""
212+
}
213+
},
214+
"db3c95b3da54": {
215+
"ref": [
216+
"4760ece6f4f6",
217+
"01b190b8abde"
218+
],
219+
"statement": "⟦4760ece6f4f6⟧ \\to ⟦01b190b8abde⟧",
220+
"notes": {
221+
"title": "every piece is S³",
222+
"content": "Every standard piece of the decomposition of M is homeomorphic to S³."
223+
}
224+
},
225+
"5baee104cc6a": {
226+
"ref": [
227+
"5baee104cc6a"
228+
],
229+
"statement": "\\text{van Kampen: } \\pi_1(A \\# B) \\cong \\pi_1(A) * \\pi_1(B)",
230+
"notes": {
231+
"title": "cite: van Kampen",
232+
"content": "Fundamental group of a connected sum is the free product of the factors' groups; a free product is trivial iff every factor is trivial."
233+
}
234+
},
235+
"f484ae4a1775": {
236+
"ref": [
237+
"f484ae4a1775"
238+
],
239+
"statement": "\\text{fundamental groups: } \\pi_1(S^3/\\Gamma) = \\Gamma,\\ \\pi_1(S^2 \\times S^1) = \\mathbb{Z},\\ \\pi_1(\\mathbb{RP}^3 \\# \\mathbb{RP}^3) = \\mathbb{Z}/2 * \\mathbb{Z}/2",
240+
"notes": {
241+
"title": "cite: π₁ of the pieces",
242+
"content": "Among the standard pieces, only S³ (Γ = 1) is simply connected."
243+
}
244+
},
245+
"32417f9c091f": {
246+
"ref": [
247+
"32417f9c091f"
248+
],
249+
"statement": "\\text{connected sum: } S^3 \\# S^3 \\cong S^3",
250+
"notes": {
251+
"title": "cite: S³ idempotent",
252+
"content": "A finite connected sum of copies of S³ is homeomorphic to S³."
253+
}
254+
},
255+
"53c5be962bd7": {
256+
"ref": [
257+
"02b022ba06c5"
258+
],
259+
"statement": "\\mathrm{sorry}(\\text{proof of } ⟦02b022ba06c5⟧ \\text{ via Ricci flow with surgery: existence for all time, finite-time extinction from } \\pi_3 \\neq 0 \\text{, finitely many surgeries, and reversal of the surgery history})",
260+
"notes": {
261+
"title": "HOLE: Ricci flow machinery",
262+
"content": "Everything analytic lives here: Perelman existence of the flow with surgery, Colding–Minicozzi finite-time extinction, volume bound on surgery count, and the topological reconstruction of M by undoing surgeries."
263+
}
264+
},
265+
"07063e73256e": {
266+
"ref": [
267+
"02abbe5cdbc6"
268+
],
269+
"statement": "\\mathrm{sorry}(\\text{proof of } ⟦02abbe5cdbc6⟧ \\text{ via the canonical neighborhood classification of manifolds covered by } \\varepsilon\\text{-necks and caps})",
270+
"notes": {
271+
"title": "HOLE: canonical neighborhood classification",
272+
"content": "Classification of closed 3-manifolds entirely covered by canonical neighborhoods (ε-necks and ε-caps)."
273+
}
274+
},
275+
"95cf63be2671": {
276+
"ref": [
277+
"18edb0114050",
278+
"5baee104cc6a",
279+
"02b022ba06c5",
280+
"6b67d6146914"
281+
],
282+
"statement": "⟦18edb0114050⟧ \\text{ by } ⟦5baee104cc6a⟧ \\text{ from } ⟦02b022ba06c5⟧, ⟦6b67d6146914⟧",
283+
"notes": {
284+
"title": "step: pieces simply connected",
285+
"content": "π₁(M) is the free product of the factors' fundamental groups; since π₁(M) = 1, every factor's group is trivial."
286+
}
287+
},
288+
"b0cec8832750": {
289+
"ref": [
290+
"db3c95b3da54",
291+
"f484ae4a1775",
292+
"02abbe5cdbc6",
293+
"18edb0114050"
294+
],
295+
"statement": "⟦db3c95b3da54⟧ \\text{ by } ⟦f484ae4a1775⟧ \\text{ from } ⟦02abbe5cdbc6⟧, ⟦18edb0114050⟧",
296+
"notes": {
297+
"title": "step: pieces are S³",
298+
"content": "Each piece is one of the classified types and is simply connected; the group computation eliminates all but S³."
299+
}
300+
},
301+
"40e5b86f2d92": {
302+
"ref": [
303+
"b2cd37106ef5",
304+
"32417f9c091f",
305+
"02b022ba06c5",
306+
"db3c95b3da54"
307+
],
308+
"statement": "⟦b2cd37106ef5⟧ \\text{ by } ⟦32417f9c091f⟧ \\text{ from } ⟦02b022ba06c5⟧, ⟦db3c95b3da54⟧",
309+
"notes": {
310+
"title": "step: M ≅ S³",
311+
"content": "M is a finite connected sum of copies of S³, hence homeomorphic to S³."
312+
}
313+
},
314+
"797cb757c993": {
315+
"ref": [
316+
"3dad30a9ab71",
317+
"ddc5d8071d26",
318+
"b2cd37106ef5"
319+
],
320+
"statement": "⟦3dad30a9ab71⟧ \\text{ by implication introduction: assuming } ⟦ddc5d8071d26⟧\\text{, } ⟦b2cd37106ef5⟧ \\text{ was derived}",
321+
"notes": {
322+
"title": "step: close the theorem",
323+
"content": "Discharge the hypotheses to conclude the Poincaré conjecture."
324+
}
325+
}
326+
}

poincare-conjecture/poincare-conjecture-proof.json renamed to poincare-network/tmp/poincare-conjecture-proof.json

File renamed without changes.

poincare-conjecture/poincare-conjecture-statement.json renamed to poincare-network/tmp/poincare-conjecture-statement.json

File renamed without changes.

0 commit comments

Comments
 (0)