Buchumschlag

Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Hulak, David B., Ramos, Arthur F., de Queiroz, Ruy J. G. B.
Format:	Preprint
Veröffentlicht:	2026
Schlagworte:	Logic in Computer Science Differential Geometry
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Synthetic Differential Geometry in Lean
von: Brasca, Riccardo, et al.
Veröffentlicht: (2026)

Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL
von: Hulak, David B., et al.
Veröffentlicht: (2026)

Token-Sensitive Enclosure Semantics for Measurement-Bearing Expressions
von: Hulak, David B., et al.
Veröffentlicht: (2026)

A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4
von: Ramos, Arthur F., et al.
Veröffentlicht: (2026)

Formalizing Singer Sidon Constructions and Sidon Set Infrastructure in Lean 4
von: Hulak, David B., et al.
Veröffentlicht: (2026)

Remarks on the Gluing Theorems for Compact Special Lagrangian Submanifolds with Isolated Conical Singularities
von: Imagi, Yohsuke
Veröffentlicht: (2025)

On smoothness, tangent cones, and the metric geometry of definable sets
von: Rocha, André Gadelha, et al.
Veröffentlicht: (2025)

Formalizing $A_1^{(1)}$ Curve Neighborhoods in Lean 4
von: Huang, Yihe, et al.
Veröffentlicht: (2026)

Higher order differential calculus in mathlib
von: Gouëzel, Sébastien
Veröffentlicht: (2025)

Rigidity in the Positive Mass Theorem with $C^0$ Decay
von: Mazurowski, Liam, et al.
Veröffentlicht: (2026)

Pullback Flow Matching on Data Manifolds
von: de Kruiff, Friso, et al.
Veröffentlicht: (2024)

A Thom Isotopy Theorem for nonproper semialgebraic maps
von: Dias, Luis Renato Gonçalves, et al.
Veröffentlicht: (2024)

Hearing Exotic Smooth Structures
von: Cavenaghi, Leonardo F., et al.
Veröffentlicht: (2024)

Score-based Pullback Riemannian Geometry: Extracting the Data Manifold Geometry using Anisotropic Flows
von: Diepeveen, Willem, et al.
Veröffentlicht: (2024)

Integral Curves and Flows on Banach Manifolds in Lean
von: Yin, Weichen Winston, et al.
Veröffentlicht: (2026)

Obstructions to Smooth Full-Holonomy Cayley Fibrations
von: Majewski, Viktor F., et al.
Veröffentlicht: (2026)

Spectral (0,4)-tensor functionals and the noncommutative residue
von: Li, Hongfeng, et al.
Veröffentlicht: (2025)

A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums
von: Ramos, Arthur, et al.
Veröffentlicht: (2025)

There is no Definable Grauert Direct Image Theorem
von: Esnault, Hélène, et al.
Veröffentlicht: (2026)

Diffeological Smoothness in Hodge Theory
von: Li, Jiayong
Veröffentlicht: (2009)

Singular Lie filtrations and weightings
von: Loizides, Yiannis, et al.
Veröffentlicht: (2022)

Embedded contact homology of the unit cotangent bundle of the Klein bottle
von: Miranda, Marcelo, et al.
Veröffentlicht: (2025)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
von: Qian, Yicheng, et al.
Veröffentlicht: (2025)

On a Class of Singular Complex Manifolds
von: Bahraini, Alireza
Veröffentlicht: (2024)

Remarks on Singular Kähler-Einstein Metrics
von: Hallgren, Max, et al.
Veröffentlicht: (2025)

On the Linearization of Certain Singularities of Nijenhuis Operators
von: Konyaev, Andrey Yu.
Veröffentlicht: (2025)

Singularities of two-dimensional Nijenhuis operators
von: Akpan, Dinmukhammed
Veröffentlicht: (2025)

The Penrose Inequality for Metrics with Singular Sets
von: Zhang, Huaiyu
Veröffentlicht: (2024)

Partial Groupoid Actions on Smooth Manifolds
von: Marín, Víctor, et al.
Veröffentlicht: (2023)

Classification of Smooth Alignable Voss Surfaces
von: Rasoulzadeh, Arvin
Veröffentlicht: (2026)

Area-minimizing Hypersurfaces in Singular Ambient Manifolds
von: Wang, Yihan
Veröffentlicht: (2024)

Singular metrics with nonnegative scalar curvature and RCD
von: Dai, Xianzhe, et al.
Veröffentlicht: (2024)

Mean Curvature Flow from Conical Singularities
von: Chodosh, Otis, et al.
Veröffentlicht: (2023)

The Linearizability of Singular Foliations Is a Morita Invariant
von: Zambon, Marco
Veröffentlicht: (2025)

A Holomorphic Splitting Theorem
von: Song, Miao
Veröffentlicht: (2025)

Extensions of the Bonnet-Myers Theorem
von: Li, Ronggang, et al.
Veröffentlicht: (2025)

Isoperimetric Inequalities on Slabs with applications to Cubes and Gaussian Slabs
von: Milman, Emanuel
Veröffentlicht: (2024)

A Smooth Intrinsic Flat Limit of with Negative Curvature
von: Krandel, Jared, et al.
Veröffentlicht: (2024)

Infinite-Time Singularities of the Lagrangian Mean Curvature Flow
von: Su, Wei-Bo, et al.
Veröffentlicht: (2024)

Singular sets in noncollapsed Ricci flow limit spaces
von: Fang, Hanbing, et al.
Veröffentlicht: (2025)