What was already known
The published planar upper bound was 0.7. The cited earlier metric-space bound was about 0.72655.
AI involvement
Yongxi Lin set the target and supplied and checked certificate material. ChatGPT project sessions developed the six-point analysis, finite constant and Gram-certificate proof; Claude Code later formalized it.
The disclosure attributes the central six-point argument and retained rational certificates to ChatGPT sessions, with Lin setting the problem and controlling the final proof artifact.
Importance
Improves the planar threshold and gives the same upper bound for all real Hilbert spaces.
Limitations
This bounds the threshold infimum; it does not prove that 0.6934 itself forces rectifiability or settle the conjectured value 1/2. The repository reports exact checks of thirty Gram certificates and a Lean proof; no external human proof check is documented.
Technical verification
The source reports a complete Lean proof of the Hilbert-space and planar bounds with exact rational recomputation of all thirty Gram certificates and permitted-axiom/statement audits. Independent external human review is absent.
Formal checking
Repository reports complete Lean proof, exact rational recomputation of thirty certificates and axiom audit.
- Checker
- Lean 4 kernel and exact-rational certificate verifier
- Scope
- Besicovitch.sigma_one_le_6934_div_10000 and planar specialization
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The extensive proof notes and six-point account are model-generated; no named human explanation of the central Gram-certificate mechanism is documented. Few is the evidence-gap default, not a finding that Lin cannot understand it.
Correction and publication history
The reported Lean theorem and rational certificates support the stated 0.6934 threshold bound.
Read this published revision