# Lean development: geometric part of Iconological Semantics

Single self-contained file `IconologicalGeometry.lean` (Lean 4, core only, no Mathlib;
reals replaced by `Rat`; all proofs are ring identities so this is immaterial).
Run `./check.sh` (type-checks, rejects `sorry`/`axiom`, prints axioms of the main theorems:
only `propext`, `Classical.choice`, `Quot.sound`, from `grind`; numeric examples use
`decide +kernel`).

Layout
1. Linear algebra on `Rat^3` (`V3`, `M3` stored by columns, `IsRot` = orthogonal with det 1;
   `rightHanded_isRot`: the paper's "right-handed orthonormal triple" is exactly `IsRot`).
2. ORIGINAL: `Frame`, `Pose`, `center`, `orientation` (84), `Viewpoint` (84b), `projStatic` (85),
   `projDyn` (90), written as literally as possible.
3. ELEGANT (our reconstruction from fn. 45 / fn. 64, NOT Schlenker's Claude output):
   `Sim` (uniform scaling, rotation, translation), `projSim`: classifier pose is carried onto
   the object pose by one similarity determined by the viewpoint. `Viewpoint.toSim`,
   `Sim.toViewpoint`, `projDynSim`.
4. Equivalences: `projStatic_iff`, `toViewpoint_toSim` (viewpoints = similarities),
   `projDyn_iff`, `projDyn_i_redundant`, `lexical_condition_redundant`,
   `projLocus_iff_exists_orientation`.
5. Easy consequences: composition, inverse, symmetry, vacuity of the unconstrained existential
   reading of fn. 64 (`exists_sim_of_valid`), uniqueness, same-viewpoint constraints,
   frame-change invariance and the signer/addressee equivalence (`rotZ180`).
6. Worked examples (86)-(89), (91), (129), by computation over `Rat`.
7. Counterexamples (mirror/non-unit orientation).

See `../RESULTS.md` for the table of results with line numbers and `../TODO.md` for the
extraction of the paper's definitions and the issues found.