Issues

• g6_unconditional_closure: exists m <= 33, crystal saturated and eigenmode locked

  TOTOGT/AXLE#48 · Filter by author TOTOGT opened on Oct 1, 2026

• Regularity-free closurePoints_stationary (the stated goal of #6) is false when cof alpha = omega

  TOTOGT/AXLE#47 · Filter by author TOTOGT opened on Oct 1, 2026

• closurePoints_stationary: lean/Main.lean and AXLE_v8_1.lean state it with a false hypothesis

  TOTOGT/AXLE#46 · Filter by author TOTOGT opened on Oct 1, 2026

• P_ON (correctOrder drv) > 0: discretisation bound

  TOTOGT/AXLE#45 · Filter by author TOTOGT opened on Oct 1, 2026

• p-adic local coefficient definition

  TOTOGT/AXLE#44 · Filter by author TOTOGT opened on Oct 1, 2026

• Critical line as contact symmetry locus: digamma cancellation

  TOTOGT/AXLE#43 · Filter by author TOTOGT opened on Oct 1, 2026

• g_arith: connect to Mathlib vonMangoldt

  TOTOGT/AXLE#42 · Filter by author TOTOGT opened on Oct 1, 2026

• No homotopy between gamma_K and gamma_F: formal statement

  TOTOGT/AXLE#41 · Filter by author TOTOGT opened on Oct 1, 2026

• P_ON (wrongOrder drv) = 0: formal statement for the wrong operator order

  TOTOGT/AXLE#40 · Filter by author TOTOGT opened on Oct 1, 2026

• Matrix.minnorm missing from Mathlib: blocks Proof 6 / Chapter 5 zero-sorry

  TOTOGT/AXLE#39 · Filter by author TOTOGT opened on Oct 1, 2026

• jackknife_correspondence: contact diffeomorphism tractor-trailer to LAW3M

  TOTOGT/AXLE#38 · Filter by author TOTOGT opened on Oct 1, 2026

• inner_basin_escape: obstruction to inner-basin escape (null-causality route)

  TOTOGT/AXLE#37 · Filter by author TOTOGT opened on Oct 1, 2026

• Outer basin: convergence domain (z(0) hypothesis) for the helical attractor

  TOTOGT/AXLE#36 · Filter by author TOTOGT opened on Oct 1, 2026

• kappa_lipschitz: Lipschitz bound on the dm3 coupling term

  TOTOGT/AXLE#35 · Filter by author TOTOGT opened on Oct 1, 2026

• Linear independence of {log p} over ℚ and non-integrability of α_arith (elementary, by unique factorisation; not Baker)

  TOTOGT/AXLE#34 · Filter by author TOTOGT opened on Sep 15, 2026

• State the Global Positivity Theorem as a Lean proposition

  TOTOGT/AXLE#33 · Filter by author TOTOGT opened on Sep 15, 2026

• O7 — the asymmetric inner boundary against the symmetric Gronwall bound

  TOTOGT/AXLE#32 · Filter by author TOTOGT opened on Sep 15, 2026

• Kernel dimension from contact topology

  TOTOGT/AXLE#31 · Filter by author TOTOGT opened on Sep 15, 2026

• LCH construction for Legendrian action positivity

  TOTOGT/AXLE#30 · Filter by author TOTOGT opened on Sep 15, 2026

• Spectral measure of the transfer operator at a Whitney fold

  TOTOGT/AXLE#29 · Filter by author TOTOGT opened on Sep 15, 2026

• IPR_trib > IPR_fib — formal bound

  TOTOGT/AXLE#28 · Filter by author TOTOGT opened on Sep 15, 2026

• Floquet multipliers for the spiral return map

  TOTOGT/AXLE#27 · Filter by author TOTOGT opened on Sep 15, 2026

• Regeneration loop invariant after g6 cycles — transfinite case

  TOTOGT/AXLE#26 · Filter by author TOTOGT opened on Sep 15, 2026

• Update code

  TOTOGT/AXLE#15 · Filter by author TOTOGT opened on May 24, 2026
  1

• O3: Theorem T1 — full ODE Gronwall integration (z(t) monotonicity)

  TOTOGT/AXLE#14 · Filter by author TOTOGT opened on May 21, 2026