P⁺ does not depend on which class in the positive cone names it

PositiveFrame.lean defines the two halves against a fixed reference frame, and says plainly that reference-independence is a further statement — the projection-sign cocycle, whose usual proof runs through connectedness of the Grassmannian of positive planes.

This file proves the case route (A) actually needs, and proves it by a path rather than by the cocycle: if ω and ω' lie in the same component of the positive cone, the exponential pairs at ω and at ω' are similarly oriented. So the half named by exp(β + iω) is the half named by exp(β' + iω'), and P⁺ is well defined by the cone rather than by a choice inside it.

Why a path works here and not in general

The segment from ω to ω' stays in the positive cone — that is one line of bilinear algebra once 0 < b ω ω' says the two are in the same component — so the whole family exp(β_t + iω_t) consists of positive frames, and the pairing determinant against the reference is a continuous function of t that never vanishes (pairingDet_ne_zero). It is positive at t = 0, so the intermediate value theorem makes it positive at t = 1.

The general cocycle has no such path handed to it: three arbitrary positive planes are not joined by a distinguished family. That statement remains open as its own issue, and nothing here should be read as settling it.

Scope

β is carried along the path and is otherwise unconstrained; the positivity condition is on ω alone, exactly as in isPositiveFrame_exp.

Why this path, and one declaration that does not belong to it

The subject is a comparison between two charts: the half named by exp(β + iω) against the half named by exp(β' + iω'). That is chart vocabulary, so it followed the chart out of LinearAlgebra/Lattice/Mukai/.

continuous_bilin is the exception and is recorded rather than moved. It says a bilinear form on a finite-dimensional real normed space is jointly continuous; it mentions no Mukai extension, no chart and no charge, and its neutral owner is QuadraticForm/Continuous.lean. Re-homing it there is a separate change: Continuous.lean is one of the neutral charge roots rule 8 pins, whose transitive closure may contain neither stability conditions nor geometry, and moving a declaration into a pinned root deserves its own justification rather than a ride on a path cutover.

theorem Mukai.continuous_bilin {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (hb : ∀ (x y : V), (b x) y = (b y) x) : Continuous fun (p : V × V) => (b p.1) p.2

A bilinear form on a finite-dimensional real normed space is jointly continuous. It is half the polar form of its own quadratic map.

theorem Mukai.pairingDet_exp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (hb : ∀ (x y : V), (b x) y = (b y) x) (β ω β' ω' : V) : PeriodDomain.pairingDet (realForm b) (expRe b β ω) (expIm b β ω) (expRe b β' ω') (expIm b β' ω') = ((b β) β' - ((b β') β' - (b ω') ω') / 2 - ((b β) β - (b ω) ω) / 2) * (b ω) ω' - ((b β) ω' - (b β') ω') * ((b ω) β' - (b β) ω)

The pairing determinant of two exponential pairs, in terms of b alone.

noncomputable def Mukai.segment {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (β ω β' ω' : V) (t : ℝ) : V × V

The straight-line family between two exponential data.

Equations

• Mukai.segment β ω β' ω' t = ((1 - t) • β + t • β', (1 - t) • ω + t • ω')

@[simp]

theorem Mukai.segment_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (β ω β' ω' : V) : segment β ω β' ω' 0 = (β, ω)

@[simp]

theorem Mukai.segment_one {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (β ω β' ω' : V) : segment β ω β' ω' 1 = (β', ω')

theorem Mukai.pos_segment {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω β' ω' : V) (hb : ∀ (x y : V), (b x) y = (b y) x) (hω : 0 < (b ω) ω) (hω' : 0 < (b ω') ω') (hcone : 0 < (b ω) ω') {t : ℝ} (ht : t ∈ Set.Icc 0 1) : 0 < (b (segment β ω β' ω' t).2) (segment β ω β' ω' t).2

The positive cone is convex along the segment. Positivity of b ω ω' is what says the two classes are in the same component of the cone; without it the segment can pass through zero.

noncomputable def Mukai.pathDet {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω β' ω' : V) (t : ℝ) : ℝ

The pairing determinant along the segment, as a function of t.

Equations

• One or more equations did not get rendered due to their size.

theorem Mukai.continuous_pathDet {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω β' ω' : V) (hb : ∀ (x y : V), (b x) y = (b y) x) : Continuous (pathDet b β ω β' ω')

theorem Mukai.pathDet_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω β' ω' : V) (hb : ∀ (x y : V), (b x) y = (b y) x) : pathDet b β ω β' ω' 0 = (b ω) ω ^ 2

theorem Mukai.pathDet_one {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω β' ω' : V) : pathDet b β ω β' ω' 1 = PeriodDomain.pairingDet (realForm b) (expRe b β ω) (expIm b β ω) (expRe b β' ω') (expIm b β' ω')

theorem Mukai.mem_positiveFramesPlus_exp_of_sameCone {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω β' ω' : V) (hsig : PeriodDomain.HasSignatureTwo (realForm b)) (hb : ∀ (x y : V), (b x) y = (b y) x) (hω : 0 < (b ω) ω) (hω' : 0 < (b ω') ω') (hcone : 0 < (b ω) ω') : (expRe b β' ω', expIm b β' ω') ∈ PeriodDomain.positiveFramesPlus (realForm b) (expRe b β ω) (expIm b β ω)

The half named by ω is the half named by any ω' in the same cone.

The determinant along the segment is continuous and never zero, and it starts positive, so the intermediate value theorem keeps it positive at the far end.

hsig is not a new assumption: route (A) supplies it from the Hodge index signature of V (hasSignatureTwo_realForm).

theorem Mukai.mem_positiveFramesPlus_exp_of_sameCone_of_sigPos {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω β' ω' : V) (hb : ∀ (x y : V), (b x) y = (b y) x) (hsigPos : sigPos (LinearMap.BilinMap.toQuadraticMap b) = 1) (hsigNeg : sigNeg (LinearMap.BilinMap.toQuadraticMap b) + 1 = Module.finrank ℝ V) (hω : 0 < (b ω) ω) (hω' : 0 < (b ω') ω') (hcone : 0 < (b ω) ω') : (expRe b β' ω', expIm b β' ω') ∈ PeriodDomain.positiveFramesPlus (realForm b) (expRe b β ω) (expIm b β ω)

The same statement resting on the Hodge index hypotheses alone.

hasSignatureTwo_realForm discharges the signature hypothesis, so with V = NS(X) ⊗ ℝ the inputs are: the Hodge index signature of V, and two classes in the same component of its positive cone.