Iconological Semantics (Schlenker and Lamberton), geometric part, Sections 7.2-7.3
The original projection definitions (85) and (90), a reconstruction of the similarity-based formulation suggested in footnotes 45 and 64, and proofs that the two are equivalent.
Paper text (Greek letters restored from the PDF)Let ρ* be the Cartesian frame of reference associated with the signer, and let WORD be a word (e.g. a predicate classifier). For any viewpoint π, time t, world w, and object d, proj(d, π, t, w) = WORD iff (i) word't,w(d) = 1, and (ii) modulo the scaling factor σ(π) (> 0), the position and orientation of d relative to ρ(π) correspond (in terms of coordinates) to the position and orientation of CL relative to ρ*, or in formal terms: a. center(d, ρ(π)) = σ(π) • center(WORD, ρ*) b. orientation(d, ρ(π)) = orientation(WORD, ρ*)
proj(π, t, w, d) = word-cl_τ iff (i) word′_{t,w}(d) = 1, and (ii) for each δ′ ≤ δ, proj(d, π, t+(τ(π))δ′, w) = word-cl_τ(δ′).
Suggested replacement
proj(d, π, t, w) = word-cl_τ iff (i) word′_{t,w}(d) = 1, and (ii) for each δ′ such that 0 ≤ δ′ ≤ δ, proj(d, π, t+(τ(π))δ′, w) = word-cl_τ(δ′).
Further edits
Paper text
proj(π, t, w, Obama) = CL-person_τ
Suggested replacement (Example (91))
proj(Obama, π, t, w) = CL-person_τ
Paper text
(insert)
Suggested replacement (Just after (85)(ii)b (new sentence))
Here center(d, ρ(π)) and orientation(d, ρ(π)) are the position and orientation of d at the time t and in the world w of evaluation.
What the paper does, and why it fails
(1) The left-hand side of (90) and (91) writes proj(π, t, w, d), while (85) and the right-hand side of (90)(ii) write proj(d, π, t, w). (2) The range of δ′ is given as ‘δ′ ≤ δ’ without δ′ ≥ 0 (although the classifier movement is defined on [0, δ]). (3) In (85), center(d, ρ(π)) and orientation(d, ρ(π)) have no time or world argument, but (90) needs the object’s pose at times t + τ(π)δ′.
What the change does
proj has the same argument order everywhere, δ′ ranges over [0, δ] explicitly, and (85) says that positions and orientations are those of the time and world of evaluation, so that (90)(ii) evaluates (85) at the right time. Lean: projDyn, projDyn_iff, example_dynamic.
Anything else affected?No other change to results. Also affects: the prose of Section 7.3 (‘for each δ′ ≤ δ’, twice, before (90)) should carry the same ‘0 ≤ δ′’. Note that (85)(i) must then hold throughout the movement (a sitting person stays sitting).
Text note: Greek letters and subscripts restored from the PDF (page 36); the text extraction writes d’ ≤ d, t(π) and wordt.
theorem projDyn_iff (lex : Rat → Prop) (π : Viewpoint) (rstar : Frame) (dur : Rat)
(cl obj : Rat → Pose) (t : Rat) :
projDyn lex π rstar dur cl obj t ↔
lex t ∧ projDynSim lex (π.toSim rstar) π.ts dur cl obj t := byunfold projDyn projDynSim
constructor
· rintro ⟨h0, h⟩
refine ⟨h0, fun d' a b => ?_⟩
have := (projStatic_iff _ π rstar _ _).1 (h d' a b)
exact this
· rintro ⟨h0, h⟩
refine ⟨h0, fun d' a b => ?_⟩
exact (projStatic_iff _ π rstar _ _).2 (h d' a b)
(ii) a (right-handed) triple of orthogonal vectors of unit length that encode the orientation of d.
Suggested replacement (after the sentence ‘… of the form <u, v, w>, where u is a triple of coordinates of a unit-length vector, and similarly for v and w.’ in (84a)(ii), as a new sentence)
Which side of d (for instance front, side, top) each of the three vectors marks is fixed by a convention for each type of object or classifier; (85)(ii)b only requires that the triple for the classifier and the triple for the object coincide.
What the paper does, and why it fails
The orientation is a triple <u, v, w> but the paper does not say what the vectors mean (front, side, up). (85)(ii)b only compares the triples of the classifier and the object.
What the change does
The inserted sentence states that the convention is set per kind of object or classifier and that (85) only needs the two triples to coincide.
Anything else affected?No other change: (85) and the example only use equality of triples; no convention is needed for the results.
Judgment call: the wording of this replacement is ours and not checked in Lean. Optional clarification (our wording). We did not pick a specific convention (e.g. which vector is ‘front’): the example’s triples do not settle it.
Paper text (Greek letters restored from the PDF)Let ρ* be the Cartesian frame of reference associated with the signer, and let word-clτ be a dynamic [...] predicate classifier. If δ is the duration of the classifier movement, we view word-clτ as a function from the interval [0, δ] to static classifiers. Then: proj(π, t, w, d) = wordτ iff (i) word't,w(d) = 1, and (ii) for each δ' ≤ δ, proj(d, π, t+(τ(π))δ', w) = word-clτ(δ').
Statementdynamic projection: (i) lexical, (ii) for each d' in [0,d], proj at time t+t(pi)d' to static classifier word-cl(d')
Paper text(ii) a (right-handed) triple of orthogonal vectors of unit length that encode the orientation of d. Relative to a frame of reference r, the coordinates of this triple of vectors are given by orientation(d, r), [...] <u, v, w>, where u is a triple of coordinates of a unit-length vector, and similarly for v and w.
Statementa right-handed triple of orthogonal unit vectors is the same as an orthogonal matrix with det 1
(ii) a (right-handed) triple of orthogonal vectors of unit length that encode the orientation of d.
Suggested replacement (after the sentence ‘… of the form <u, v, w>, where u is a triple of coordinates of a unit-length vector, and similarly for v and w.’ in (84a)(ii) (before footnote 45’s continuation), as a new sentence in the same item)
Note that (85) itself only compares coordinates. The requirement that the triples be right-handed and orthonormal matters if projection is later reformulated as the existence of a rotation, translation and scaling taking the classifier to the object (footnote 64): no such transformation maps a right-handed orthonormal triple onto a left-handed or non-unit one.
What the paper does, and why it fails
(84a)(ii) requires the orientation to be a right-handed triple of orthogonal unit vectors, but nothing in (85) uses this: (85)(ii)b just compares two triples for equality, and makes sense for arbitrary triples. The requirement only matters for the footnote-64 reading (a transformation carrying classifier to object).
What the change does
The inserted note says where the requirement is actually needed. Left-handed objects (mirror images) can never project on a right-handed classifier under the transformation reading. Lean: no_sim_to_mirror_pose, no_sim_to_nonunit_pose, exists_sim_of_valid; projStatic_iff holds for all poses.
Anything else affected?No other change: (85) is unaffected. Mirror-image objects are not handled by the transformation reading.
Judgment call: the wording of this replacement is ours and not checked in Lean. This is an optional clarifying sentence (mine); (85) needs no correction.
theorem no_sim_to_mirror_pose :
¬ ∃ g : Sim, g.act ⟨0, M3.one⟩ = ⟨0, M3.diag 11 (-1)⟩ := by
rintro ⟨g, h⟩
have := congrArg Pose.O h
simp only [Sim.act, M3.mul_one] at this
have hd := g.hQ.2.2
rw [this] at hd; revert hd; decide +kernel
/-- Likewise a non-unit "orientation triple" (orthogonal but not normalized). -/theorem no_sim_to_nonunit_pose :
¬ ∃ g : Sim, g.act ⟨0, M3.one⟩ = ⟨0, M3.diag 222⟩ := by
rintro ⟨g, h⟩
have := congrArg Pose.O h
simp only [Sim.act, M3.mul_one] at this
have hd := g.hQ.2.2
rw [this] at hd; revert hd; decide +kernel
Paper textWe could then take a classifier representation to be true of an object just in case there is a certain geometric transformation (based for instance on translations, rotations and scaling) from one to the other.
Statementclassifier's pose is mapped onto the object's pose by a similarity (scale s>0, rotation, translation) fixed by the viewpoint
/-- A similarity of space: uniform scaling `s > 0`, rotation `Q`, translation `t`. -/@[ext]structure Sim where
s : Rat
hs : 0 < s
Q : M3
hQ : IsRot Q
t : V3
Asananonymousreviewernotes,it would bemore standard and elegant to defineorientationasatriple of angles,as this suffices to characterize the tripleoforthogonalvectorsassociatedwiththeobject
Suggested replacement (at the end of footnote 45, after ‘… rather than by a triple of triples of vector coordinates.’)
Note, however, that different triples of angles can represent the same orientation, so (85)(ii)b would then have to require that the two triples of angles represent the same orientation, rather than that they be identical.
What the paper does, and why it fails
A triple of angles does determine the orthogonal triple, but not uniquely: the same orientation can be given by several triples of angles (and at some orientations the angles are not well defined). (85)(ii)b asks for equality of the orientation of the object and that of the classifier, which would go wrong if it compared angle triples literally.
What the change does
The added sentence keeps the reviewer’s suggestion and says what (85)(ii)b would have to become. Rotation matrices (used in Lean, columns u, v, w) or unit quaternions avoid the issue.
Anything else affected?No other change: the paper keeps triples of vectors; footnote 45 is not formalized beyond the rotation-matrix encoding (Lean: rightHanded_isRot).
Judgment call: the wording of this replacement is ours and not checked in Lean. Optional caveat (our wording); the reviewer’s claim that angles suffice to characterize the vectors is true.
/-- The paper's "right-handed triple of orthogonal unit vectors" is exactly a rotation matrix. -/theorem rightHanded_isRot {u v w : V3} (h : RightHandedOrthonormal u v w) :
IsRot ⟨u, v, w⟩ := byobtain ⟨h1, h2, h3, h4, h5, h6, h7⟩ := h
simp [V3.dot, V3.ext_iff, V3.cross] at h1 h2 h3 h4 h5 h6 h7
obtain ⟨h7x, h7y, h7z⟩ := h7
refine ⟨?_, ?_, ?_⟩
· simp [M3.ext_iff, V3.ext_iff, M3.mul, M3.T, M3.one]; grind
· simp [M3.ext_iff, V3.ext_iff, M3.mul, M3.T, M3.one]; grind
· simp [M3.det, V3.dot, V3.cross]; grind
E10note Note: scaling is a single factor about the origin of ρ*
Location: Section 7.2, (84b), (85)(ii)a, p. 33 PDF
Paper text
scaling will be implemented by way of a multiplicative factor applied to all positional coordinates
Suggested replacement
(delete)
What the paper does, and why it fails
Scaling by one factor σ(π) applied to positional coordinates only makes sense if the origins of ρ* and ρ(π) are put in correspondence: centers are scaled about the origin of ρ*. The paper does not say this.
What the change does
No edit is needed. In the similarity reformulation the translation is explicit (Lean: Viewpoint.toSim), and (frame, scale) and similarity determine each other given ρ* (toViewpoint_toSim).
Anything else affected?No other change: nothing is lost or added by the similarity reformulation.
Paper text (Greek letters restored from the PDF)(ii) modulo the scaling factor σ(π) (> 0), the position and orientation of d relative to ρ(π) correspond (in terms of coordinates) to the position and orientation of CL relative to ρ*, or in formal terms: a. center(d, ρ(π)) = σ(π) • center(WORD, ρ*) b. orientation(d, ρ(π)) = orientation(WORD, ρ*)
Statement(85) holds for pi iff toSim maps the classifier pose onto the object pose (no assumption on poses)
theorem projStatic_iff (lex : Prop) (π : Viewpoint) (rstar : Frame) (cl d : Pose) :
projStatic lex π rstar cl d ↔ projSim lex (π.toSim rstar) cl d := byunfold projStatic projSim center orientation
constructor
· rintro ⟨hl, hc, ho⟩
refine ⟨hl, ?_⟩
have hc' : d.c = π.frame.point (π.s • rstar.coord cl.c) := byrw [← hc, Frame.point_coord]
have ho' : d.O = π.frame.R.mul (rstar.R.T.mul cl.O) := byrw [← ho, frame_cancel]
refine Pose.ext ?_ ?_
· show (π.toSim rstar).apply cl.c = d.c
rw [toSim_apply]; exact hc'.symm
· show (π.toSim rstar).Q.mul cl.O = d.O
rw [toSim_orient]; exact ho'.symm
· rintro ⟨hl, h⟩
refine ⟨hl, ?_, ?_⟩
· have := congrArg Pose.c h
simp only [Sim.act, toSim_apply] at this
rw [← this, Frame.coord_point]
· have := congrArg Pose.O h
simp only [Sim.act, toSim_orient] at this
rw [← this, frame_cancel']
proven
The equivalence theorem: exactly what it says
Absolute ambient coordinates are added (implicit in the paper): a pose is (center c, orientation matrix O with columns u,v,w); a frame is (origin o, rotation R). Then center(P,F) = R^T(c - o) and orientation(P,F) = R^T O (as in (84)). A viewpoint pi is (frame r(pi), s(pi), t(pi)).
projStatic_iff: for every viewpoint pi, signer frame r*, poses cl, d:
(85)(ii)a,b <=> g_pi(cl) = d, where g_pi = (scale s(pi), rotation Q = R_pi R*^T, translation o_pi - s(pi) Q o*), and g(c,O) = (s Q c + t, Q O).
So the data (r(pi), s(pi)) of pi become one similarity g_pi (Viewpoint.toSim); the map (frame, scale) -> similarity is a bijection given r* (toViewpoint_toSim), so nothing is lost or added. The theorem needs no hypothesis on poses. Dynamic: projDyn_iff gives lex(t) and, for d' in [0,d], lex(t+t(pi)d') and g_pi(cl(d')) = obj(t+t(pi)d'): spatial similarity plus the affine time map d' -> t + t(pi) d'.
Minor typo: fn 64: transformation should be the one fixed by the viewpoint
E4ill-posed statement Footnote 64: the transformation should be the one determined by the viewpoint, otherwise ‘there is a transformation’ says nothing
We could then take a classifier representation to be true of an object just in case there is a certain geometric transformation (based for instance on translations, rotations and scaling)from one to the other.
Suggested replacement
We could then take a classifier representation to be true of an object just in case a certain geometric transformation (based for instance on translations, rotations and scaling), the one determined by the viewpoint π and the signer’s frame of reference ρ*, maps the classifier’s center and orientation onto those of the object. Once the scaling factor σ(π) is fixed, this transformation is unique.
What the paper does, and why it fails
Read as a plain existential (‘there is some transformation’), the condition is empty: for any two proper poses and any scale there is a rotation, translation and scaling carrying one to the other. The condition only constrains anything because all classifiers of a scene share one viewpoint, hence one transformation.
What the change does
The transformation is now the one fixed by π and ρ*, so the constraint bites: with all classifiers of a scene under the same π, distances scale by σ(π) and relative orientations are preserved. This reading is equivalent to (85) (Lean: projStatic_iff; exists_sim_of_valid shows the plain existential is vacuous; sim_unique gives uniqueness).
Anything else affected?No other change: footnote 64 is a suggestion for future work and nothing later depends on it.
Judgment call: the wording of this replacement is ours and not checked in Lean. The reading ‘the transformation determined by π and ρ*’ is our reconstruction (the Lean ‘elegant version’), not necessarily what the authors have in mind.
/-- Given the scale, the transformation is unique (for a valid classifier pose). -/theorem sim_unique (cl : Pose) (hcl : cl.Valid) (g g' : Sim) (hs : g.s = g'.s)
(h : g.act cl = g'.act cl) : g = g' := byhave hO := congrArg Pose.O h
have hc := congrArg Pose.c h
simp only [Sim.act] at hO hc
have hQ : g.Q = g'.Q := byhave := congrArg (fun M => M.mul cl.O.T) hO
simp only [M3.mul_assoc, hcl.2.1, M3.mul_one] at this
exact this
obtain ⟨s, hs0, Q, hQ0, t⟩ := g
obtain ⟨s', hs0', Q', hQ0', t'⟩ := g'
simp only at hs hQ
subst hs; subst hQ
simp only [Sim.apply] at hc
have : t = t' := by
...
Paper text (Greek letters restored from the PDF)Any viewpoint π specifies a Cartesian frame of reference ρ(π), a spatial scaling factor σ(π) (and for dynamic projection, a temporal scaling factor τ(π)).
Statementevery similarity (with any t(pi)>0) comes from a viewpoint and back: (frame, scale) <-> similarity, given r*
theorem projDyn_iff (lex : Rat → Prop) (π : Viewpoint) (rstar : Frame) (dur : Rat)
(cl obj : Rat → Pose) (t : Rat) :
projDyn lex π rstar dur cl obj t ↔
lex t ∧ projDynSim lex (π.toSim rstar) π.ts dur cl obj t := byunfold projDyn projDynSim
constructor
· rintro ⟨h0, h⟩
refine ⟨h0, fun d' a b => ?_⟩
have := (projStatic_iff _ π rstar _ _).1 (h d' a b)
exact this
· rintro ⟨h0, h⟩
refine ⟨h0, fun d' a b => ?_⟩
exact (projStatic_iff _ π rstar _ _).2 (h d' a b)
proven
Minor typo: (90): argument order, range 0<=d'<=d, missing time argument of (85)
E6ill-posed statement Definition (90): use the argument order of (85), write the range 0 ≤ δ′ ≤ δ, and give (85) a time argument (details above)
Not stated in the paper as such — related passage (Greek letters restored from the PDF)
Related passage in the paperThen: proj(π, t, w, d) = wordτ iff (i) word't,w(d) = 1, and (ii) for each δ' ≤ δ, proj(d, π, t+(τ(π))δ', w) = word-clτ(δ').
Statementfor d>=0 the condition (i) follows from (ii)
(90)(ii) with δ′ = 0 asks that d projects to word-cl_τ(0) at time t, and (85) includes (i) at that time; so condition (i) of (90) is already implied by (ii) whenever δ ≥ 0.
What the change does
No edit is needed; the redundancy is harmless (it parallels the redundancy of the lexical condition in (53)). One could delete (i), keeping only (ii). Lean: projDyn_i_redundant.
Anything else affected?No other change. If (i) were deleted, (90) would consist of (ii) alone.
Text note: This is line (i) of definition (90), p. 36 (the same line occurs in (85) and in Appendix I-E).
theorem lexical_condition_redundant (lex : Prop) (π : Viewpoint) (rstar : Frame)
(cl d : Pose) :
(lex ∧ projStatic lex π rstar cl d) ↔ projStatic lex π rstar cl d :=
⟨fun h => h.2, fun h => ⟨h.1, h⟩⟩
proven (trivial; caveat, see Issues 10)
Minor typo: lexical conjunct redundant only for two-valued lexical content
E7overclaim Section 7.2 and footnote 49: the lexical conjunct of (53) is redundant only for two-valued lexical content
Location: Section 7.2, p. 35, footnote 49 (rule (53), pp. 21-22) PDF
Paper text
The result is that, as announced, the lexical conditions we had in (53) become redundant with the definition of projections in (85).
Suggested replacement
The result is that, as announced, the lexical conditions we had in (53) become redundant with the definition of projections in (85), at least when the lexical predicate is two-valued: the case in which [[P]] c, s, t, w(x) = # in (53) is not covered by (85).
What the paper does, and why it fails
Rule (53) returns # when [[P]](x) = # (presupposition failure of the lexical predicate) and otherwise conjoins [[P]](x) = 1 with the projective condition. Definition (85) is a condition on proj with a two-valued lexical condition word′_{t,w}(d) = 1, so it cannot reproduce the # case.
What the change does
The sentence now claims redundancy only where it holds, the two-valued case, and flags the # case. Lean: lexical_condition_redundant (the lexical predicate is abstracted as a two-valued proposition).
Anything else affected?No other change: nothing later depends on the claim; rule (53) cannot be simplified where undefinedness of the lexical predicate matters. Footnote 49 already discusses another limit (complex WORD containing variables).
Judgment call: the wording of this replacement is ours and not checked in Lean. The wording of the caveat is mine; the paper’s (53) is stated in the text of Section 5 (pp. 21-22).
Related passage in the paperb. Orientation: We take the orientation of a locus to be ambiguous, in the sense that one can pick any orientation one wishes. For present purposes, we can take this condition to be trivialized, i.e. always satisfied.
Statementdropping the orientation condition = some locus orientation exists making (127) true
Not stated in the paper as such — related passage ((fn 64); the composition lemma itself is not in the paper)
Related passage in the paperSecond, as noted by E. Chemla (p.c.), we have in effect encoded real-world objects and sign language classifiers alike by way of points and frames. We could then take a classifier representation to be true of an object just in case there is a certain geometric transformation (based for instance on translations, rotations and scaling) from one to the other.
Statementacting by g2 after g1 is acting by the composite
Not stated in the paper as such — related passage ((fn 64); the inverse and symmetry lemmas themselves are not in the paper)
Related passage in the paperSecond, as noted by E. Chemla (p.c.), we have in effect encoded real-world objects and sign language classifiers alike by way of points and frames. We could then take a classifier representation to be true of an object just in case there is a certain geometric transformation (based for instance on translations, rotations and scaling) from one to the other.
Paper textwe have in effect encoded real-world objects and sign language classifiers alike by way of points and frames. We could then take a classifier representation to be true of an object just in case there is a certain geometric transformation (based for instance on translations, rotations and scaling) from one to the other.
Statementfor valid poses and any scale, some similarity maps classifier to object: "there is a transformation" alone says nothing
E4ill-posed statement Footnote 64: the transformation should be the one determined by the viewpoint, otherwise ‘there is a transformation’ says nothing
We could then take a classifier representation to be true of an object just in case there is a certain geometric transformation (based for instance on translations, rotations and scaling)from one to the other.
Suggested replacement
We could then take a classifier representation to be true of an object just in case a certain geometric transformation (based for instance on translations, rotations and scaling), the one determined by the viewpoint π and the signer’s frame of reference ρ*, maps the classifier’s center and orientation onto those of the object. Once the scaling factor σ(π) is fixed, this transformation is unique.
What the paper does, and why it fails
Read as a plain existential (‘there is some transformation’), the condition is empty: for any two proper poses and any scale there is a rotation, translation and scaling carrying one to the other. The condition only constrains anything because all classifiers of a scene share one viewpoint, hence one transformation.
What the change does
The transformation is now the one fixed by π and ρ*, so the constraint bites: with all classifiers of a scene under the same π, distances scale by σ(π) and relative orientations are preserved. This reading is equivalent to (85) (Lean: projStatic_iff; exists_sim_of_valid shows the plain existential is vacuous; sim_unique gives uniqueness).
Anything else affected?No other change: footnote 64 is a suggestion for future work and nothing later depends on it.
Judgment call: the wording of this replacement is ours and not checked in Lean. The reading ‘the transformation determined by π and ρ*’ is our reconstruction (the Lean ‘elegant version’), not necessarily what the authors have in mind.
/-- Given the scale, the transformation is unique (for a valid classifier pose). -/theorem sim_unique (cl : Pose) (hcl : cl.Valid) (g g' : Sim) (hs : g.s = g'.s)
(h : g.act cl = g'.act cl) : g = g' := byhave hO := congrArg Pose.O h
have hc := congrArg Pose.c h
simp only [Sim.act] at hO hc
have hQ : g.Q = g'.Q := byhave := congrArg (fun M => M.mul cl.O.T) hO
simp only [M3.mul_assoc, hcl.2.1, M3.mul_one] at this
exact this
obtain ⟨s, hs0, Q, hQ0, t⟩ := g
obtain ⟨s', hs0', Q', hQ0', t'⟩ := g'
simp only at hs hQ
subst hs; subst hQ
simp only [Sim.apply] at hc
have : t = t' := by
...
Related passage in the paperWe could then take a classifier representation to be true of an object just in case there is a certain geometric transformation (based for instance on translations, rotations and scaling) from one to the other.
Statementtransformation of given scale is unique (valid classifier)
/-- Given the scale, the transformation is unique (for a valid classifier pose). -/theorem sim_unique (cl : Pose) (hcl : cl.Valid) (g g' : Sim) (hs : g.s = g'.s)
(h : g.act cl = g'.act cl) : g = g' := byhave hO := congrArg Pose.O h
have hc := congrArg Pose.c h
simp only [Sim.act] at hO hc
have hQ : g.Q = g'.Q := byhave := congrArg (fun M => M.mul cl.O.T) hO
simp only [M3.mul_assoc, hcl.2.1, M3.mul_one] at this
exact this
obtain ⟨s, hs0, Q, hQ0, t⟩ := g
obtain ⟨s', hs0', Q', hQ0', t'⟩ := g'
simp only at hs hQ
subst hs; subst hQ
simp only [Sim.apply] at hc
have : t = t' := byhave hx := congrArg V3.x hc
have hy := congrArg V3.y hc
have hz := congrArg V3.z hc
simpat hx hy hz
ext <;> grind
subst this; rfl
proven
E4ill-posed statement Footnote 64: the transformation should be the one determined by the viewpoint, otherwise ‘there is a transformation’ says nothing (details above)
Not stated in the paper as such — related passage (Greek letters restored from the PDF)
Related passage in the paper(ii) modulo the scaling factor σ(π) (> 0), the position and orientation of d relative to ρ(π) correspond (in terms of coordinates) to the position and orientation of CL relative to ρ*
Statementtwo classifiers under the same pi: squared distances scale by s^2, relative orientation preserved
/-- ... and the relative orientation of two depicted objects is preserved exactly. -/theorem shared_viewpoint_relative_orientation (g : Sim) (cl₁ cl₂ d₁ d₂ : Pose)
(h₁ : g.act cl₁ = d₁) (h₂ : g.act cl₂ = d₂) :
d₁.O.T.mul d₂.O = cl₁.O.T.mul cl₂.O := bysubst h₁ h₂
simp only [Sim.act, M3.T_mul]
rw [M3.mul_assoc, ← M3.mul_assoc g.Q.T, g.hQ.1, M3.one_mul]
proven
E4ill-posed statement Footnote 64: the transformation should be the one determined by the viewpoint, otherwise ‘there is a transformation’ says nothing (details above)
Related passage in the paperThis equivalence captures the fact that the notion of 'viewpoint' is underspecified in this system, as two salient choices correspond to the signer's position and to the addressee's position.
Statementrotating the axes of r* and r(pi) together leaves projection unchanged (static and dynamic)
We could define the very same coordinate system while starting from the addressee's position, say with coordinates (0, 1, 0), and with the x axis extending toward the addressee's left, the y axis toward their back and the z axis upwards.
Suggested replacement
We could define the very same coordinate system while starting from the addressee's position, say with coordinates (0, 1, 0), and with the x axis extending toward the addressee's left, the y axis toward their back and the z axis upwards. (Axes that are natural for the addressee, x toward their right and y toward their front, give the same system rotated by 180 degrees around the z axis; using them requires rotating ρ* and ρ(π) together, since rotating only one of them changes which objects project to which classifiers.)
What the paper does, and why it fails
The sentence is correct as written: the axes described coincide with the signer’s. But it can be read as saying that one may freely switch to the addressee’s natural axes (x to their right, y to their front) for one frame only. That would rotate ρ* by 180 degrees around z without rotating ρ(π), and change the verdict of (85).
What the change does
The added parenthesis says how the addressee’s natural axes relate to the signer’s and that both frames must be rotated together. Rotating both leaves projection unchanged (Lean: projStatic_rot, projDyn_rot, addressee_natural_frame); rotating only one flips the verdict (example_one_sided_change_fails).
Anything else affected?No other change: the underspecification of ‘viewpoint’ mentioned in the same paragraph and footnote 47 (addressee at (0, 10, 0)) are unaffected; footnote 47 should also be read as changing both frames.
Judgment call: the wording of this replacement is ours and not checked in Lean. Optional clarification (our wording); the original statement is not false.
Paper textWe could define the very same coordinate system while starting from the addressee's position, say with coordinates (0, 1, 0), and with the x axis extending toward the addressee's left, the y axis toward their back and the z axis upwards.
Statementpaper's addressee axes (left, back, up) coincide with signer axes; natural (right, front, up) axes are r* rotated 180 degrees about z; verdicts equal
We could define the very same coordinate system while starting from the addressee's position, say with coordinates (0, 1, 0), and with the x axis extending toward the addressee's left, the y axis toward their back and the z axis upwards.
Suggested replacement
We could define the very same coordinate system while starting from the addressee's position, say with coordinates (0, 1, 0), and with the x axis extending toward the addressee's left, the y axis toward their back and the z axis upwards. (Axes that are natural for the addressee, x toward their right and y toward their front, give the same system rotated by 180 degrees around the z axis; using them requires rotating ρ* and ρ(π) together, since rotating only one of them changes which objects project to which classifiers.)
What the paper does, and why it fails
The sentence is correct as written: the axes described coincide with the signer’s. But it can be read as saying that one may freely switch to the addressee’s natural axes (x to their right, y to their front) for one frame only. That would rotate ρ* by 180 degrees around z without rotating ρ(π), and change the verdict of (85).
What the change does
The added parenthesis says how the addressee’s natural axes relate to the signer’s and that both frames must be rotated together. Rotating both leaves projection unchanged (Lean: projStatic_rot, projDyn_rot, addressee_natural_frame); rotating only one flips the verdict (example_one_sided_change_fails).
Anything else affected?No other change: the underspecification of ‘viewpoint’ mentioned in the same paragraph and footnote 47 (addressee at (0, 10, 0)) are unaffected; footnote 47 should also be read as changing both frames.
Judgment call: the wording of this replacement is ours and not checked in Lean. Optional clarification (our wording); the original statement is not false.
Related passage in the paperThis is the viewer position corresponding to that of the signer, but we could equally define a viewer position corresponding to that of the addressee, which would look at the same scene from a position facing the smiley face in (86), say with the addressee's chest in position (0, 10, 0).
Statementchanging only r* (not r(pi)) by 180 degrees breaks the example
Paper textWith this frame of reference, the Dalai Lama is at the center, and thus has coordinates (0, 0, 0), while Obama has coordinates (50, 0, 0). [...] Obama: <uO, vO, wO> = <(0, 1, 0), (-1, 0, 0), (0, 0, 1)> Dalai Lama: <uDL, vDL, wDL> = <(0, -1, 0), (1, 0, 0), (0, 0, 1)>
StatementObama at (50,0,0), classifier at (1,0,0), same orientations: projects with s=50; orientation triples are right-handed
/-- The elegant reading: the similarity is a uniform scaling by 50 about the origin. -/theorem example_obama_sim : projSim True (vp50.toSim idFrame) clObama obama :=
(projStatic_iff _ _ _ _ _).1 example_obama_s50
proven (computed)
E1false statement Example (88)-(89): the scaling factor must be 50, not 1/50, given (85)(ii)a
Location: Section 7.2, (85)(ii)a and example (88)-(89), pp. 33-34 PDF
Paper text
We will assume that the scaling factor is 1/50.
Suggested replacement
We will assume that the scaling factor σ(π) is 50 (since, by (85)(ii)a, the coordinates of the object are σ(π) times those of the classifier).
What the paper does, and why it fails
(85)(ii)a says center(d, ρ(π)) = σ(π) • center(WORD, ρ*): multiplying the classifier’s coordinates by σ(π) gives the object’s. In the example Obama is at x = 50 and the classifier at x = 1, so σ(π) must be 50. With σ(π) = 1/50 the equation of (85)(ii)a fails (1/50 • 1 ≠ 50).
What the change does
The example now agrees with (85)(ii)a, and with the temporal factors in (90)-(91) (5 and 14,400), which already multiply classifier durations to get object durations. Lean: example_obama_s50 (works) and example_obama_paper_scale_fails (1/50 fails).
Anything else affected?No other change: the classifier coordinate (1, 0, 0) in (89)a and the orientations in (88) stay as they are. Alternative fix: keep 1/50 and rewrite (85)(ii)a as center(WORD, ρ*) = σ(π) • center(d, ρ(π)); then (85), footnote 46 and the sentence before (91) would change too.
Text note: σ is written s in the text extraction; the PDF uses σ(π), ρ(π), ρ*, τ(π).
/-- With the scaling applied object -> classifier (as the prose of (89) does), 1/50 is right. -/theorem example_obama_prose_direction :
center clObama idFrame = (1/50 : Rat) • center obama idFrame := bydecide +kernel
E2typo Example after (85): ρ* and ρ(π) are swapped in the prose
Location: Section 7.2, example after (85), p. 34 PDF
Paper text
this is the frame of reference notated as ρ* in (85).
Suggested replacement (Section 7.2, paragraph after (85))
this is the frame of reference notated as ρ(π) in (85).
Paper text
the signer’s frame of reference (notated as ρ(π) in (85)),
Suggested replacement (Section 7.2, paragraph before (89), ‘Finally, Obama and the Dalai Lama project …’)
the signer’s frame of reference (notated as ρ* in (85)),
What the paper does, and why it fails
In (85), ρ* is the signer’s frame of reference and ρ(π) is the real-world (scene) frame determined by the viewpoint π. The prose says the opposite in both places: the scene’s viewpoint frame is called ρ* and the signer’s frame ρ(π).
What the change does
The two labels now match (85), (84b) and (84c), and the later sentence ‘the Obama classifier at (1, 0, 0) in the signer’s frame of reference ρ*’.
Anything else affected?No other change: prose only; the computations in the example are unaffected (Lean uses ρ* as the signer’s frame).
Text note: Greek letters restored from the PDF (the text extraction writes r* and r(π)).
Paper text (Greek letters restored from the PDF)We will assume that the scaling factor is 1/50. Since we conveniently picked our example so that all coordinates are 0 except for the Obama's x-coordinate, which is at x = 50, we only need to revise the latter, putting the Obama classifier at (1, 0, 0) in the signer's frame of reference ρ*
Statementwith (85)(ii)a as written, s = 1/50 does NOT give the example
E1false statement Example (88)-(89): the scaling factor must be 50, not 1/50, given (85)(ii)a
Location: Section 7.2, (85)(ii)a and example (88)-(89), pp. 33-34 PDF
Paper text
We will assume that the scaling factor is 1/50.
Suggested replacement
We will assume that the scaling factor σ(π) is 50 (since, by (85)(ii)a, the coordinates of the object are σ(π) times those of the classifier).
What the paper does, and why it fails
(85)(ii)a says center(d, ρ(π)) = σ(π) • center(WORD, ρ*): multiplying the classifier’s coordinates by σ(π) gives the object’s. In the example Obama is at x = 50 and the classifier at x = 1, so σ(π) must be 50. With σ(π) = 1/50 the equation of (85)(ii)a fails (1/50 • 1 ≠ 50).
What the change does
The example now agrees with (85)(ii)a, and with the temporal factors in (90)-(91) (5 and 14,400), which already multiply classifier durations to get object durations. Lean: example_obama_s50 (works) and example_obama_paper_scale_fails (1/50 fails).
Anything else affected?No other change: the classifier coordinate (1, 0, 0) in (89)a and the orientations in (88) stay as they are. Alternative fix: keep 1/50 and rewrite (85)(ii)a as center(WORD, ρ*) = σ(π) • center(d, ρ(π)); then (85), footnote 46 and the sentence before (91) would change too.
Text note: σ is written s in the text extraction; the PDF uses σ(π), ρ(π), ρ*, τ(π).
/-- With the scaling applied object -> classifier (as the prose of (89) does), 1/50 is right. -/theorem example_obama_prose_direction :
center clObama idFrame = (1/50 : Rat) • center obama idFrame := bydecide +kernel
Paper text (Greek letters restored from the PDF)Finally, Obama and the Dalai Lama project to the classifiers SIT-cla and SIT-clb just in case in the signer's frame of reference (notated as ρ(π) in (85)), the classifiers have the same coordinates modulo the relevant scaling factor as well as the same orientation as the objects they depict.
/-- With the scaling applied object -> classifier (as the prose of (89) does), 1/50 is right. -/theorem example_obama_prose_direction :
center clObama idFrame = (1/50 : Rat) • center obama idFrame := bydecide +kernel
proven (computed)
E1false statement Example (88)-(89): the scaling factor must be 50, not 1/50, given (85)(ii)a
Location: Section 7.2, (85)(ii)a and example (88)-(89), pp. 33-34 PDF
Paper text
We will assume that the scaling factor is 1/50.
Suggested replacement
We will assume that the scaling factor σ(π) is 50 (since, by (85)(ii)a, the coordinates of the object are σ(π) times those of the classifier).
What the paper does, and why it fails
(85)(ii)a says center(d, ρ(π)) = σ(π) • center(WORD, ρ*): multiplying the classifier’s coordinates by σ(π) gives the object’s. In the example Obama is at x = 50 and the classifier at x = 1, so σ(π) must be 50. With σ(π) = 1/50 the equation of (85)(ii)a fails (1/50 • 1 ≠ 50).
What the change does
The example now agrees with (85)(ii)a, and with the temporal factors in (90)-(91) (5 and 14,400), which already multiply classifier durations to get object durations. Lean: example_obama_s50 (works) and example_obama_paper_scale_fails (1/50 fails).
Anything else affected?No other change: the classifier coordinate (1, 0, 0) in (89)a and the orientations in (88) stay as they are. Alternative fix: keep 1/50 and rewrite (85)(ii)a as center(WORD, ρ*) = σ(π) • center(d, ρ(π)); then (85), footnote 46 and the sentence before (91) would change too.
Text note: σ is written s in the text extraction; the PDF uses σ(π), ρ(π), ρ*, τ(π).
/-- With the scaling applied object -> classifier (as the prose of (89) does), 1/50 is right. -/theorem example_obama_prose_direction :
center clObama idFrame = (1/50 : Rat) • center obama idFrame := bydecide +kernel
Related passage in the paperNo scaling factor is applied to the vectors that define orientation, since all vectors are of unit length, and we just need to ensure that the very same triples of vectors define the orientation of the classifiers as the orientation of the individuals they depict
Statementswapping orientations breaks projection though positions match
Not stated in the paper as such — related passage ((§7.2, after (89)), with ρ restored; the example with non-trivial frames is ours)
Related passage in the paperFinally, Obama and the Dalai Lama project to the classifiers SIT-cla and SIT-clb just in case in the signer's frame of reference (notated as ρ(π) in (85)), the classifiers have the same coordinates modulo the relevant scaling factor as well as the same orientation as the objects they depict.
Statementclassifier at absolute (1,0,0), r*=Z-rotated, r(pi) at (10,0,0): lands at (-40,0,0) rotated
Paper text (Greek letters restored from the PDF)if the expression [PERSON-clτ]a moves toward b for a duration of 1 second, and the scaling factor is 5, the condition in (90)(ii) will translate into (91), and will require that for 5 seconds after t, Obama moves toward the Dalai Lama in a way that mirrors the classifier movement.
Statementclassifier moves 1 s, t(pi)=5, s=50: object mirrors movement for 5 s
Paper text (Greek letters restored from the PDF)This is why we posited that a viewpoint π doesn't just make available a spatial scaling factor σ(π), but also a temporal scaling factor τ(π). We can thus require that for each δ' ≤ δ, at t+(τ(π))δ', d projects to word-clτ(δ').
proj(π, t, w, d) = word-cl_τ iff (i) word′_{t,w}(d) = 1, and (ii) for each δ′ ≤ δ, proj(d, π, t+(τ(π))δ′, w) = word-cl_τ(δ′).
Suggested replacement
proj(d, π, t, w) = word-cl_τ iff (i) word′_{t,w}(d) = 1, and (ii) for each δ′ such that 0 ≤ δ′ ≤ δ, proj(d, π, t+(τ(π))δ′, w) = word-cl_τ(δ′).
Further edits
Paper text
proj(π, t, w, Obama) = CL-person_τ
Suggested replacement (Example (91))
proj(Obama, π, t, w) = CL-person_τ
Paper text
(insert)
Suggested replacement (Just after (85)(ii)b (new sentence))
Here center(d, ρ(π)) and orientation(d, ρ(π)) are the position and orientation of d at the time t and in the world w of evaluation.
What the paper does, and why it fails
(1) The left-hand side of (90) and (91) writes proj(π, t, w, d), while (85) and the right-hand side of (90)(ii) write proj(d, π, t, w). (2) The range of δ′ is given as ‘δ′ ≤ δ’ without δ′ ≥ 0 (although the classifier movement is defined on [0, δ]). (3) In (85), center(d, ρ(π)) and orientation(d, ρ(π)) have no time or world argument, but (90) needs the object’s pose at times t + τ(π)δ′.
What the change does
proj has the same argument order everywhere, δ′ ranges over [0, δ] explicitly, and (85) says that positions and orientations are those of the time and world of evaluation, so that (90)(ii) evaluates (85) at the right time. Lean: projDyn, projDyn_iff, example_dynamic.
Anything else affected?No other change to results. Also affects: the prose of Section 7.3 (‘for each δ′ ≤ δ’, twice, before (90)) should carry the same ‘0 ≤ δ′’. Note that (85)(i) must then hold throughout the movement (a sitting person stays sitting).
Text note: Greek letters and subscripts restored from the PDF (page 36); the text extraction writes d’ ≤ d, t(π) and wordt.
theorem projDyn_iff (lex : Rat → Prop) (π : Viewpoint) (rstar : Frame) (dur : Rat)
(cl obj : Rat → Pose) (t : Rat) :
projDyn lex π rstar dur cl obj t ↔
lex t ∧ projDynSim lex (π.toSim rstar) π.ts dur cl obj t := byunfold projDyn projDynSim
constructor
· rintro ⟨h0, h⟩
refine ⟨h0, fun d' a b => ?_⟩
have := (projStatic_iff _ π rstar _ _).1 (h d' a b)
exact this
· rintro ⟨h0, h⟩
refine ⟨h0, fun d' a b => ?_⟩
exact (projStatic_iff _ π rstar _ _).2 (h d' a b)
Paper textThe scaling factor could be huge: if an 8-hour flight is represented by a 2-second movement, the scaling factor is… 14,400 (= (8*60*60) / 2).
Paper text (Greek letters restored from the PDF)suppose that locus a has a z-coordinate of 30cm above the center signing space (of coordinates (0, 0, 0) in the signer's referential r*) [...] If the scaling factor s(σ(π) is 3, the head of s(A) should have a z-coordinate of 3 * 30cm = 90cm, and thus it should be 90cm above the level of a person's chest, so at 2m10
Statementz=0.3, s=3, origin at 1.2 m: head at 2.10 m
/-- the head of s(A) at 2.10 m qualifies; orientation is irrelevant (trivialized). -/theorem example_locus : projLocus True vpLocus idFrame locusA headS := byrefine ⟨trivial, ?_⟩; decide +kernel
Paper textThird, classifier predicates as well as real world objects will be assumed to come with a distinguished point, which we will call their 'center', and a distinguished 'orientation', encoded by way of three orthogonal vectors of unit length (i.e. an orthonormal basis; here too, we restrict attention to right-handed ones).
Statementno similarity maps a right-handed pose onto a left-handed one (mirror) or onto non-unit triple
theorem no_sim_to_mirror_pose :
¬ ∃ g : Sim, g.act ⟨0, M3.one⟩ = ⟨0, M3.diag 11 (-1)⟩ := by
rintro ⟨g, h⟩
have := congrArg Pose.O h
simp only [Sim.act, M3.mul_one] at this
have hd := g.hQ.2.2
rw [this] at hd; revert hd; decide +kernel
/-- Likewise a non-unit "orientation triple" (orthogonal but not normalized). -/theorem no_sim_to_nonunit_pose :
¬ ∃ g : Sim, g.act ⟨0, M3.one⟩ = ⟨0, M3.diag 222⟩ := by
rintro ⟨g, h⟩
have := congrArg Pose.O h
simp only [Sim.act, M3.mul_one] at this
have hd := g.hQ.2.2
rw [this] at hd; revert hd; decide +kernel
(ii) a (right-handed) triple of orthogonal vectors of unit length that encode the orientation of d.
Suggested replacement (after the sentence ‘… of the form <u, v, w>, where u is a triple of coordinates of a unit-length vector, and similarly for v and w.’ in (84a)(ii) (before footnote 45’s continuation), as a new sentence in the same item)
Note that (85) itself only compares coordinates. The requirement that the triples be right-handed and orthonormal matters if projection is later reformulated as the existence of a rotation, translation and scaling taking the classifier to the object (footnote 64): no such transformation maps a right-handed orthonormal triple onto a left-handed or non-unit one.
What the paper does, and why it fails
(84a)(ii) requires the orientation to be a right-handed triple of orthogonal unit vectors, but nothing in (85) uses this: (85)(ii)b just compares two triples for equality, and makes sense for arbitrary triples. The requirement only matters for the footnote-64 reading (a transformation carrying classifier to object).
What the change does
The inserted note says where the requirement is actually needed. Left-handed objects (mirror images) can never project on a right-handed classifier under the transformation reading. Lean: no_sim_to_mirror_pose, no_sim_to_nonunit_pose, exists_sim_of_valid; projStatic_iff holds for all poses.
Anything else affected?No other change: (85) is unaffected. Mirror-image objects are not handled by the transformation reading.
Judgment call: the wording of this replacement is ours and not checked in Lean. This is an optional clarifying sentence (mine); (85) needs no correction.
theorem no_sim_to_mirror_pose :
¬ ∃ g : Sim, g.act ⟨0, M3.one⟩ = ⟨0, M3.diag 11 (-1)⟩ := by
rintro ⟨g, h⟩
have := congrArg Pose.O h
simp only [Sim.act, M3.mul_one] at this
have hd := g.hQ.2.2
rw [this] at hd; revert hd; decide +kernel
/-- Likewise a non-unit "orientation triple" (orthogonal but not normalized). -/theorem no_sim_to_nonunit_pose :
¬ ∃ g : Sim, g.act ⟨0, M3.one⟩ = ⟨0, M3.diag 222⟩ := by
rintro ⟨g, h⟩
have := congrArg Pose.O h
simp only [Sim.act, M3.mul_one] at this
have hd := g.hQ.2.2
rw [this] at hd; revert hd; decide +kernel
Paper textit would be more standard and elegant to define orientation as a triple of angles, as this suffices to characterize the triple of orthogonal vectors associated with the object
StatementEuler-angle parametrization of rotations
Lean statementnot formalized
not formalized
Why not formalized: A suggestion in a footnote (fn 45) to reparametrize orientation by angles. The Lean development uses rotation matrices instead; relating the two parametrizations (Euler angles to rotation matrices) was not done.
E9overclaim Footnote 45: a triple of angles is not a unique parametrization of orientation (details above)
A1suggested new result
Two projected classifiers determine the viewpoint
Statement to add (§7.2, right after (85)/(86) or after fn 64 (p. 33), as a remark on why a viewpoint may be shared by several classifiers in one scene.)
Fix the signer's frame r*. Suppose two classifiers cl₁, cl₂ with distinct centers (cl₁ with an orthonormal, right-handed orientation triple) are projected onto objects d₁, d₂ under a viewpoint π, and also under a viewpoint π′. Then s(π) = s(π′) and r(π) = r(π′) (same origin, same axes). In particular one classifier cannot fix s(π), but two classifiers with distinct centers fix (r(π), s(π)) completely; t(π) is not constrained by the spatial clause.
Why it is useful
Explains that the scaling s(π) and frame r(π) are recoverable from the depicted scene, so multi-classifier scenes are not free to choose different viewpoints per classifier. Turns fn 64's remark about a single transformation into a precise uniqueness statement.
Proof idea
By the similarity reformulation both viewpoints give similarities carrying cl₁, cl₂ to d₁, d₂. Squared distance between the objects is s² times that between the classifiers, so s² = s′² (nonzero distance), hence s = s′ as both are positive. With the scale fixed a similarity is unique given a valid classifier pose, and (frame, scale) ↔ similarity is a bijection given r*, so r(π) = r(π′).
FidelityFaithful to the reconstructed similarity version (Rat instead of R, lexical condition abstracted as a proposition, worlds suppressed). The lexical conjuncts play no role. Hypothesis that cl₁ is valid is needed for uniqueness (pose orthonormality is only stated in words in the paper).
When two classifiers can share one viewpoint: an intrinsic criterion
Statement to add (§7.2 after (89) (p. 35), or as a footnote to fn 64, to characterize which multi-classifier scenes are describable with one π.)
Let cl₁, cl₂ be classifiers and d₁, d₂ objects (orientation triples of cl₁ and d₁ orthonormal right-handed), and s > 0. Some single viewpoint (equivalently some similarity) with spatial scale s projects cl₁ onto d₁ and cl₂ onto d₂ iff (a) the relative orientation is preserved: orientation(d₁,d₂ frame) = orientation(cl₁,cl₂ frame), i.e. O(d₁)ᵀ O(d₂) = O(cl₁)ᵀ O(cl₂), and (b) the displacement from center 1 to center 2, read in each first object's own axes, is scaled by s: O(d₁)ᵀ(c(d₂) − c(d₁)) = s · O(cl₁)ᵀ(c(cl₂) − c(cl₁)).
Why it is useful
Gives a checkable, coordinate-free criterion (no reference to r*, r(π)) for whether a two-classifier depiction is coherent, and shows that the shared-viewpoint constraints (scaled distances, preserved relative orientation) are jointly sufficient, not merely necessary.
Proof idea
Necessity: apply the similarity and use that rotations preserve dot products and cancel with their transposes. Sufficiency: build the rotation Q = O(d₁)O(cl₁)ᵀ and the translation that sends cl₁ to d₁; conditions (a) and (b) then give Q·O(cl₂) = O(d₂) and s·Q·(c₂ − c₁) = d₂ − d₁. Validity of cl₂ and d₂ is not needed.
FidelityStates the existence of a similarity of scale s; by the paper's reformulation (projStatic_iff, toViewpoint_toSim) this is a viewpoint for any r*. Extends the existing necessary-only shared_viewpoint_distance / relative_orientation to an iff; the intrinsic form (body-axes displacement) is our formulation.
theorem shared_viewpoint_iff (cl₁ cl₂ d₁ d₂ : Pose)
(h₁ : cl₁.Valid) (k₁ : d₁.Valid) (s : Rat) (hs : 0 < s) :
(∃ g : Sim, g.s = s ∧ g.act cl₁ = d₁ ∧ g.act cl₂ = d₂) ↔
d₁.O.T.mul d₂.O = cl₁.O.T.mul cl₂.O ∧ bodyDisp d₁ d₂ = s • bodyDisp cl₁ cl₂ := byconstructor
· rintro ⟨g, rfl, e1, e2⟩
refine ⟨shared_viewpoint_relative_orientation g cl₁ cl₂ d₁ d₂ e1 e2, ?_⟩
have hc := act_c_sub g cl₁ cl₂
rw [e1, e2] at hc
have ho : d₁.O = g.Q.mul cl₁.O := byrw [← e1]; rflunfold bodyDisp
rw [hc, ho, M3.T_mul, M3.mulV_smul, ← M3.mul_mulV, M3.mul_assoc, g.hQ.1, M3.mul_one]
· rintro ⟨ho, hd⟩
let Q := d₁.O.mul cl₁.O.T
have hQ : IsRot Q := k₁.mul h₁.T
let g : Sim := ⟨s, hs, Q, hQ, d₁.c - s • Q.mulV cl₁.c⟩
...
A3suggested new result
Dynamic projection scales speeds by s(π)/t(π)
Statement to add (§7.3 after (91) (p. 36), as a general remark on the example: s=50, t(π)=5 gives a speed factor of 10.)
If proj(d, π, t, w) = word-cl(d) holds dynamically as in (90), then for any two classifier times a ≠ b in [0,d], (distance between the object at times t+t(π)a and t+t(π)b)/(elapsed time) = (s(π)/t(π)) × (distance between the classifier at a and b)/(b − a), i.e. the depicted object moves s(π)/t(π) times as fast as the classifier (squared speeds scale by (s/t)²).
Why it is useful
Makes the interplay of the spatial and temporal scalings of (84b) explicit: speed ratio is a derived quantity, which is what the flight example (8 h vs 2 s) really constrains.
Proof idea
By dynamic equivalence all classifier poses are carried by one similarity of scale s, so squared displacement between two times scales by s². The real-time gap is t(π)(a−b), so squared speed scales by s²/t(π)².
FidelityStated for squared average speed (avoids square roots over Rat); the square-root form follows by positivity. Time is Rat, worlds suppressed. Fairly elementary corollary; include only if the author wants a remark on speed.