Add set-mbox-jag mathbox by jorge-agra · Pull Request #5432 · metamath/set.mm

jorge-agra · 2026-08-12T13:54:36Z

Summary

This PR adds a mathbox for Jorge Agra with a proof of the AAS triangle congruence theorem tgaas, addressing #2983.

The change is intended to be mathbox-only apart from the contributor-list entry. The new mathbox contains the live dependency cone needed for tgaas, including the exterior-angle theorem tgexta, the side-equality main tgaas1, and the final congruence wrapper tgaas.

Notes on provenance

The proofs were produced with heavy use of LLM's tooling and then inserted into set.mm.

The proof skeleton started with https://github.com/tirix/metamath-blueprints Triangle Congruence blueprint, but derived to a path closer to the one used by GeoCoq, used as a route map: its formalization identified useful intermediate geometry lemmas and the proof outline. No Coq proof term was translated or ported into Metamath.

The route avoids introducing a new strict-angle definition. Since set.mm has leA but no ltA, strictness is carried inline as leA together with non-congruence.

Validation

Local validation performed before submission using only metamath-exe:

tirix · 2026-08-13T09:16:54Z

You'll need to run scripts/rewrap to make the failing test pass.

jorge-agra · 2026-08-13T21:56:45Z

From first push I think I followed the steps at CONTRIBUTING.md, but seems some extraneous line spaces got through. it.
Cant get a clear diagnostic from pipeline, probably I am looking into the wrong place.

tirix · 2026-08-16T15:24:09Z

+    |- ( ph -> G TarskiGDim>= 2 )
+      $=
+  ( ncoltgdim2 ) AEFGHBCDIJKLMNOPQ $.
+  $}


This is a exactly theorem ncoltgdim2, it's probably superfluous to define a new theorem.

tirix · 2026-08-16T15:25:20Z

+    tgdefncol $p
+    |- ( ph -> -. ( F e. ( D L E ) \/ D = E ) )
+      $=
+  ( cgrancol ) ABCDEFGHIJKLMONQRSTUAUBUCUEPUDUF $.


Same remark: this is exactly cgrancol. You could propose improvements to the theorem comments or propose to rename it.

tirix · 2026-08-16T15:27:31Z

+       ~ cgrane4 ), and betweenness alone permits a collapsed arm.  Same
+       skeleton as ~ cgrahlb with segment addition ( ~ tgcgrextend ) in place
+       of subtraction.  (Contributed by JAG, 12-Aug-2026.) $)
+    cgrabtwnb $p |- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )


I think this is the same as ~ flatcgra

tirix · 2026-08-16T15:34:33Z

+  ( cv cs3 cinag cfv wbr ccgra wa wceq simpr breq1d eqidd breq2d anbi12d cstrkg
+  s3eqd cgrane3 cgrane4 cds eqid tgbtwntriv1 hlid olcd isinagd cgrahlb rspcedvd
+  necomd jca ) ABUGZKLMUHZGUIUJZUKZCEJUHZKLVNUHZGULUJZUKZUMKVOVPUKZVRKLKUHZVTUK
+  ZUMBKDUBAVNKUNZUMZVQWBWAWDWFVNKVOVPAWEUOZUPWFVSWCVRVTWFKLVNKKLWFKUQWFLUQWGVAU
+  RUSAWBWDAKLMDGHIUTKKNOPUBUBUCUDQUBALKACEFKDLMGHINOPQRSTUBUCUDUEVBVLZALMACEFKD
+  LMGHINOPQRSTUBUCUDUEVCVLWHAKMDGHGVDUJZNWIVEZOQUBUDVFAKKLIUJUKKLUNAKKLDGHINOPU
+  BUBUCQWHVGZVHVIACEJKDLKGHIWINOPWJQRSUAUBUCUBUFWKVJVMVK $.


The proof block takes the whole 80 chars width. I'm surprised rewrap did not indent, usually there is an indentation of 4 blank spaces.

rewrap didnt complain so I didnt changed it. The 4 spaces indent is required?

Actually, I see a few other theorems also do not indent the proof blocks. I'll check the opinion of the community, but this is certainly not blocking.

tirix · 2026-08-16T15:44:48Z

+       trichotomy and its first two disjuncts collapse into the half-line exit
+       through ~ btwnhl2 .  Generic ray/betweenness bookkeeping; ~ cgrainag
+       uses it to route the collinear half of its case analysis.  (Contributed
+       by JAG, 12-Aug-2026.) $)


A note on the comment: E is not really the "middle one", since D and W could be on the same size of E.
I find it's often easier to name the objects when describing a theorem:

Given three colinear points `D`, `E` and `W`, the point `E` is either between `D` and `W`, or both `D` and `W` lie on a ray starting at `E`.

tirix · 2026-08-16T15:45:14Z

+       through ~ btwnhl2 .  Generic ray/betweenness bookkeeping; ~ cgrainag
+       uses it to route the collinear half of its case analysis.  (Contributed
+       by JAG, 12-Aug-2026.) $)
+    hlorbtwn $p |- ( ph -> ( D ( K ` E ) W \/ E e. ( D I W ) ) )


This seems to be the same theorem as lnhl

tirix

Sorry I lack time to review carefully.
I only reviewed until hlorbtwn for now.
To be continued

tirix · 2026-08-17T07:19:34Z

+  $( 'v' is bound in the conclusion, so these are mandatory and propagate to
+     every caller. $)


That's correct, but it's also the case for all theorems with bound variables.

tirix · 2026-08-17T07:21:03Z

+    inagcgrabtwn $p
+    |- ( ph -> E. v e. P
+         ( v ( inA ` G ) <" X Y Z ">
+           /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
+      $=


As a general remark: the labels for the essential hypotheses (iabtw) do not match the labels for the theorem (inagcgrabtwn). It's better to keep them aligned, in order to avoid possible future conflicts.

This also applies to the 3~4 previous theorems.

tirix · 2026-08-17T07:25:01Z

+  VKEVPVQVAZVSNOEURZWAVAZVKBEDUJAVOEVCZVKZVRWCWBWEWGVOEVPVQAWFVDZVEWGVTWDVSWAWG
+  NOVOENOWGNVFWGOVFWHVGVHVIACDEFGHIJKLIVJUTZMNOPQRSWIVLTUAUBUCUDUEUFUGUHUIUJUKU
+  LUMUNUOUPVMVN $.
+  $}


It looks like the essential hypotheses $e for inagcgratrgmain and inagcgratrgw are exactly the same: in that case, you can put both theorems in the same scope ${ ... $} and avoid duplicating them.

This also works for inagcgratrgncol and inagcgratrgncol: inagcgratrgncol has a few additional hypotheses, you can put it in a nested scope and share the common ones.

jorge-agra · 2026-08-23T11:01:43Z

Hypothesis-block deduplication (comment + sweep) — 9 groups collapsed into shared ${ ... } scopes, first-member-owns-the-labels convention:

inagcgratrgmain/inagcgratrgw, inagcgratrgncol/inagcgratrgn (the two pairs on comments)
tgmircgrg/tgmircgra/tgextamirn
tgextalem1inag/tgextale/tgextamirnhl/tgextahp/tgextancgra
tgaascgra/tgaas1h
tgaas1/tgaas (shared labels renamed to tgaas1.*, the first member)

jorge-agra · 2026-08-23T11:02:51Z

Duplicate theorems removed :

tgatgdim2 → callers now cite ~ ncoltgdim2 directly
tgdefncol → callers now cite ~ cgrancol directly
cgrabtwnb → callers now cite ~ flatcgra directly
hlorbtwn → callers now cite ~ lnhl + ~ hlcomd (commuted disjunct)

jorge-agra · 2026-08-23T11:03:51Z

No warnings from metamath or metamath-knife

wlammen · 2026-09-11T07:37:24Z

If no one objects, I will merge this next week.

avekens · 2026-09-13T12:02:56Z

There is still no approval. @tirix what do you think? Can this PR be merged, although there are may be some issues to be discussed? Since this PR concerns a mathbox only, I think the discussion can be continued after this PR is merged.

icecream17

I looked at about half of it and nothing is blocking, which might slightly help with mergability.

Plenty of (somewhat vague) thoughts to chew on for a later pr though.

icecream17 · 2026-09-16T14:37:07Z

+$( Proof of the exterior-angle theorem 'tgexta' and the
+   AAS triangle congruence criterion 'tgaas' in Tarski geometry.
+
+   Elementary consequences of triangle non-collinearity, the
+   degenerate-angle congruence constructor, in-angle transport
+   across an angle congruence, the exterior-angle theorem and its strictness
+   half, and finally the AAS assembly, with 'tgaas'.
+
+   Strictness of an angle comparison has no primitive here: 'set.mm' defines
+   'leA' but no 'ltA', so "strictly less" is carried inline as 'leA' together
+   with the failure of 'cgrA'. $)
+
+$( Consequences of triangle non-collinearity: vertex inequalities, the
+   dimension condition, and non-collinearity transported across an angle
+   congruence. $)
+
+
+  ${


Suggested change

$( Proof of the exterior-angle theorem 'tgexta' and the

AAS triangle congruence criterion 'tgaas' in Tarski geometry.

Elementary consequences of triangle non-collinearity, the

degenerate-angle congruence constructor, in-angle transport

across an angle congruence, the exterior-angle theorem and its strictness

half, and finally the AAS assembly, with 'tgaas'.

Strictness of an angle comparison has no primitive here: 'set.mm' defines

'leA' but no 'ltA', so "strictly less" is carried inline as 'leA' together

with the failure of 'cgrA'. $)

$( Consequences of triangle non-collinearity: vertex inequalities, the

dimension condition, and non-collinearity transported across an angle

congruence. $)

${

$( The exterior-angle theorem ~ tgexta and the

AAS triangle congruence criterion ~ tgaas in Tarski geometry.

In order: Elementary consequences of triangle non-collinearity, the

degenerate-angle congruence constructor, in-angle transport across an

angle congruence, the exterior-angle theorem and its strictness half,

and finally the AAS assembly, with ~ tgaas .

Strict less-than angle comparison is notated as 'leA' together

with the failure of 'cgrA', since 'set.mm' defines 'leA' but not 'ltA'. $)

$( Consequences of triangle non-collinearity: vertex inequalities, the

dimension condition, and non-collinearity transported across an angle

congruence. $)

${

non-blocking

feel free to choose only the changes that look good to you:

Shorter "title" first paragraph

Clarify what the second paragraph is for

Simplify the third paragraph (more readable I think)

Remove newline: double newline very uncommon + the second comment becomes a bit closer to the theorems its about, which is clearer (edit: see below suggestion for an alternative to this)

Sign in to view

+    $( A flat sub-angle forces the containing angle flat: if ' W ' is inside
+       angle ' <" D E F "> ' and ' E ' lies between ' D ' and ' W ' ,
+       then ' E ' lies between ' D ' and ' F ' .  This is
+       GeoCoq ' bet__in__angle__bet '.  Proved by unfolding ~ isinag and
+       following its segment point.  (Contributed by JAG, 12-Aug-2026.) $)


Sign in to view

+    $( In-angle transport, degenerate branch (i): the sub-angle ' <" D E W
+       "> ' is **null**, ' W ' lying on ray ' ED ' .  The witness is not
+       constructed -- it is ' X ' , the target's own first arm -- and ~ cgrahlb
+       supplies the copied angle from the two ray degeneracies.  No GeoCoq
+       counterpart:  GeoCoq's branch only locates a witness supplied by its
+       universal statement.  (Contributed by JAG, 12-Aug-2026.) $)
+    inagcgrasubhl $p
+    |- ( ph -> E. v e. P
+         ( v ( inA ` G ) <" X Y Z ">
+           /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )


icecream17 · 2026-09-16T15:21:11Z

+  $}
+
+$( Angle order ('leA') and its witnesses: passing between "inside the angle"
+   and 'leA', transporting a witness across a congruent target angle, and
+   replacing either compared angle by a congruent one. $)
+
+
+  ${


Actually, as an alternative to my earlier suggestion, maybe it would make more sense to have:

2 empty lines before
1 empty line after

such comments.

icecream17 · 2026-09-16T15:29:04Z

+    inaglea.p $e |- P = ( Base ` G ) $.
+    inaglea.i $e |- I = ( Itv ` G ) $.
+    inaglea.k $e |- K = ( hlG ` G ) $.
+    inaglea.g $e |- ( ph -> G e. TarskiG ) $.
+    inaglea.a $e |- ( ph -> A e. P ) $.
+    inaglea.b $e |- ( ph -> B e. P ) $.
+    inaglea.c $e |- ( ph -> C e. P ) $.
+    inaglea.y $e |- ( ph -> Y e. P ) $.
+    inaglea.1 $e |- ( ph -> C ( inA ` G ) <" A B Y "> ) $.
+    $( If ' C ' lies inside angle ' <" A B Y "> ' , then angle ' <" A B C
+       "> ' is less than or equal to ' <" A B Y "> ' .  (Contributed by JAG,
+       12-Aug-2026.) $)
+    inaglea $p
+    |- ( ph -> <" A B C "> ( leA ` G ) <" A B Y "> )
+      $=


I'm not sure if it is valid to order the theorems like this, but I'm thinking this theorem could shorten the proof of ~ inagbtwn .

Anyhow:

Suggested change

inaglea.p $e |- P = ( Base ` G ) $.

inaglea.i $e |- I = ( Itv ` G ) $.

inaglea.k $e |- K = ( hlG ` G ) $.

inaglea.g $e |- ( ph -> G e. TarskiG ) $.

inaglea.a $e |- ( ph -> A e. P ) $.

inaglea.b $e |- ( ph -> B e. P ) $.

inaglea.c $e |- ( ph -> C e. P ) $.

inaglea.y $e |- ( ph -> Y e. P ) $.

inaglea.1 $e |- ( ph -> C ( inA ` G ) <" A B Y "> ) $.

$( If ' C ' lies inside angle ' <" A B Y "> ' , then angle ' <" A B C

"> ' is less than or equal to ' <" A B Y "> ' . (Contributed by JAG,

12-Aug-2026.) $)

inaglea $p

|- ( ph -> <" A B C "> ( leA ` G ) <" A B Y "> )

$=

inaglea.p $e |- P = ( Base ` G ) $.

inaglea.i $e |- I = ( Itv ` G ) $.

inaglea.k $e |- K = ( hlG ` G ) $.

inaglea.g $e |- ( ph -> G e. TarskiG ) $.

inaglea.a $e |- ( ph -> A e. P ) $.

inaglea.b $e |- ( ph -> B e. P ) $.

inaglea.c $e |- ( ph -> C e. P ) $.

inaglea.y $e |- ( ph -> Y e. P ) $.

inaglea.1 $e |- ( ph -> C ( inA ` G ) <" A B Y "> ) $.

$( If ` C ` lies inside angle ` <" A B Y "> ` , then angle ` <" A B C "> `

is less than or equal to ` <" A B Y "> ` . (Contributed by JAG,

12-Aug-2026.) $)

inaglea $p

|- ( ph -> <" A B C "> ( leA ` G ) <" A B Y "> )

$=

(the code bracket formatting suggestion can probably be applied to several other theorems)

icecream17 · 2026-09-16T15:33:19Z

+    $d F w $.  $d G w $.  $d H w $.  $d J w $.  $d P w $.  $d U w $.
+
+    $( Source-side ' leA ' transport: replacing the smaller angle by a


Not gonna lie, this pr has plenty of unusual formatting events. For instance, normally this empty line would not exist and the dv conditions would be above the hypotheses.

But I guess it's fine (?)

icecream17 · 2026-09-16T15:34:27Z

+  KVLVM $.
+  $}
+
+$( Angle order under congruence of both compared angles ( ~ leacgra ), used by


Only reviewed up to here (around halfway)

tirix · 2026-09-16T16:18:19Z

I meant to take more time to review this PR but I've been pretty busy lately, thanks for jumping in!

david-a-wheeler · 2026-09-19T19:35:48Z

@jorge-agra - thank you SO MUCH for setting up a mathbox, and I'm always excited to see our geometry material expand.

There are some review comments above, but please don't let that discourage you. Our goal is high quality, and that means that we get picky sometimes, but we're always delighted to see people working to make real contributions.

jorge-agra · 2026-09-20T22:20:08Z

Will try to address @icecream17 review comments during this week/next weekend. Thank you for taking the time to take a look at it.

Add set-mbox-jag mathbox

28f5567

jorge-agra mentioned this pull request Aug 12, 2026

Prove SAS etc. theorems for triangles #861

Open

jkingdon added the mathbox only label Aug 12, 2026

address metamath-knife warnings

eba33c2

retry - small change in inagbtwn

4cbada2

tirix reviewed Aug 16, 2026

View reviewed changes

tirix reviewed Aug 17, 2026

View reviewed changes

fix: tgaas PR comments 1st

9c2f9ed

tirix mentioned this pull request Aug 23, 2026

Angle addition is compatible with congruence (again) #5454

Merged

icecream17 approved these changes Sep 16, 2026

View reviewed changes

		$( 'v' is bound in the conclusion, so these are mandatory and propagate to
		every caller. $)

		$d F w $. $d G w $. $d H w $. $d J w $. $d P w $. $d U w $.

		$( Source-side ' leA ' transport: replacing the smaller angle by a

Conversation

jorge-agra commented Aug 12, 2026

Summary

Notes on provenance

Validation

Uh oh!

tirix commented Aug 13, 2026

Uh oh!

jorge-agra commented Aug 13, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tirix Aug 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tirix left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tirix Aug 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tirix Aug 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jorge-agra commented Aug 23, 2026

Uh oh!

jorge-agra commented Aug 23, 2026

Uh oh!

jorge-agra commented Aug 23, 2026

Uh oh!

wlammen commented Sep 11, 2026

Uh oh!

avekens commented Sep 13, 2026

Uh oh!

icecream17 left a comment

Choose a reason for hiding this comment

Uh oh!

icecream17 Sep 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tirix commented Sep 16, 2026

Uh oh!

tirix Aug 16, 2026 •

edited

Loading

tirix Aug 17, 2026 •

edited

Loading

tirix Aug 17, 2026 •

edited

Loading

icecream17 Sep 16, 2026 •

edited

Loading