Exact P1 forest N25A

Abstract

Exact structural traversal and local numerical premises of the same full scalar reduction.

Theorem 1.1 (Exact forest premise accepted).

Lean statement: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/N25A.accepted

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/N25A.accepted (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact rational or structural premise is used in the complete forest check, which supplies the continuous real scalar inequality.

References

• Truth anchor: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/N25A.accepted
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N25APart00
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N25APart01
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N25APart02
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N25APart03
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N25APart04
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N25APart05
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N25APart06
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N25APart07
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N25APart08
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N25APart09
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Nodes/N25A
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Traversal/N25AWalk