Physlib export root: the Fubini–Study geometry of ℂℙⁿ and its Fisher–Rao bridge

Category: Special (a convenience re-export; the review scope of the Physlib export).

This module contains no mathematics. Its import closure within CsdLean4/Mathlib/ is the review scope of the Physlib (leanprover-community/physlib) work around PR #1652. Of it, what is offered to Physlib is slice 2 alone (2026-09-18): the vector-level files Analysis/InformationGeometry/FubiniStudyFisherRao.lean (the Born map and the Fisher–Rao identity) and Analysis/InformationGeometry/BraunsteinCaves.lean (homogeneous coordinates and the Braunstein–Caves inequality), which the exporter emits Physlib-ready from scripts/physlib-sidecars/. The rest stays here, on the Mathlib track: the manifold structure of ℂℙⁿ with its affine atlas, differential forms and the exterior derivative, the symplectic and Kähler structure, the Fubini–Study form, metric and volume, the torus moment map, and the bridge

`fsMetric x u v = fisherRaoInner (toOpenSimplex x) (momentDeriv x u) (momentDeriv x v)`

for u horizontal at a point of the regular stratum (Projectivization.fsMetric_eq_fisherRaoInner), with its vector-level form FisherRao.fisherRaoInner_bornDeriv on the open simplex of FisherRao.lean.

scripts/export-physlib.sh computes that closure, slices it in dependency order, emits slice 2 in Physlib's form (module-doc template, columns, [ref:] tags, terse docstrings, checked by replicas of Physlib's linters), checks that nothing mentions this repository outside provenance notes, builds everything against Physlib's Mathlib pin, and writes CsdLean4/Interop/Physlib/MANIFEST.md, the page a reviewer reads first. Nothing in the closure imports a CSD layer (scripts/check-import-hygiene.sh, rule 4).

When Physlib has merged the tree and this repository depends on Physlib, this directory gains the one-line adapters between the two libraries' quantum-state types and the export script retires. Until then it is the window, not the wall.