Exact P1 forest N30A

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/N30A.accepted

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/N30A.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/N30A.accepted
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N30APart00
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N30APart01
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N30APart02
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Nodes/N30A
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Traversal/N30AWalk