#!/usr/bin/env python3
"""BS-MIN-01: finite exact demonstration of a continuous algebraic fact.
Python standard library only. The finite run is not a Lean proof or a full
quantified theorem over all real numbers.
"""
from fractions import Fraction as F

def vertices(t):
    t=F(t)
    return ((F(0),F(0),F(0)),(F(1),F(0),F(0)),
            (F(0),F(1),F(0)),(F(1),F(1),t))

def projection(points):
    return tuple((x,y) for x,y,z in points)

def squared_distance(a,b):
    return sum((u-v)**2 for u,v in zip(a,b))

def distances(t):
    p=vertices(t)
    return tuple(squared_distance(p[i],p[j])
                 for i,j in ((0,1),(0,2),(1,2),(0,3),(1,3),(2,3)))

reference=projection(vertices(0))
assert reference==((0,0),(1,0),(0,1),(1,1))
for t in range(-3,4):
    assert projection(vertices(t))==reference
    assert distances(t)==(1,1,2,2+t*t,1+t*t,1+t*t)
    assert distances(t)==distances(-t)
assert vertices(1)!=vertices(-1)
assert distances(1)==distances(-1)==(1,1,2,3,2,2)
assert F(1)**2==F(-1)**2
# Signed oriented tetrahedral volume is determinant/6 = t/6.
assert F(1,6)!=F(-1,6)
assert squared_distance(vertices(1)[3],(1,1,1))==0
assert squared_distance(vertices(-1)[3],(1,1,1))==4
print("BS-MIN-01 sample checks PASS: projection invariance, squared distances,")
print("mirror ambiguity, signed orientation, off-plane anchor discrimination")
print("Sample domain: exact rational t values -3 to +3")
print("Limit: finite executable check; algebraic reasoning required for all real t")