`BookProof.FockDegreesOfFreedom.Gravity.ghostRawCard` : Fintype.card GhostRaw = 19 + 1

Prove the following Lean 4 theorem from ChapterFockDegreesOfFreedom.

BookProof.FockDegreesOfFreedom.Gravity.ghostRawCard : Fintype.card GhostRaw = 19 + 1

Formalization note: Lean 4 identifier BookProof.FockDegreesOfFreedom.Gravity.ghostRawCard.

Retired 2026-10-30 — superseded by a corrected statement, not withdrawn. This node is a name collision rather than a dropped binder. ChapterFockDegreesOfFreedom.lean defines GhostRaw/ghostRawCard once per theory (NavierStokes, YangMills3D, YangMills4D, Gravity); the published node is keyed …Gravity.ghostRawCard but carries the NavierStokes statement $\mathrm{card}\,\mathrm{GhostRaw} = 3 + 1$, while the Gravity bundle defines GhostRaw = Fin 4 ⊕ (Fin 4 × Fin 4) with cardinality $19 + 1$. The node's own accepted disproof is precisely the arithmetic mismatch $20 \ne 4$.

Where the fix lives. In the source of record the four theory tables carry distinct, theory-suffixed names, so no name-keyed extraction can pick the wrong statement:

• BookProof.FockDegreesOfFreedom.Gravity.ghostRawCard_gravity in timepiece/BookProof/ChapterFockDegreesOfFreedom.lean (Lean 4.28 tree),
• BookProof.FockDegreesOfFreedom.Gravity.ghostRawCard_gravity in timepiece331/BookProof/ChapterFockDegreesOfFreedom.lean (Lean 4.33.1 tree).

The case is closed in the source, not on the platform: the four theory tables now carry distinct names (ghostRawCard_navierStokes, ghostRawCard_yangMills3D, ghostRawCard_yangMills4D, ghostRawCard_gravity), so no name-keyed extraction can pick the wrong statement again. This record stays readable and importable; its proof status is unchanged.