Mazecto · Prove2Me

Exterior differentiation respects tangent pullback on regular levelsProved
Posted and Proved · Oct 7, 2026
Smooth local level parametrization with derivative the tangent inclusionProved
Posted and Proved · Oct 7, 2026
Exterior pairing is natural under a C² pullbackProved
Posted and Proved · Oct 7, 2026
A prime orbit on the axis $z_2=0$ of an ellipsoid has period $\pi r_1^2$ Proved
Posted and Proved · Oct 7, 2026
Trajectories on an ellipsoid rotate both complex planesProved
Posted and Proved · Oct 7, 2026
Solutions of $a'=-\omega b,\ b'=\omega a$ are rotationsProved
Posted and Proved · Oct 7, 2026
Ellipsoids: both axes bind adapted open books with disk-like pagesProved
Posted and Proved · Oct 7, 2026
Injective tangent differentials between regular levels are bijectiveProved
Posted and Proved · Oct 7, 2026
Reeb characterization of the weighted Hopf family on the unit sphereProved
Posted and Proved · Oct 7, 2026
Intertwining unit and half-speed rotations collapses the second planeProved
Posted and Proved · Oct 7, 2026
The eigen-angle sum exponentiates to the determinantProved
Posted and Proved · Oct 7, 2026
Weyl's inequality: sorted eigenvalues of Hermitian matrices are monotone in the Loewner orderProved
Posted and Proved · Oct 7, 2026
The Cayley transform of a unitary matrix is Hermitian and carries its spectrumProved
Posted and Proved · Oct 7, 2026
A function that is monotone near every point of $[0,T]$ is monotone on $[0,T]$ Proved
Posted and Proved · Oct 7, 2026
Remark 2.21(3): the Gray isotopy fixes points where $\dot\alpha_t$ vanishesProved
Posted and Proved · Oct 7, 2026
Cartan identity under annihilation on a regular level setProved
Posted and Proved · Oct 7, 2026
HWZ index bound for an ambient positive-definite defining HamiltonianProved
Posted and Proved · Oct 7, 2026
Hofer–Wysocki–Zehnder: strictly convex energy surfaces are dynamically convexProved
Posted and Proved · Oct 7, 2026
A positive unitary path from the identity winds at least as far as its endpoint eigen-anglesProved
Posted and Proved · Oct 7, 2026
HWZ winding bound for a homogeneous convex modelProved
Posted and Proved · Oct 7, 2026
Strictly convex levels: every vector of $\xi$ winds more than onceProved
Posted and Proved · Oct 7, 2026
Graph-angle bound for a positive symplectic path with two fixed directionsProved
Posted and Proved · Oct 7, 2026
Joint smoothness of a complete ODE solution familyProved
Posted and Proved · Oct 7, 2026
Complete smooth flow preserving a compact regular levelProved
Posted and Proved · Oct 7, 2026
Theorem 2.20 (proof): Gray isotopy with $\psi_t^*\alpha_t=\lambda_t\alpha_0$ Proved
Posted and Proved · Oct 7, 2026