Positive CurvatureOPEN VERIFICATION

SAGEMATH VERIFICATION COMPANION

Positive curvature.
Visible evidence.

An open, reproducible computational companion to “Positive curvature on all smooth 7-spheres”. Read the checks. Inspect the certificates. Know exactly what they establish.

Explore the checks Get the complete package
v12Loading release record…Exact algebra + rigorous interval bounds
TWO FILLINGS. ONE GEOMETRIC INTERFACE.
Two-cap construction schematic An abstract wireframe of a northern and a southern cap meeting at a common boundary. This is a schematic, not a computed metric or curvature plot. DNDS BOUNDARY MATCHING + SMOOTH GLUING
Northern fillingSouthern fillingSchematic, not a curvature plot
THE RECORDED RUN

Results you can
inspect and replay.

—passed check groups
—exact certificates
—unformalized dependency groups
—failed checks

01 / UNDERSTAND THE SCOPE

Exact about the mathematics.
Honest about the limits.

What this package checks

Symbolic curvature identities, decomposable-plane algebra, coefficient bounds and boundary formulas, plus directed-rounding checks of specified scalar inequalities. Exported polynomial certificates can be replayed independently with exact rational arithmetic; interval checks require Sage.

A PASS belongs to its stated check—not automatically to the full theorem.

What a passing run does not prove

The global theorem is not machine-certified end to end. Smooth topology, geometric interpretation, uniform analytic estimates and external theorems still require mathematical arguments. This is not a Lean formalization.

Unverified by this computation does not mean false; it means outside its certified scope.

Where computation meets the proof

The companion checks selected steps in a larger geometric argument.

  1. 01Smooth typeClutching and classificationGeometry + external results
  2. 02Southern fillingConnection curvatureExact algebra + analysis
  3. 03Northern fillingWarping and horizontal planesExact algebra + analysis
  4. 04Boundary matchingMetric and second fundamental formExact algebra + analysis
  5. 05Smooth gluingGlobal positive curvatureAnalytic + external results

02 / FOLLOW THE MATHEMATICS

A map of the verification.

Each module has a specific claim, a reproducible calculation, and a visible boundary of responsibility.

Module records are loading.

03 / INSPECT THE RECORD

Every check, out in the open.

Search the recorded claims and expand any row to inspect its evidence. Counts refer to check groups, not sampled planes.

Recorded exact checks and explicit unverified dependencies
StatusCheck & claimModuleEvidence
Loading the reproducibility record…

Check identifiers and mathematical claims are preserved verbatim from the machine-readable release record.

04 / TAKE THE EVIDENCE WITH YOU

Open files. Clear provenance.

The release brings together the code, manuscript, exact certificates, raw execution records and two detailed reading guides.

ZIP

The complete
verification package.

Everything needed to inspect and reproduce this release. Includes the submitted source, verification code, certificates, logs and both explanatory reports.

Download the release
PDF · ENGLISH

The verification, explained.

A detailed guide to the mathematics, certificates, assumptions and actual scope of the package.
PDF · 中文

计算验证，逐层解读。

中文完整解读：检查了什么、如何复现，以及哪些结论仍然需要数学证明。
TEXSubmitted manuscript JSONMachine-readable results DATAExact certificates

05 / REPRODUCE THE RUN

Don’t take a
green badge on faith.

Download and extract the package, then run the checks yourself. These commands start in the extracted package directory. The archived reference run stays separate from your new results.

SageMath —recorded runtime

With SageMath available in your terminal:
sh reproduce.sh

TRACEABLE TO THE SOURCE

One manuscript. An identifiable release.

The source fingerprint links this computational record to the exact submitted LaTeX file. A hash identifies bytes; it does not certify a theorem.

SHA-256 · v12_clean.tex
Waiting for the release fingerprint…