Skip to content

High-dimensional APPT endpoints — Lean verification v1

Choose a tag to compare

View all tags
@mxym mxym released this 12 Oct 01:02
· 717 commits to main since this release
Immutable release. Only release title and notes can be modified.
appt-high-dimensional-endpoints-lean-v1
fe1527c

This immutable release records two additional kernel-checked endpoints for the high-dimensional APPT purity program.

Verified theorems:

  • APPTReview.appt_fixed_local_excess_sup_tendsto: for every fixed integer m >= 2, the physical APPT purity supremum satisfies
    Tendsto (fun n => (m*n) * (P_sup(m,n) - 1/(m*n))) atTop (nhds (1/(m^2-1))).
  • APPTReview.plateauScaledPurity_le_continuous: every two-level projection plateau lies below the continuous two-level value, with an exact square-deficit identity.
  • APPTReview.plateauScaledPurity_even_rank_max: when (m-1)*n is even, rank ((m-1)*n)/2 attains that value and is maximal within the plateau family.

Verification:

  • Lean 4.34.1 and the pinned Mathlib revision.
  • lake build APPTReview completed 2,850 jobs.
  • Direct compilation of APPTReview/PlateauOptimizer.lean passed.
  • Kernel axiom checks for all three theorem roots use only propext, Classical.choice, and Quot.sound.

Scope: these endpoints strengthen the fixed-local and two-level plateau portions of the program. They do not claim the full higher-dimensional APPT purity maximum, matching growing-local-dimension lower bounds, all-maximizer classification, entropy extrema, or rigidity.

Assets 3
Loading