Establish complex-coordinate and projective semantics

COMPLEX-PROJECTIVE.md

@@ -0,0 +1,61 @@
+# Complex and projective semantic boundary
+
+This slice establishes the type-level distinction needed by complex and projective arithmetic without choosing a machine representation or silently settling the separate floating-precision work.
+
+## What the checker now distinguishes
+
+`ComplexCoordinates complex n` is the structural type of an element of a complex coordinate space with exactly `n` coordinates. `ComplexProjectivePoint complex n` is a projective point with a nonzero homogeneous representative containing exactly `n + 1` complex coordinates.
+
+The `complex` parameter is deliberate. The current canonical tree does not yet have a settled general real-scalar hierarchy whose precision semantics can honestly define the numerical carrier for the mathematical field C. This module therefore does **not** define C as two `Double`s, two `Float32`s, a GLSL `vec2`, or an x86 register pair merely to obtain executable code.
+
+The concrete executable Float32 implementation currently belongs to the x86-64 leading backend and is checked against the shared corpus at `_/fixtures/complex-projective/float32.json`. The exact `ExactComplex` type in `QuadraticForms.idric` remains a Gaussian-integral test scalar used only to make structural identities reduce exactly in compiler acceptance.
+
+## Projective semantics
+
+For projective dimension `n`, a representative has `n + 1` homogeneous coordinates. The all-zero tuple is excluded by `NonzeroHomogeneousCoordinates`.
+
+The runtime representation may carry a homogeneous tuple directly. The semantic point is the equivalence class under common nonzero complex rescaling:
+
+```text
+[z0:...:zn] = [lambda z0:...:lambda zn],  lambda != 0.
+```
+
+`projective_rescaling_witness` expresses one explicit witness for that quotient relation. Raw component equality is not projective equality. There is intentionally no ordinary `Eq` instance, vector addition, or multiplication for `ComplexProjectivePoint`.
+
+Normalization is not part of construction. A backend may choose a gauge for numerical stability, chart extraction, comparison, serialization, or rendering, but common scale is otherwise retained as redundant homogeneous information.
+
+## Affine chart
+
+`affine_to_projective` implements
+
+```text
+(z1,...,zn) -> [1:z1:...:zn].
+```
+
+`projective_first_chart` divides by the first homogeneous coordinate only when that coordinate is nonzero. For CP^1, `[0:1]` therefore remains the point at infinity and is outside this chart.
+
+## Holomorphic boundary
+
+Projective structure does not make observational operations holomorphic. Conjugation, magnitude, phase, gauge choice, and coloring may be used for observation or rendering. They must not be inserted into an evolving value that is meant to remain holomorphic.
+
+The shared render fixture uses the current whole-plane explorer model
+
+```text
+f(z) = R(z) exp(q(z))
+```
+
+where `R` carries an explicit zero/pole divisor and `q` is an entire polynomial. The fixture contains no lasso, overlapping-disc, path, Riemann-surface, or lacunary machinery.
+
+## Precision and tolerances
+
+The shared numerical corpus declares Float32 explicitly. Its machine implementations must preserve that declared width. A wider host calculation may be used only as an external oracle.
+
+Exact-binary32 cases use exact comparison. Ordinary floating cases use an error bound derived from binary32 epsilon and the conditioning/operation count of the case. The current bounded complex-exponential implementation is a degree-7 Taylor polynomial and is accepted only for input magnitude at most `0.5`; its analytic truncation bound is
+
+```text
+exp(|q|) |q|^8 / 8!
+```
+
+plus a separately recorded binary32 rounding allowance. Inputs outside the declared approximation domain must be rejected rather than silently accepted with a larger arbitrary tolerance.
+
+Projective comparison uses rescaling witnesses or invariant cross-products such as `zi*wj - zj*wi`, never raw homogeneous component equality.

_/examples/unified-higher-mathematics/ComplexProjective.idric

@@ -0,0 +1,188 @@
+module ComplexProjective
+
+import MathematicalSpaces
+
+%unbound_implicits off
+
+-- Complex arithmetic and machine representation are separate questions.
+-- This module establishes the structural types needed by the checker without
+-- choosing Float16, Float32, Cartesian machine pairs, SIMD lanes, or a backend
+-- ABI.  The `complex` parameter is the scalar carrier supplied by a concrete
+-- complex-arithmetic implementation.  In the exact acceptance test it is the
+-- Gaussian-integral ExactComplex fixture from QuadraticForms; that fixture is
+-- not the definition of the mathematical complex numbers.
+
+-- An element of C^n has n complex coordinates.  Dimension is part of the type,
+-- so a C^2 value cannot be consumed where C^3 is required.
+public export
+data ComplexCoordinates : Type → CoordinateRank → Type where
+  NoComplexCoordinates :
+    {complex : Type} →
+    ComplexCoordinates complex Z
+  ComplexCoordinate :
+    {complex : Type} →
+    {remaining : CoordinateRank} →
+    complex →
+    ComplexCoordinates complex remaining →
+    ComplexCoordinates complex (S remaining)
+
+export
+map_complex_coordinates :
+  {source : Type} →
+  {target : Type} →
+  {dimension : CoordinateRank} →
+  (map_coordinate : source → target) →
+  ComplexCoordinates source dimension →
+  ComplexCoordinates target dimension
+map_complex_coordinates map_coordinate NoComplexCoordinates =
+  NoComplexCoordinates
+map_complex_coordinates
+  map_coordinate
+  (ComplexCoordinate coordinate remaining) =
+    ComplexCoordinate
+      (map_coordinate coordinate)
+      (map_complex_coordinates map_coordinate remaining)
+
+public export
+scale_complex_coordinates :
+  {complex : Type} →
+  {dimension : CoordinateRank} →
+  (multiply_complex : complex → complex → complex) →
+  complex →
+  ComplexCoordinates complex dimension →
+  ComplexCoordinates complex dimension
+scale_complex_coordinates
+  multiply_complex
+  scalar
+  NoComplexCoordinates = NoComplexCoordinates
+scale_complex_coordinates
+  multiply_complex
+  scalar
+  (ComplexCoordinate coordinate remaining) =
+    ComplexCoordinate
+      (multiply_complex scalar coordinate)
+      (scale_complex_coordinates multiply_complex scalar remaining)
+
+-- The constructor is explicitly unsafe because this module does not invent a
+-- fake generic proof that an arbitrary complex carrier can decide nonzeroness.
+-- Concrete complex arithmetic should expose checked constructors appropriate
+-- to its scalar semantics.
+public export
+record NonzeroComplexScalar (complex : Type) where
+  constructor UnsafeKnownNonzeroComplexScalar
+  nonzero_complex_value : complex
+
+-- CP^n uses n+1 homogeneous complex coordinates, with the all-zero tuple
+-- excluded.  The witness constructor is unsafe for the same reason as above:
+-- nonzeroness belongs to the concrete complex carrier, not to this structural
+-- module.
+public export
+record NonzeroHomogeneousCoordinates
+    (complex : Type)
+    (projective_dimension : CoordinateRank) where
+  constructor UnsafeKnownNonzeroHomogeneousCoordinates
+  homogeneous_coordinates :
+    ComplexCoordinates complex (S projective_dimension)
+
+-- A projective point carries a homogeneous representative but has quotient
+-- semantics.  There is deliberately no Eq instance and no vector addition or
+-- multiplication on this type.  Common nonzero complex rescaling is expressed
+-- by the witness type below.
+public export
+data ComplexProjectivePoint : Type → CoordinateRank → Type where
+  UnsafeProjectiveClass :
+    {complex : Type} →
+    {projective_dimension : CoordinateRank} →
+    NonzeroHomogeneousCoordinates complex projective_dimension →
+    ComplexProjectivePoint complex projective_dimension
+
+export
+homogeneous_representative :
+  {complex : Type} →
+  {projective_dimension : CoordinateRank} →
+  ComplexProjectivePoint complex projective_dimension →
+  NonzeroHomogeneousCoordinates complex projective_dimension
+homogeneous_representative (UnsafeProjectiveClass representative) =
+  representative
+
+-- For a chosen nonzero lambda this type is inhabited exactly when
+--
+--   lambda * left = right
+--
+-- coordinate by coordinate.  Projective equivalence is the existence of such
+-- a nonzero lambda.  Keeping the scale as explicit evidence prevents raw
+-- component equality from being mistaken for equality in CP^n.
+public export
+projective_rescaling_witness :
+  {complex : Type} →
+  {projective_dimension : CoordinateRank} →
+  (multiply_complex : complex → complex → complex) →
+  (scale : NonzeroComplexScalar complex) →
+  (left : NonzeroHomogeneousCoordinates complex projective_dimension) →
+  (right : NonzeroHomogeneousCoordinates complex projective_dimension) →
+  Type
+projective_rescaling_witness
+  multiply_complex
+  (UnsafeKnownNonzeroComplexScalar scalar)
+  (UnsafeKnownNonzeroHomogeneousCoordinates left)
+  (UnsafeKnownNonzeroHomogeneousCoordinates right) =
+    scale_complex_coordinates multiply_complex scalar left = right
+
+-- (z1,...,zn) maps to [1:z1:...:zn].  The first homogeneous coordinate is
+-- supplied as a known-nonzero complex scalar rather than inferred from a
+-- machine representation.
+public export
+affine_to_projective :
+  {complex : Type} →
+  {projective_dimension : CoordinateRank} →
+  NonzeroComplexScalar complex →
+  ComplexCoordinates complex projective_dimension →
+  ComplexProjectivePoint complex projective_dimension
+affine_to_projective
+  one
+  affine_coordinates =
+    UnsafeProjectiveClass $
+      UnsafeKnownNonzeroHomogeneousCoordinates $
+        ComplexCoordinate
+          (nonzero_complex_value one)
+          affine_coordinates
+
+public export
+divide_coordinates_by :
+  {complex : Type} →
+  {dimension : CoordinateRank} →
+  (divide_complex : complex → complex → complex) →
+  complex →
+  ComplexCoordinates complex dimension →
+  ComplexCoordinates complex dimension
+divide_coordinates_by divide_complex denominator NoComplexCoordinates =
+  NoComplexCoordinates
+divide_coordinates_by
+  divide_complex
+  denominator
+  (ComplexCoordinate coordinate remaining) =
+    ComplexCoordinate
+      (divide_complex coordinate denominator)
+      (divide_coordinates_by divide_complex denominator remaining)
+
+-- Extract the affine chart with first homogeneous coordinate nonzero.  The
+-- operation is partial: [0:z1:...:zn] is outside this chart.  In particular,
+-- [0:1] in CP^1 is the point at infinity and returns Nothing here.
+public export
+projective_first_chart :
+  {complex : Type} →
+  {projective_dimension : CoordinateRank} →
+  (is_zero_complex : complex → Bool) →
+  (divide_complex : complex → complex → complex) →
+  ComplexProjectivePoint complex projective_dimension →
+  Maybe (ComplexCoordinates complex projective_dimension)
+projective_first_chart
+  is_zero_complex
+  divide_complex
+  (UnsafeProjectiveClass
+    (UnsafeKnownNonzeroHomogeneousCoordinates
+      (ComplexCoordinate first remaining))) =
+        if is_zero_complex first
+          then Nothing
+          else Just $
+            divide_coordinates_by divide_complex first remaining

_/examples/unified-higher-mathematics/ComplexProjectiveTests.idric

@@ -0,0 +1,116 @@
+module ComplexProjectiveTests
+
+import MathematicalSpaces
+import QuadraticForms
+import ComplexProjective
+
+%unbound_implicits off
+
+-- ExactComplex is used only as an exact algebraic fixture for the structural
+-- complex/projective API.  It remains the Gaussian-integral acceptance scalar
+-- defined in QuadraticForms, not the future general complex-number carrier.
+
+cp2_left : NonzeroHomogeneousCoordinates ExactComplex 2
+cp2_left =
+  UnsafeKnownNonzeroHomogeneousCoordinates $
+    ComplexCoordinate complex_one $
+      ComplexCoordinate complex_i $
+        ComplexCoordinate (Complex 2 0) NoComplexCoordinates
+
+cp2_scaled_by_two : NonzeroHomogeneousCoordinates ExactComplex 2
+cp2_scaled_by_two =
+  UnsafeKnownNonzeroHomogeneousCoordinates $
+    ComplexCoordinate (Complex 2 0) $
+      ComplexCoordinate (Complex 0 2) $
+        ComplexCoordinate (Complex 4 0) NoComplexCoordinates
+
+cp2_scale_two : NonzeroComplexScalar ExactComplex
+cp2_scale_two = UnsafeKnownNonzeroComplexScalar (Complex 2 0)
+
+cp2_real_rescaling_test :
+  projective_rescaling_witness
+    complex_multiply
+    cp2_scale_two
+    cp2_left
+    cp2_scaled_by_two
+cp2_real_rescaling_test = Refl
+
+cp2_scaled_by_i : NonzeroHomogeneousCoordinates ExactComplex 2
+cp2_scaled_by_i =
+  UnsafeKnownNonzeroHomogeneousCoordinates $
+    ComplexCoordinate complex_i $
+      ComplexCoordinate (Complex (-1) 0) $
+        ComplexCoordinate (Complex 0 2) NoComplexCoordinates
+
+cp2_scale_i : NonzeroComplexScalar ExactComplex
+cp2_scale_i = UnsafeKnownNonzeroComplexScalar complex_i
+
+cp2_phase_rescaling_test :
+  projective_rescaling_witness
+    complex_multiply
+    cp2_scale_i
+    cp2_left
+    cp2_scaled_by_i
+cp2_phase_rescaling_test = Refl
+
+affine_value : ComplexCoordinates ExactComplex 1
+affine_value =
+  ComplexCoordinate (Complex 3 (-2)) NoComplexCoordinates
+
+exact_complex_is_zero : ExactComplex → Bool
+exact_complex_is_zero (Complex 0 0) = True
+exact_complex_is_zero _ = False
+
+-- The affine embedding fixes the first homogeneous coordinate to 1, so this
+-- exact fixture only needs division by that unit.  It is intentionally not
+-- advertised as Gaussian-integer division.
+exact_divide_by_embedding_unit : ExactComplex → ExactComplex → ExactComplex
+exact_divide_by_embedding_unit numerator (Complex 1 0) = numerator
+exact_divide_by_embedding_unit numerator _ = numerator
+
+affine_embedding : ComplexProjectivePoint ExactComplex 1
+affine_embedding =
+  affine_to_projective
+    (UnsafeKnownNonzeroComplexScalar complex_one)
+    affine_value
+
+affine_chart_round_trip_test :
+  projective_first_chart
+    exact_complex_is_zero
+    exact_divide_by_embedding_unit
+    affine_embedding = Just affine_value
+affine_chart_round_trip_test = Refl
+
+cp1_infinity : ComplexProjectivePoint ExactComplex 1
+cp1_infinity =
+  UnsafeProjectiveClass $
+    UnsafeKnownNonzeroHomogeneousCoordinates $
+      ComplexCoordinate complex_zero $
+        ComplexCoordinate complex_one NoComplexCoordinates
+
+cp1_infinity_not_in_first_chart_test :
+  projective_first_chart
+    exact_complex_is_zero
+    exact_divide_by_embedding_unit
+    cp1_infinity = Nothing
+cp1_infinity_not_in_first_chart_test = Refl
+
+-- Dimension is carried by the result type itself.  Keep this acceptance
+-- diagnostic-independent: the constructors below inhabit C^2 exactly, while a
+-- C^3 consumer cannot accept this value without a type error.
+complex_dimension_two_value : ComplexCoordinates ExactComplex 2
+complex_dimension_two_value =
+  ComplexCoordinate complex_one $
+    ComplexCoordinate complex_i NoComplexCoordinates
+
+complex_dimension_two_identity :
+  ComplexCoordinates ExactComplex 2 → ComplexCoordinates ExactComplex 2
+complex_dimension_two_identity coordinates = coordinates
+
+complex_dimension_index_test :
+  complex_dimension_two_identity complex_dimension_two_value =
+    complex_dimension_two_value
+complex_dimension_index_test = Refl
+
+main : IO ()
+main = putStrLn "complex/projective structural semantics: PASS"