Exact P1 forest N25B

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

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/N25B.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/N25B.accepted
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N25BPart00
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N25BPart01
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N25BPart02
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Checks/N25BPart03
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Nodes/N25B
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/P1Data/Traversal/N25BWalk