Repository navigation
Convert Euclidean n-spaces to 0-based indices #5416
Description
When first introducing definitions for Euclidean n-spaces, I raised the question about whether 1-based indices or 0-based indices would be a better choice.
My original choice was to used 1-based indices because @sctfn's df-ee was already using 1-based indices, and I wanted to later reference it.
The one advantage I thought about for 0-based indices was the direct sum:
For proving
RR^m ⊕ RR^n = RR^(m+n), it might be interesting to use theWordconcept, which has indices starting at zero( 0 ..^ n ), but I still don't believe it a reason enough to choose this convention.
Later, @avekens built upon this definition and added theorems about circles and circle-line intersections, using 1-based indices.
Recently, @littledumb proposed a definition of cross-product which also uses 1-based indices, referring to ~ rrxval and ~ ehlval.
@ProgramCrafter accurately pointed out that using 0-based indices would allow to use Word, and the word constructor <" X Y Z "> would make things much easier. This would be another advantage of 0-based indices.
It would be really nice if the definition of the cross product could be both practical (using the word constructor <" X Y Z ">), and could fit in the more general definition of Euclidean space of dimension n.
Note that the chapter header for matrices mentions 1-based indices, but actually, very few theorems about matrices require 1-based indices. Instead, most theorems are proved about a generic finite set of indices.
What is the community's opinion?
Activity
ProgramCrafter commentedon Jul 29, 2026
My background is programming so I'm for 0-based.
Remember that there is the zero-dimensional space, for which
( 0 ..^ 0 )looks much better than( 1 ... 0 ).I wouldn't care too much if coordinates were named, either, as the extensible structures do; but it hardly works for higher dimensions.
benjub commentedon Jul 29, 2026
As for me:
ProgramCrafter commentedon Jul 29, 2026
If only the same symbol for natural numbers u. { 0 } was any more standard.$\mathbb{N}^+$ and $\mathbb{N}_0$ . On opt-in basis, to be clear.
Fortunately here is the realm of definition-based maths, and any other inconvenience could be avoided by rendering
NNasNN0astirix commentedon Jul 30, 2026
Copying here @david-a-wheeler's comment in #5411 :
jkingdon commentedon Aug 3, 2026
Being able to use
Wordseems like maybe a convincing reason for 0-based but I haven't done enough with the theorems being discussed here to have an especially well informed opinion.sctfn commentedon Aug 3, 2026
FWIW df-ee predates words in set.mm. If I was redoing it today I'd use words and 0-indices.
tirix commentedon Oct 2, 2026
I see a consensus is building around 0-based indices - thanks all for your feedback!
I've started checking what the impacts would be.
Many impacted theorems are in @avekens's mathbox (Real euclidean space of dimension 2, Spheres and lines in real Euclidean spaces) @avekens, what would be your position about this issue in general? If we were to do the change, would you agree that I change the related theorems in your mathbox?
Same question to @arpie-steele, for your section on Simplicial Sets.
avekens commentedon Oct 3, 2026
I did not join the discussion yet, but I also would prefer 0-based indices in general, and especially for df-ee and df-ehl (if these can be unified, as proposed by @benjub , this would be fine). I think the theorems in my mathbox are based on df-ehl and not on df-ee (but I am not sure anymore). In either case, I agree that the theorems in my mathbox are adapted to the new definition(s).
[-]0-based or 1-based indices for Euclidean n-spaces[/-][+]Convert Euclidean n-spaces to 0-based indices[/+]tirix commentedon Oct 11, 2026
@benjub writes:
A difference between
EEandEEHilis that the former is a set of points, while the latter is a structure (as a Hilbert space with addition, inner product, etc.).We have
( Base ` ( EEHil ` N ) ) = ( EE ` N ), therefore I could replace( EE ` N )with( Base ` ( EEHil ` N ) )wherever it is used.The alternative would be to use the more basic
( RR ^m ( 0 ..^ N ) )instead of( EE ` N ).In either case I would probably add hypotheses giving an alias, as in:
(choosing
Pfor the set of points, which does not seem to have too many collisions)I think I would prefer
( RR ^m ( 0 ..^ N ) ). The reason is that we have two separated constructions of the Euclidean spaces:@avekens has built a bridge between the two by defining a nothing of line in an algebraic way, and proving that it matches the "geometric" definition of the line. This is the theorem
eenglngeehlnmwhich I could not immediately convert in #5531, but this is currently the only link.By using
( Base ` ( EEHil ` N ) ), we would use the algebraic concept to define the geometric notion : I my view, this would break that independance. I would prefer the link to be made as late as possible.I would be nice to hear the opinion of others about eliminating the definition
EE, and if they agree, which replacement they would prefer.@sctfn, this second part will massively impact your mathbox. In your comments you already suggested he would agree with the change of base, what about the removal of the
EEdefinition?avekens commentedon Oct 11, 2026
I agree with replacing
( EE ` N )by( RR ^m ( 0 ..^ N ) ), and I would disagree with a replacement by( Base ` ( EEHil ` N ) ), having the same concerns as @tirix .I searched for
EEin set.mm, and found 984 occurences, but "only" 273 not in @sctfn`s mathbox. So all these must be replaced, preferably by an aliasP = ( RR ^m ( 0 ..^ N ) )as suggested by @tirix .I wonder if certain "closure" therorems may cause problems (see ~ eedimeq], whereas others become trivial (see ~ eleei) and may be removed entirely.
The replacement of
( EE ` N )in the definition ofEEGshould not cause any problems, and this is the only change which would have an impact on theorem ~eenglngeehlnm in my mathbox.benjub commentedon Oct 11, 2026
Yes, that sounds more practical and "economical" (except maybe in a few statements that already use EEHil at other places).
tirix commentedon Oct 11, 2026
Ok, this sounds daunting!
Maybe I would first do the change in Jiamin Zhao's mathbox. @littledumb would you agree?
littledumb commentedon Oct 11, 2026
Thanks for the ping @tirix . I agree that starting with my mathbox makes sense.
I’ve just submitted the Pascal PR, so I’d prefer to keep that PR focused and do the
EE → RR ^m ( 0 ...^ N )migration separately right after it. I’m happy to take this on and report back if I run into any closure-theorem issues.sctfn commentedon Oct 12, 2026
sctfn commentedon Oct 12, 2026
tirix commentedon Oct 12, 2026
I think it's very similar to what I did with
df-eeg: It is an extensible structure with:( EE ` N ) = ( RR ^m ( 0 ..^ N ) )as its base,distslot)Itvslot)The theorems
eengtrkgandeengtrkgethen proceed to show that thisEEGstructure fulfills all of Tarski's axioms. This means that all results derived from those axioms are valid inEEG.The other advantage of that approach is that non-Euclidean geometries are also covered.
littledumb commentedon Oct 16, 2026
Hi @tirix, I'd like to revisit the sequencing of the 0-based migration in my mathbox, particularly in relation to the pending Pascal PR (#5535).
I've done some preliminary migration experiments. The 0-based cross and triple products are verified, including their equivalence to the existing 1-based versions. I've also verified a generalization of the 3×3 determinant theorems to arbitrary three-element index sets, which should make the matrix side of the migration more straightforward.
There is still substantial coupling between the cross/triple-product definitions and the Pascal proof chain, but the migration looks manageable.
I see two possible approaches:
I'm comfortable with either approach and happy to do the migration work myself. From the perspective of the broader community effort, which sequencing would you prefer?