/-
BS-MIN-01 / Formal demonstrator A
Scope: a product-coordinate projection erases the third coordinate,
so two configurations can have identical shadows despite differing height.
Parametric theorem: valid for any coordinate type alpha.
Concrete non-injectivity witness: distinct Int triples.
This is NOT an ONAR9 theorem, physical experiment, or full distance-rigidity result.
Toolchain: leanprover/lean4:v4.33.0-rc1, Lean core only.
-/
import Init

namespace BSMin01

abbrev Point3 (α : Type) := α × α × α

def projection {α : Type} (p : Point3 α) : α × α :=
  (p.1, p.2.1)

def point (α : Type) (x y t : α) : Point3 α :=
  (x, y, t)

theorem projection_ignores_height
    {α : Type} (x y t u : α) :
    projection (point α x y t) =
    projection (point α x y u) := by
  rfl

theorem projection_value
    {α : Type} (x y t : α) :
    projection (point α x y t) = (x, y) := by
  rfl

theorem distinct_integer_points_same_projection :
    point Int 0 0 0 ≠ point Int 0 0 1 ∧
    projection (point Int 0 0 0) = projection (point Int 0 0 1) := by
  constructor
  · decide
  · rfl

#print axioms projection_ignores_height
#print axioms projection_value
#print axioms distinct_integer_points_same_projection

end BSMin01