The projection-sign cocycle

PositiveFrame.lean splits the positive frames in two by the sign of pairingDet against a fixed reference pair, and says plainly that the split might depend on the reference. It does not. For any three positive frames

0 < pairingDet r p * pairingDet p q * pairingDet q r

(pairingDet_cocycle), so the sign against one reference is the product of the signs through any other; sameOrientation_iff_of_reference turns that into independence of the partition, which is what makes positiveFramesPlus the half rather than a half.

The proof, and what it does not use

The textbook argument runs through connectedness of the Grassmannian of positive planes. That is not used here and not assumed. What replaces it is that a positive frame can be pushed into the reference plane along an explicit straight line that never leaves the positive frames:

• proj is orthogonal projection onto the reference plane, written by Cramer's rule out of the reference's own Gram determinant — invertible exactly because the reference is positive. No orthogonal-complement theory is needed.
• isPositiveFrame_interp: the whole segment t ↦ (πx + t x', πy + t y'), t ∈ [0, 1], consists of positive frames. The residual lies where Q is nonpositive, so shrinking it only increases Q on every combination.
• pairingDet_proj: the determinant against the reference does not move along that segment at all. It only ever sees the projection.
• pairingDet_proj_mul_pos: the determinant against a second reference keeps its sign along it.

At t = 0 both pairs lie in the reference plane and the identity is algebra: pairingDet_ref_comb turns two of the three factors into the same change-of-basis determinant times a Gram determinant, so that determinant appears squared and its sign drops out.

The analytic input, named

One step is not algebra: pairingDet_proj_mul_pos is the intermediate value theorem, applied through pos_mul_endpoints_of_ne_zero to a quadratic polynomial in t that pairingDet_ne_zero forbids from vanishing on [0, 1]. That is intermediate_value_Icc on ℝ, used once, and it is a theorem rather than a hypothesis — the connectedness that the textbook proof assumes about the Grassmannian is nowhere required.

theorem PeriodDomain.pairingDet_comm {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x₀ y₀ x y : M) : pairingDet Q x₀ y₀ x y = pairingDet Q x y x₀ y₀

The pairing determinant is symmetric in the two pairs: it is the same 2 × 2 determinant read along the other diagonal.

theorem PeriodDomain.pairingDet_ref_comb {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x₀ y₀ x y : M) (a b c d : ℝ) : pairingDet Q (a • x₀ + b • y₀) (c • x₀ + d • y₀) x y = (a * d - b * c) * pairingDet Q x₀ y₀ x y

Replacing the reference pair by a combination scales the determinant by the determinant of the combination.

theorem PeriodDomain.pairingDet_self {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x y : M) : pairingDet Q x y x y = 4 * Q x * Q y - QuadraticMap.polar (⇑Q) x y ^ 2

The determinant of a pair against itself is its Gram determinant.

theorem PeriodDomain.pairingDet_self_pos {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {x y : M} (h : IsPositiveFrame Q x y) : 0 < pairingDet Q x y x y

A positive frame has positive Gram determinant.

theorem PeriodDomain.isPositiveFrame_iff_forall_combination {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x y : M) : IsPositiveFrame Q x y ↔ ∀ (a b : ℝ), a ≠ 0 ∨ b ≠ 0 → 0 < Q (a • x + b • y)

A pair is positive exactly when Q is positive on every nontrivial combination. Sylvester's criterion in the form the interpolation argument wants.

noncomputable def PeriodDomain.projCoeffFst {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (x₀ y₀ v : M) : ℝ

The x₀-coefficient of the orthogonal projection onto the reference plane, solved out of the 2 × 2 Gram system by Cramer.

Equations

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

noncomputable def PeriodDomain.projCoeffSnd {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (x₀ y₀ v : M) : ℝ

The y₀-coefficient of the orthogonal projection onto the reference plane.

Equations

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

noncomputable def PeriodDomain.proj {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (x₀ y₀ v : M) : M

Orthogonal projection onto the plane of a positive frame, written out in the pair's own coordinates. No general orthogonal-complement theory is needed: the Gram determinant of a positive frame is invertible, so Cramer's rule gives the projection directly.

Equations

• PeriodDomain.proj Q x₀ y₀ v = PeriodDomain.projCoeffFst Q x₀ y₀ v • x₀ + PeriodDomain.projCoeffSnd Q x₀ y₀ v • y₀

theorem PeriodDomain.polar_proj_fst {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {x₀ y₀ : M} (h₀ : IsPositiveFrame Q x₀ y₀) (v : M) : QuadraticMap.polar (⇑Q) x₀ (proj Q x₀ y₀ v) = QuadraticMap.polar (⇑Q) x₀ v

theorem PeriodDomain.polar_proj_snd {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {x₀ y₀ : M} (h₀ : IsPositiveFrame Q x₀ y₀) (v : M) : QuadraticMap.polar (⇑Q) y₀ (proj Q x₀ y₀ v) = QuadraticMap.polar (⇑Q) y₀ v

theorem PeriodDomain.proj_mem_pairSpan {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (x₀ y₀ v : M) : proj Q x₀ y₀ v ∈ pairSpan x₀ y₀

theorem PeriodDomain.sub_proj_mem_orthogonal {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {x₀ y₀ : M} (h₀ : IsPositiveFrame Q x₀ y₀) (v : M) : v - proj Q x₀ y₀ v ∈ orthogonal Q (pairSpan x₀ y₀)

What the projection is for: the residual is orthogonal to the reference plane, so Q is nonpositive on it.

theorem PeriodDomain.pairingDet_proj {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {x₀ y₀ : M} (h₀ : IsPositiveFrame Q x₀ y₀) (x y : M) : pairingDet Q x₀ y₀ (proj Q x₀ y₀ x) (proj Q x₀ y₀ y) = pairingDet Q x₀ y₀ x y

The determinant only sees the projection. Both entries of each column are pairings against the reference, and those are unchanged by projecting.

theorem PeriodDomain.pos_mul_endpoints_of_ne_zero {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc 0 1)) (hne : ∀ t ∈ Set.Icc 0 1, f t ≠ 0) : 0 < f 0 * f 1

A continuous nonvanishing function on [0, 1] takes the same sign at both ends. This is the only analytic input the cocycle needs.

theorem PeriodDomain.isPositiveFrame_interp {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) {x₀ y₀ x y : M} (h₀ : IsPositiveFrame Q x₀ y₀) (h : IsPositiveFrame Q x y) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : IsPositiveFrame Q (proj Q x₀ y₀ x + t • (x - proj Q x₀ y₀ x)) (proj Q x₀ y₀ y + t • (y - proj Q x₀ y₀ y))

Shrinking the orthogonal component keeps a pair positive. The residual lies where Q is nonpositive, so scaling it down by t ≤ 1 only increases Q on every combination.

theorem PeriodDomain.pairingDet_proj_mul_pos {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) {x₀ y₀ u v x y : M} (h₀ : IsPositiveFrame Q x₀ y₀) (huv : IsPositiveFrame Q u v) (h : IsPositiveFrame Q x y) : 0 < pairingDet Q u v (proj Q x₀ y₀ x) (proj Q x₀ y₀ y) * pairingDet Q u v x y

The sign against a second reference survives the projection. The two frames are the ends of an interpolation through positive frames, and the determinant against (u, v) is a quadratic polynomial along it that never vanishes.

theorem PeriodDomain.pairingDet_cocycle {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) {x₀ y₀ u v x y : M} (h₀ : IsPositiveFrame Q x₀ y₀) (huv : IsPositiveFrame Q u v) (h : IsPositiveFrame Q x y) : 0 < pairingDet Q x₀ y₀ x y * pairingDet Q x y u v * pairingDet Q u v x₀ y₀

The projection-sign cocycle. For any three positive frames the three pairing determinants taken cyclically have positive product, so the sign against one reference is the product of the signs through any other.

theorem PeriodDomain.sameOrientation_iff_of_reference {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) {x₀ y₀ u v : M} (h₀ : IsPositiveFrame Q x₀ y₀) (huv : IsPositiveFrame Q u v) {p q : M × M} (hp : IsPositiveFrame Q p.1 p.2) (hq : IsPositiveFrame Q q.1 q.2) : SameOrientation Q x₀ y₀ p q ↔ SameOrientation Q u v p q

The orientation partition does not depend on the reference. Changing the reference pair either preserves every sign or flips every sign, so SameOrientation against one positive frame is SameOrientation against any other.