# RESULTS: geometric part of "Iconological Semantics" (Schlenker & Lamberton 2024)

All Lean in `lean/IconologicalGeometry.lean` (checked by `lean/check.sh`, no `sorry`).
Page references: manuscript page numbers of `source/Iconological-Semantics.pdf`.

## Results table

**Verdict** (does the paper's claim hold?): **confirmed** = holds as stated; **corrected-proof** = statement holds but the paper's proof was wrong or had a gap, repaired in Lean; **modified-statement** = statement as printed is false or ill-posed, a corrected statement is proven; **disconfirmed** = false with no repair; **n/a** = definition, new result of ours, or not formalized. The **Status** column records only the formalization status.


| Result | Paper location | Informal statement | Lean formalization | Lean file:line | Verdict | Status |
|---|---|---|---|---|---|---|
| Original (84)-(85) | §7.2 pp. 32-33 | proj(d,pi,t,w)=WORD iff lexical condition, center(d,r(pi)) = s(pi).center(WORD,r*), orientation(d,r(pi)) = orientation(WORD,r*) | `projStatic` with `Frame`, `Pose`, `center`, `orientation`, `Viewpoint` | IconologicalGeometry.lean:163-207 | n/a | formalized (definition) |
| Original (90) | §7.3 pp. 35-36 | dynamic projection: (i) lexical, (ii) for each d' in [0,d], proj at time t+t(pi)d' to static classifier word-cl(d') | `projDyn` | :210 | n/a | formalized (definition) |
| Right-handed orthonormal triple = rotation | (84a)(ii) p. 32 | a right-handed triple of orthogonal unit vectors is the same as an orthogonal matrix with det 1 | `rightHanded_isRot` | :147 | confirmed | proven |
| Elegant version (reconstruction) | fn 45 p. 33, fn 64 p. 49 | classifier's pose is mapped onto the object's pose by a similarity (scale s>0, rotation, translation) fixed by the viewpoint | `Sim`, `Sim.act`, `projSim`, `Viewpoint.toSim` | :218-250 | n/a | formalized (definition) |
| Static equivalence | (85) vs fn 64 | (85) holds for pi iff `toSim` maps the classifier pose onto the object pose (no assumption on poses) | `projStatic_iff` | :285 | confirmed | proven |
| Viewpoints = similarities | (84b) | every similarity (with any t(pi)>0) comes from a viewpoint and back: (frame, scale) <-> similarity, given r* | `toViewpoint_toSim`, `toSim_toViewpoint_frame` | :310, :321 | confirmed | proven |
| Dynamic equivalence | (90) | (90) iff lex at t and one similarity carries cl(d') to obj(t+t(pi)d') for all d' in [0,d] | `projDyn_iff` | :334 | confirmed | proven |
| Redundancy of (90)(i) | (90) | for d>=0 the condition (i) follows from (ii) | `projDyn_i_redundant` | :350 | n/a | proven |
| Redundancy of lexical conjunct of (53) | p. 35, fn 49 | lex and proj iff proj (two-valued reading) | `lexical_condition_redundant` | :365 | confirmed | proven (trivial; caveat, see Issues 10) |
| Loci: trivialized orientation | App. I-E (128)(ii)b p. 48 | dropping the orientation condition = some locus orientation exists making (127) true | `projLocus`, `projLocus_iff_exists_orientation` | :373, :379 | n/a | proven |
| Composition of transformations | fn 64 | acting by g2 after g1 is acting by the composite | `Sim.act_comp`, `Sim.act_id` | :400, :406 | n/a | proven |
| Inverse / symmetry | fn 64 | projection symmetric: object = g.cl iff cl = g^-1.object | `Sim.inv_act`, `Sim.act_inv`, `projSim_symm` | :415, :424, :435 | n/a | proven |
| Vacuity of unconstrained existential | fn 64 | for valid poses and any scale, some similarity maps classifier to object: "there is a transformation" alone says nothing | `exists_sim_of_valid` | :445 | modified-statement | proven |
| Uniqueness given the scale | fn 64 | transformation of given scale is unique (valid classifier) | `sim_unique` | :455 | n/a | proven |
| Shared viewpoint constrains scenes | (85)-(89) | two classifiers under the same pi: squared distances scale by s^2, relative orientation preserved | `shared_viewpoint_distance`, `shared_viewpoint_relative_orientation` | :479, :492 | n/a | proven |
| Frame-change invariance | p. 31-32, fn 47 | rotating the axes of r* and r(pi) together leaves projection unchanged (static and dynamic) | `toSim_rot`, `projStatic_rot`, `projDyn_rot` | :507, :518, :524 | n/a | proven |
| Signer/addressee coordinate system | p. 32 | paper's addressee axes (left, back, up) coincide with signer axes; natural (right, front, up) axes are r* rotated 180 degrees about z; verdicts equal | `addressee_paper_frame_eq_signer`, `addressee_natural_frame`, `signer_addressee_equivalence` | :545, :549, :554 | modified-statement | proven |
| One-sided frame change flips the verdict | p. 31-32 (remark) | changing only r* (not r(pi)) by 180 degrees breaks the example | `example_one_sided_change_fails` | :625 | n/a | proven (counterexample to a careless reading) |
| Example (88)-(89), s=50 | pp. 34-35 | Obama at (50,0,0), classifier at (1,0,0), same orientations: projects with s=50; orientation triples are right-handed | `obama_valid`, `oOb_rightHanded`, `oDL_rightHanded`, `example_obama_s50`, `example_dalai_s50`, `example_obama_sim` | :581-608 | modified-statement | proven (computed) |
| Example with s=1/50 as printed | p. 34 | with (85)(ii)a as written, s = 1/50 does NOT give the example | `example_obama_paper_scale_fails` | :600 | modified-statement | counterexample |
| Example with prose direction | p. 34 | center(cl) = (1/50).center(d) | `example_obama_prose_direction` | :604 | modified-statement | proven (computed) |
| Orientation matters | (85)(ii)b | swapping orientations breaks projection though positions match | `example_orientation_matters` | :612 | n/a | proven |
| Non-trivial frames | (85) | classifier at absolute (1,0,0), r*=Z-rotated, r(pi) at (10,0,0): lands at (-40,0,0) rotated | `example` (vp₂) | :636 | n/a | proven (computed) |
| Dynamic example (91) | p. 36 | classifier moves 1 s, t(pi)=5, s=50: object mirrors movement for 5 s | `example_dynamic` | :647 | confirmed | proven |
| Dynamic with wrong scale | p. 36 | with t(pi)=1 (91) fails | `example_dynamic_wrong_time_scale` | :654 | modified-statement | proven |
| Flight scaling | p. 35 | 8 h / 2 s = 14,400 | `example` | :661 | confirmed | proven (computed) |
| Locus example (129) | App. I-E p. 49 | z=0.3, s=3, origin at 1.2 m: head at 2.10 m | `example_locus` | :671 | confirmed | proven (computed) |
| Handedness essential | (84a)(ii), fn 64 | no similarity maps a right-handed pose onto a left-handed one (mirror) or onto non-unit triple | `no_sim_to_mirror_pose`, `no_sim_to_nonunit_pose`, `mirror_pose_not_valid` | :684, :693, :704 | modified-statement | counterexample (to unconstrained reading) |
| fn 45 orientation as triple of angles | p. 33 | Euler-angle parametrization of rotations | not formalized | - | n/a | not formalized |

## 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'.

## Issues found in the paper

See TODO.md section B for the full list. Confirmed in Lean:

**E1.** Scale direction: (85)(ii)a needs s=50 for the Obama example, whereas the text uses 1/50 (`example_obama_paper_scale_fails`; s=50 works: `example_obama_s50`). The temporal scaling (5, 14,400) has the direction of (85).

**E2.** r* and r(pi) are swapped in the prose of the example (p. 34).

**E3.** Orthonormality/handedness only stated in words; the elegant reading depends on it (`no_sim_to_mirror_pose`, `no_sim_to_nonunit_pose`); the corrected statement is `exists_sim_of_valid` (valid poses) plus `projStatic_iff` (no assumption).

**E4.** fn 64 read as a plain existential is vacuous (`exists_sim_of_valid`); the transformation must be the one determined by the shared viewpoint (`projSim`, `shared_viewpoint_distance`). With the scale fixed it is unique (`sim_unique`).

**E5.** Signer/addressee: the paper's addressee axes are literally r* (`addressee_paper_frame_eq_signer`); the natural addressee axes are a z-rotation by 180 degrees, and both frames must be changed together (`projStatic_rot`, `example_one_sided_change_fails`).

**E6.** (90): notation clashes (d, t), missing 0<=d', time/world-independent center/orientation, (90)(i) redundant (`projDyn_i_redundant`), proj written as a function though relational.

**E7.** Redundancy of (53)'s lexical conjunct holds only in a two-valued reading (`lexical_condition_redundant`).

## Fidelity notes

- The "elegant version" is OUR reconstruction from fn 45 (orientation as a standard rotation) and fn 64 (transformation between point+frame pairs). It is NOT Philippe Schlenker's Claude-written version, which was not available to us; his may differ in parametrization (e.g. Euler angles, quaternions, existential over transformations). The theorem here says exactly what the equivalence is for the reading "the transformation is the one the viewpoint determines"; the plain existential reading is shown vacuous.
- Ambient absolute coordinates and the split "classifier pose lives in signing space, object pose in the world" are added to make center(d,r), orientation(d,r) definable; the paper leaves them implicit.
- `Rat` replaces R (no Mathlib; the proofs are ring identities). Time is `Rat`. Worlds are suppressed: the lexical condition is a parameter `lex`.
- The lexical predicate word'_{t,w} is abstracted as a proposition; hence (53) redundancy is proved only in that abstraction.
- Objects' poses are functions of time in the dynamic part (`obj`, `cl`), which the paper's (84) does not have (Issue 6).
- Rotation matrices stored by columns so that <u,v,w> is literally the matrix [u v w]; orientation(d,r) = R^T O.
- Not formalized: fn 44 remarks (center/orientation dependent on the word, articulated classifiers), fn 45 angles, Appendix II.
- Axioms: `propext`, `Classical.choice`, `Quot.sound` (from `grind`); numeric checks by kernel evaluation.