structure HamiltonianDiffeomorphism {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) : Type (max u_1 u_2)

A Hamiltonian diffeomorphism of $(M, \omega)$: data of a Hamiltonian $H$, its Hamiltonian vector field $X_H$, and the time-1 flow of $X_H$.

• H : Ω 0
• hv : HamiltonianVectorField S self.H
• flow : HamiltonianFlow S self.H self.hv

noncomputable def HamiltonianDiffeomorphism.φ {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {S : SymplecticManifold Ω VF} (f : HamiltonianDiffeomorphism S) : DFSMorphism Ω VF Ω VF

The time-1 map $\varphi^1_{X_H}: M \to M$ of the Hamiltonian flow.

theorem HamiltonianDiffeomorphism.preserves_symplectic {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {S : SymplecticManifold Ω VF} (f : HamiltonianDiffeomorphism S) : f.φ.pullback S.ω = S.ω

A Hamiltonian diffeomorphism is symplectic: $\varphi^* \omega = \omega$.

class HasFixedPoints {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (f : HamiltonianDiffeomorphism S) : Type (max 1 u_1)

The fixed-point set $\mathrm{Fix}(\varphi)$ of a Hamiltonian diffeomorphism, exposed as a finite indexing type with evaluation $\mathrm{ev}_x(g) = g(x)$ satisfying $\mathrm{ev}_x(\varphi^* g) = \mathrm{ev}_x(g)$.

• FixedPoint : Type
• fintype : Fintype (FixedPoint f)
• eval : FixedPoint f → Ω 0 → ℝ
• eval_pullback_eq (x : FixedPoint f) (g : Ω 0) : eval x (f.φ.pullback g) = eval x g

class IsNondegenerate {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (f : HamiltonianDiffeomorphism S) extends HasFixedPoints S f : Type (max 1 u_1)

Nondegeneracy of fixed points: the evaluation map on $\mathrm{Fix}(\varphi)$ is injective, i.e. distinct fixed points are separated by smooth functions.

• FixedPoint : Type
• fintype : Fintype (FixedPoint f)
• eval : FixedPoint f → Ω 0 → ℝ
• eval_pullback_eq (x : FixedPoint f) (g : Ω 0) : eval x (f.φ.pullback g) = eval x g
• eval_injective : Function.Injective HasFixedPoints.eval

class HasCohomology {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] : Type (u_3 + 1)

A graded cohomology theory $H^k(M, \mathbb{R})$ taking finite-dimensional real values.

• H : ℕ → Type u_3
• H_addCommGroup (k : ℕ) : AddCommGroup (H Ω VF k)
• H_module (k : ℕ) : Module ℝ (H Ω VF k)
• H_finiteDimensional (k : ℕ) : FiniteDimensional ℝ (H Ω VF k)

noncomputable def HasCohomology.betti {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (hC : HasCohomology) (i : ℕ) : ℕ

The $i$-th Betti number $b_i(M) = \dim_\mathbb{R} H^i(M, \mathbb{R})$.

class HasBettiNumbers {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] extends HasCohomology : Type (u_3 + 1)

Betti-number data for a manifold of dimension manifoldDim: total Betti number $\sum_{i=0}^{\dim M} b_i(M)$ packaged with the cohomology groups.

• H : ℕ → Type u_3
• H_addCommGroup (k : ℕ) : AddCommGroup (H Ω VF k)
• H_module (k : ℕ) : Module ℝ (H Ω VF k)
• H_finiteDimensional (k : ℕ) : FiniteDimensional ℝ (H Ω VF k)
• manifoldDim : ℕ
• totalBetti : ℕ
• totalBetti_eq : totalBetti Ω VF = ∑ i ∈ Finset.range (manifoldDim Ω VF + 1), Module.finrank ℝ (HasCohomology.H Ω VF i)

theorem betti_vanish_above_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (hB : HasBettiNumbers) (i : ℕ) (hi : HasBettiNumbers.manifoldDim Ω VF < i) : Module.finrank ℝ (HasCohomology.H Ω VF i) = 0

Vanishing of Betti numbers above the manifold dimension: $b_i(M) = 0$ for $i > \dim M$.

noncomputable def HasBettiNumbers.betti {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (hB : HasBettiNumbers) (i : ℕ) : ℕ

The $i$-th Betti number $b_i(M) = \dim_\mathbb{R} H^i(M, \mathbb{R})$ recovered from the Betti-number data.

structure ActionFunctional {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (f : HamiltonianDiffeomorphism S) : Type (max 1 u_1)

The symplectic action functional $\mathcal{A}_H: \mathcal{L}M \to \mathbb{R}$ on a loop space, whose critical points correspond to 1-periodic orbits of the Hamiltonian flow (and hence to fixed points of $\varphi$).

• LoopSpace : Type
• action : self.LoopSpace → ℝ
• CriticalPoint : Type
• critToLoop : self.CriticalPoint → self.LoopSpace
• critEval : self.CriticalPoint → Ω 0 → ℝ
• crit_is_periodic (c : self.CriticalPoint) (g : Ω 0) : self.critEval c (f.φ.pullback g) = self.critEval c g
• critEval_injective : Function.Injective self.critEval

structure ActionFunctionalWithBijection {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (f : HamiltonianDiffeomorphism S) [hnd : IsNondegenerate S f] extends ActionFunctional S f : Type (max 1 u_1)

Bijection between critical points of the action functional and fixed points of $\varphi$: $\mathrm{Crit}(\mathcal{A}_H) \cong \mathrm{Fix}(\varphi)$.

• LoopSpace : Type
• action : self.LoopSpace → ℝ
• CriticalPoint : Type
• critToLoop : self.CriticalPoint → self.LoopSpace
• critEval : self.CriticalPoint → Ω 0 → ℝ
• crit_is_periodic (c : self.CriticalPoint) (g : Ω 0) : self.critEval c (f.φ.pullback g) = self.critEval c g
• critEval_injective : Function.Injective self.critEval
• critToFix : self.CriticalPoint → HasFixedPoints.FixedPoint f
• critToFix_eval (c : self.CriticalPoint) (g : Ω 0) : HasFixedPoints.eval (self.critToFix c) g = self.critEval c g
• fixToCrit : HasFixedPoints.FixedPoint f → self.CriticalPoint
• fixToCrit_eval (x : HasFixedPoints.FixedPoint f) (g : Ω 0) : self.critEval (self.fixToCrit x) g = HasFixedPoints.eval x g

structure FloerComplex {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (f : HamiltonianDiffeomorphism S) [hnd : IsNondegenerate S f] : Type 1

The Floer chain complex $(CF_*, \partial)$ generated by 1-periodic orbits, with differential $\partial^2 = 0$ and total rank equal to $\#\mathrm{Fix}(\varphi)$.

• CF : ℤ → Type
• instAddCommGroup (i : ℤ) : AddCommGroup (self.CF i)
• differential (i : ℤ) : self.CF i →+ self.CF (i + 1)
• d_squared (i : ℤ) (x : self.CF i) : (self.differential (i + 1)) ((self.differential i) x) = 0
• totalRank : ℕ
• totalRank_eq_card : self.totalRank = Fintype.card (HasFixedPoints.FixedPoint f)

class HasFloerHomologyRank {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (f : HamiltonianDiffeomorphism S) [hnd : IsNondegenerate S f] : Type

The graded and total ranks $\dim HF^i$ and $\sum_i \dim HF^i$ of Floer homology.

• floerRank : ℕ → ℕ
• totalFloerRank : ℕ

theorem floer_homology_graded_iso {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hcomp : IsCompactSymplectic Ω VF] (S : SymplecticManifold Ω VF) (f : HamiltonianDiffeomorphism S) [hnd : IsNondegenerate S f] [hbetti : HasBettiNumbers] [hfr : HasFloerHomologyRank S f] (i : ℕ) : HasFloerHomologyRank.floerRank f i = hbetti.betti i

Floer's isomorphism (graded): $HF^i(M, \varphi) \cong H^i(M, \mathbb{R})$ for a Hamiltonian diffeomorphism on a compact symplectic manifold, hence Arnold's lower bound $\#\mathrm{Fix}(\varphi) \ge \sum_i b_i(M)$.

structure FloerComplexGradedRank {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {S : SymplecticManifold Ω VF} {f : HamiltonianDiffeomorphism S} [hnd : IsNondegenerate S f] [hbetti : HasBettiNumbers] (FC : FloerComplex S f) : Type

Graded ranks of the Floer complex: $\dim CF^i$, summing to the total rank and vanishing above the manifold dimension.

• rankCF : ℕ → ℕ
• rankCF_sum : (Finset.range (HasBettiNumbers.manifoldDim Ω VF + 1)).sum self.rankCF = FC.totalRank
• rankCF_vanish (i : ℕ) : HasBettiNumbers.manifoldDim Ω VF < i → self.rankCF i = 0

structure CompactLagrangian {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} [inst_M : DifferentialFormSpace Ω_M VF_M] (S : SymplecticManifold Ω_M VF_M) : Type (max (max u_1 (u_3 + 1)) (u_4 + 1))

A compact Lagrangian submanifold $L \hookrightarrow (M, \omega)$: the pullback of $\omega$ to $L$ vanishes, $\iota^* \omega = 0$.

• Ω_L : ℕ → Type u_3
• VF_L : Type u_4
• inst_L : DifferentialFormSpace self.Ω_L self.VF_L
• inclusion : DFSMorphism self.Ω_L self.VF_L Ω_M VF_M
• lagrangian : self.inclusion.pullback S.ω = 0

class HasLagrangianIntersectionData {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} [inst_M : DifferentialFormSpace Ω_M VF_M] (S : SymplecticManifold Ω_M VF_M) (L : CompactLagrangian S) (ψ : HamiltonianDiffeomorphism S) : Type (u_3 + 1)

Data for the Lagrangian Arnold conjecture: cohomology of $L$, dimension, total Betti number $\sum_i b_i(L) \ge 2$, and the intersection number $\# (L \cap \psi(L))$.

• numIntersections : ℕ
• H_L : ℕ → Type u_3
• H_L_addCommGroup (k : ℕ) : AddCommGroup (H_L L ψ k)
• H_L_module (k : ℕ) : Module ℝ (H_L L ψ k)
• H_L_finiteDimensional (k : ℕ) : FiniteDimensional ℝ (H_L L ψ k)
• lagrangianDim : ℕ
• totalBettiL : ℕ
• totalBettiL_eq : totalBettiL L ψ = ∑ i ∈ Finset.range (lagrangianDim L ψ + 1), Module.finrank ℝ (H_L L ψ i)
• betti_ge_two : totalBettiL L ψ ≥ 2

theorem lagrangian_betti_vanish_above_axiom {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} [inst_M : DifferentialFormSpace Ω_M VF_M] {S : SymplecticManifold Ω_M VF_M} {L : CompactLagrangian S} {ψ : HamiltonianDiffeomorphism S} (hLI : HasLagrangianIntersectionData S L ψ) (i : ℕ) (hi : HasLagrangianIntersectionData.lagrangianDim L ψ < i) : Module.finrank ℝ (HasLagrangianIntersectionData.H_L L ψ i) = 0

Vanishing of Betti numbers of $L$ above its dimension: $b_i(L) = 0$ for $i > \dim L$.

class IsTransverseIntersection {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} [inst_M : DifferentialFormSpace Ω_M VF_M] (S : SymplecticManifold Ω_M VF_M) (L : CompactLagrangian S) (ψ : HamiltonianDiffeomorphism S) : Prop

Transverse intersection of $L$ and $\psi(L)$: the intersection points are non-degenerate, in the sense that a 1-form vanishing on both tangent spaces vanishes identically.

• jointly_spanning (α : Ω_M 1) : L.inclusion.pullback α = 0 → L.inclusion.pullback (ψ.φ.pullback α) = 0 → α = 0

class IsRelativelySpin {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} [inst_M : DifferentialFormSpace Ω_M VF_M] (S : SymplecticManifold Ω_M VF_M) (L : CompactLagrangian S) : Prop

Relative spin condition on $L \subset M$: existence of a closed 2-form $\beta$ on $M$ whose pullback to $L$ is exact, used to orient moduli spaces in Lagrangian Floer theory.

• spin_lift : ∃ (β : Ω_M 2), DifferentialFormSpace.d VF_M β = 0 ∧ ∃ (γ : L.Ω_L 1), L.inclusion.pullback β = DifferentialFormSpace.d L.VF_L γ

class HasH1Injectivity {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} [inst_M : DifferentialFormSpace Ω_M VF_M] (S : SymplecticManifold Ω_M VF_M) (L : CompactLagrangian S) : Prop

$H^1$-injectivity hypothesis: every closed 1-form on $L$ lifts to a closed 1-form on $M$ up to an exact form, ensuring the inclusion $H^1(M) \to H^1(L)$ is surjective on representatives.

• h1_surjective (α : L.Ω_L 1) : DifferentialFormSpace.d L.VF_L α = 0 → ∃ (β : Ω_M 1), DifferentialFormSpace.d VF_M β = 0 ∧ ∃ (γ : L.Ω_L 0), L.inclusion.pullback β = α + DifferentialFormSpace.d L.VF_L γ