Construction Algorithm

Given a finite linear space, the Constructibility Theorem proves that there exists a set of isomorphic linear surfaces. However, the Constructibility Theorem does not provide an algorithm for producing sample isomorphic linear surfaces. Here I will present such an algorithm. The input to the algorithm is a set of linear surfaces B in a space of dimension n, and a set of regions R isomorphic to a linear section. The output is a linear surface dividing the regions in R. Choose a linear surface b₀ and n noncoincidental points p₀, p₁, ... p_n-1 on b₀. Let f map each linear surface b to a point p with coordinates equal to the lengths of the segments perpendicular to b₀ from b to p₀, p₁, ... p_n-1. I claim that f maps linear surfaces through the same point to points on a linear surface. Thus f determines mapping g from points to linear surfaces. Since b₀ provides an orientation, two linear surfaces can be opposite or on the same side of a point. Let Q be the intersection points of each n-tuple from B, and D be the linear surfaces mapped to from Q by g. D forms a finite linear space with regions corresponding to sections in B. To find a linear surface dividing the regions in R, find which side of R each point in Q is on. Use those sidednesses to determine a region x in D. Choose a point y in x. Apply the inverse of f to y to obtain a linear surface dividing the regions in R.

I must prove that the map g from point to linear surface is well defined.

Consider a linear surface b through point p that f maps to coordinates c₀, c₁, ... c_n-1. Since b goes through p, one coordinate c_i depends on the other coordinates. If every coordinate except c_i and one other c_j is held fixed, then by similar triangles, c_i = dc_j + e, for some scalars d and e. Thus, the dependence of c_i upon the other coordinates is the affine composition of affine functions. Therefore, the coordinates lie on a linear surface.

Implications of this algorithm for abstract linear spaces include that every linear space of the same number of boundaries has the same number of sections, and that the notion of sidedness of n-tuples of boundaries wrt boundaries is well defined.

Section Space Theorem

If space S₀ⁿ is linear, then there exists linear space S₁ⁿ, unique up to isomorphism, with boundaries corresponding to n-tuples of boundaries from S₀ⁿ and regions corresponding to sections of S₀ⁿ.

The proof follows from the algorithm above.

Procedural Proof

The proof of the Independent Boundary Theorem in a previous post is incorrect because I failed to establish an isomorphism before applying the Antisection Theorem. To make the Independent Boundary Theorem proof more precise, I will present it as a method called extend in a class called Space. Other methods left undefined are the linear function that returns whether the given Space is linear, section and antisection that work like the Section Theorem and Antisection Theorem, and the take function. The take function converts regions from one Space to regions on the same side of shared boundaries in another Space. If both the containing Space and the given Space have the same boundaries, then take finds isomorphic regions; otherwise, take finds super-regions or sub-regions.
Space Space::extend(
  const Space &S0,
  const Space &S1,
  const int b0,
  const int b1) const {
  assert(linear());
  assert(S0.linear());
  assert(S1.linear());
  assert(boundaries()==S0.boundaries());
  assert(boundaries()==S1.boundaries());
  assert(dimension()==S0.dimension()+1);
  assert(dimension()==S1.dimension()+1);
  assert(take(S0.regions(),S0).size()==S0.regions().size());
  assert(take(S1.regions(),S1).size()==S1.regions().size());
  assert(!boundaries().contains(b0));
  assert(!boundaries().contains(b1));
  Space S2 = antisection(take(S0.regions(),S0),b0); // n2=n
  if (dimension()==1) {
    return S2.antisection(S2.take(S1.regions(),S1).choose(),b1);}
  Space S3 = subsection(S0,S1); // n3=n-1+n-1-n=n-2
  Space S4 = S1.antisection(S1.take(S3.regions(),S3),b0); // n4=n-1
  Space S5 = S2.antisection(S2.take(S4.regions(),S4),b1); // n5=n
  set<int> B0 = S5.boundaries().erase(b1);
  set<int> B1 = S5.boundaries().erase(b0);
  assert(S5.subspace(B0)==antisection(take(S0.regions(),S0),b0));
  assert(S5.subspace(B1)==antisection(take(S1.regions(),S1),b1));
  assert(S5.linear());
  return S5;}
Space Space::subsection(
  const Space &S0,
  const Space &S1) const {
  assert(linear());
  assert(S0.linear());
  assert(S1.linear()):
  assert(boundaries()==S0.boundaries());
  assert(boundaries()==S1.boundaries());
  int n = dimension();
  int n0 = S0.dimension();
  int n1 = S1.dimension();
  assert(n0+n1-n>=0);
  if (boundaries().size()==0) {
    return Space(n0+n1-n);}
  int b = boundaries().choose();
  set<int> B = boundaries().erase(b);
  set<int> R = attached(b);
  Space S2 = subspace(B); // n2=n
  Space S3 = S0.subspace(B); // n3=n0
  Space S4 = S1.subspace(B); // n4=n1
  Space S5 = S2.section(S2.take(R,*this)); // n5=n-1
  Space S6 = S2.subsection(S3,S4); // n6=n0+n1-n
  Space S7 = S2.subsection(S5,S6); // n7=n-1+n0+n1-n-n=n0+n1-n-1
  Space S8 = S6.antisection(S6.take(S7.regions(),S7),b); // n8=n0+n1-n
  assert(S8.dimension()==n0+n1-n);
  assert(take(S0.regions(),S0).contains(take(S8.regions(),S8)));
  assert(take(S1.regions(),S1).contains(take(S8.regions(),S8)));
  assert(S8.linear());
  return S8;}