Documentation

CsdLean4.LF4.KahlerOnticSetup

W2: the Kähler ontic-sector interface #

Category: 3-Local (the Kähler ontic-sector interface).

Glossary: https://glossary.constraintsurfacedynamics.com/kahler-form/ Plain-language, CSD-role and formal statements of the Kahler form, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.

This module packages the CSD Kähler-sector assumptions as a single Lean structure, KahlerOnticSetup N, whose fields are sector-level HYPOTHESES. There are NO global axioms: the CSD postulates (the ontic substrate Σ, the Kähler-sector posit, typicality via a Liouville measure) live as structure fields, so they never appear in #print axioms. This is the standing CSD posture (postulates carried as hypotheses, not axioms; AXIOMS.md §0).

Honest scope #

This is the sector INTERFACE, the forward-direction scaffold that the chain

Σ-flow → projected ℂℙ^{N-1} flow → FS-isometry / transProb-preserving flow
       → unitary Schrödinger dynamics

will consume (W3 Wigner-selection and W5 projected Schrödinger dynamics build on it). It is not a proof of Σ, not a derivation of the posited CSD sector (SO-1) posit, and not a claim the ontology is closed. The load-bearing dynamical content is carried by the flow / projectable / flow_preserves_volume fields; the Kähler-geometry data is carried by the concrete pointwise / normalization fields (see the ledger below), whose manifold-level residual stays outside the structure. Do not read this file as deriving anything.

Field ledger (all fields concrete — interface tightened 2026-08-06, F-04) #

Every field is now real Mathlib content, forced on any inhabitant:

History: the abstract-placeholder pairs (removed 2026-08-06) #

Until 2026-08-06 the two Kähler-geometry conditions were carried as instance-supplied abstract pairs (IsKahlerSector : Prop + kahler_condition, IsLiouvilleKahlerVolume : Prop + liouville_eq_kahler_volume). Every concrete instance already supplied the genuine cores (IsFubiniStudyKahler N, IsProbabilityMeasure; never True), but a consumer quantified over KahlerOnticSetup could not extract those laws from the abstract fields — the F-04 finding of the 2026-08-06 external review. The pairs were therefore replaced by the concrete fields kahler_pointwise / liouville_isProbability above, with no change to any instance's proof obligations.

The manifold residual is honestly open, and narrowed 2026-08-06: the FLAT closedness dω = 0 on the tangent model is now proved (Kahler.extDeriv_fundamentalFormAlt, KahlerClosed.lean); what remains is the quotient/manifold spelling on ℂℙ^{N-1} — closedness there and the top-power identity ω^{∧(N-1)}/(N-1)! = μ_FS — pending Mathlib manifold-form API. When Mathlib grows that API, kahler_pointwise is the slot to strengthen from the pointwise IsFubiniStudyKahler to the full closed-2-form condition; the dynamical fields are unaffected. See specs/connectivity-manifest.md (link L1) and PLACEHOLDERS.md.

source
def CSD.LF4.IsFubiniStudyKahler (N : ℕ) :
Prop

The genuine formalizable core of the Kähler-sector posit. On the tangent model EuclideanSpace ℂ (Fin N) of ℂℙ^{N-1}, the Fubini–Study triple g = re⟪·,·⟫ (metric), ω = im⟪·,·⟫ (fundamental form), J = i • · (complex structure) satisfies the defining almost-Kähler relations:

  • J² = -1 (complex structure);
  • ω u v = g (J u) v (the form is the metric twisted by J);
  • g u v = ω u (J v) (the metric is recovered from ω and J);
  • ω (J u) (J v) = ω u v (ω is a (1,1)-form);
  • ω u (J u) = ‖u‖² (positivity / taming).

This is the linear-algebra core of "Σ is a Kähler sector" — the compatible with the complex structure and positive content — proved axiom-free (Kahler.fubiniStudy_pointwise_kahler_compatibility). It is the type of the structure's kahler_pointwise field (2026-08-06 tightening; formerly an instance-supplied abstract Prop, historically True before 2026-07-19). The manifold-level closedness dω = 0 and the top-power identity ω^{∧(N-1)}/(N-1)! = μ_FS need exterior calculus absent from Mathlib and remain the honestly-named residual (connectivity link L1).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CSD.LF4.isFubiniStudyKahler (N : ℕ) :
    IsFubiniStudyKahler N

    The Fubini–Study Kähler compatibility holds on the tangent model of ℂℙ^{N-1} (axiom-free; Kahler.fubiniStudy_pointwise_kahler_compatibility). This discharges the kahler_pointwise field genuinely on every ℂℙ-based instance.

    source
    structure CSD.LF4.KahlerOnticSetup (N : ℕ) :
    Type (u_1 + 1)

    The Kähler ontic-sector interface (W2). Sector-level hypotheses bundled as structure fields (no global axioms). N is the operational Hilbert dimension; the projective target ℙ ℂ (EuclideanSpace ℂ (Fin N)) matches Wigner's, so W3 consumes wigner_rigidity on pi-images directly.

    See the module docstring for the field ledger. Every field is concrete (interface tightened 2026-08-06, F-04): the Kähler-geometry content is the pointwise kahler_pointwise : IsFubiniStudyKahler N plus the normalization liouville_isProbability; the manifold-level differential-form data (dω = 0, top-power = μ_FS) stays outside the structure, honestly open at connectivity link L1.

    • Sigma : Type u_1

      The ontic sector state space Σ.

    • instMeasurable : MeasurableSpace self.Sigma

      Bundled measurable-space instance on Σ.

    • instTopological : TopologicalSpace self.Sigma

      Bundled topological-space instance on Σ.

    • compact_sigma : CompactSpace self.Sigma

      GENUINE: Σ is compact (the compact-Kähler requirement).

    • kahler_pointwise : IsFubiniStudyKahler N

      GENUINE (the pointwise core of the Kähler-sector posit, tightened 2026-08-06 — formerly an instance-supplied abstract Prop pair, which consumers could not unpack; F-04): the Fubini–Study Kähler compatibility triple on the tangent model of the projective target — J² = -1, ω = g∘J, g = ω∘J, ω a (1,1)-form, ω u (Ju) = ‖u‖². The manifold residual (closedness dω = 0 and the top-power identity ω^{∧(N-1)}/(N-1)! = μ_FS) needs exterior calculus absent from Mathlib and stays the honestly-named open piece (connectivity link L1).

    • liouvilleMeasure : MeasureTheory.Measure self.Sigma

      GENUINE: the Liouville / typicality measure on Σ.

    • liouville_isProbability : MeasureTheory.IsProbabilityMeasure self.liouvilleMeasure

      GENUINE (the normalization core of "Liouville = Kähler top-power volume", tightened 2026-08-06 from the abstract Prop pair; F-04): liouvilleMeasure is a probability measure. Registered as an instance, so [IsProbabilityMeasure S.liouvilleMeasure] is automatic for every setup S.

    • pi : self.Sigma → Projectivization ℂ (EuclideanSpace ℂ (Fin N))

      GENUINE: the projection onto the operational projective space (Wigner's target).

    • pi_measurable : Measurable self.pi

      GENUINE: pi is measurable.

    • flow : ℝ → self.Sigma → self.Sigma

      GENUINE: the deterministic ontic flow.

    • flow_preserves_volume (t : ℝ) : MeasureTheory.MeasurePreserving (self.flow t) self.liouvilleMeasure self.liouvilleMeasure

      GENUINE: each time-t flow map preserves the Liouville measure.

    • projectedFlow : ℝ → Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))

      GENUINE: the induced flow on the projective target.

    • projectable (t : ℝ) (x : self.Sigma) : self.pi (self.flow t x) = self.projectedFlow t (self.pi x)

      GENUINE (load-bearing for W3/W5): the ontic flow descends to projectedFlow along pi. This is what makes the projected dynamics Σ-covariant, the hinge the Wigner-selection / Schrödinger chain consumes.

    Instances For
      source
      noncomputable def CSD.LF4.trivialKahlerOnticSetup (N : ℕ) (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) :
      KahlerOnticSetup N

      Inhabitation witness (non-vacuity). The degenerate base case Σ = ℙ ℂ (EuclideanSpace ℂ (Fin N)), π = id, the trivial flow-family flow t = id, and liouvilleMeasure = fubiniStudyMeasure p₀. This confirms the KahlerOnticSetup N fields are mutually satisfiable (the interface is non-empty), exactly the π = id base-case role LF4.cpSectorData plays for SectorData. The two Kähler-geometry fields are the concrete kahler_pointwise := isFubiniStudyKahler N (the pointwise FS Kähler compatibility, proved) and liouville_isProbability (μ_FS is normalized, an instance); the dynamical fields are the identity flow (Φ = id), so this witness carries no dynamics (structural debt D1, as elsewhere in LF4). A genuine Φ ≠ id inhabitant is available by reusing kFlow on KSigma; this witness only certifies inhabitability.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance CSD.LF4.instIsProbabilityMeasureTrivialLiouville (N : ℕ) (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) :
        MeasureTheory.IsProbabilityMeasure (trivialKahlerOnticSetup N p₀).liouvilleMeasure

        The witness's Liouville measure is a probability measure (Fubini-Study is normalised). Records that the base case is a genuine typicality law.