Finsler–Hadwiger theorem

TheoremFinsler–Hadwiger theorem#✓fully proved

Let \(A, B, C, D, E, F, G\) be points of the Euclidean plane \(\mathbb{R}^2\) with \(B \ne A\) and \(E \ne A\), and let \(\rho(x, y) = (-y, x)\) be the counterclockwise rotation by \(90^\circ\). Suppose that \(ABCD\) and \(AEFG\) are squares sharing the vertex \(A\), in the sense that \(D - A = \rho(B - A)\), \(C = B + D - A\), \(G - A = \rho(E - A)\) and \(F = E + G - A\). Let \(O_1 = (A + C)/2\) and \(O_2 = (A + F)/2\) be their centers, and let \(P = (B + G)/2\) and \(Q = (D + E)/2\). Then \(\|P - Q\| = \|O_1 - O_2\|\), the vectors \(P - Q\) and \(O_1 - O_2\) are orthogonal, and \(O_1 + O_2 = P + Q\); that is, the segments \(O_1O_2\) and \(PQ\) have equal length, are perpendicular and share their midpoint.

The hypotheses \(B \ne A\) and \(E \ne A\) are not used. When \(B = E\) both segments are zero; with \(B \ne E\) one also gets \(O_1 \ne O_2\), so that \(O_1 P O_2 Q\) is a square as in the source.

MetaMathlibExt.finsler_hadwiger · 18 lines

theorem finsler_hadwiger :
    ∀ (A B C D E F G O1 O2 P Q : EuclideanSpace ℝ (Fin 2)),
      B ≠ A →
      E ≠ A →
      (D - A).ofLp 0 = -((B - A).ofLp 1) →
      (D - A).ofLp 1 = (B - A).ofLp 0 →
      C = B + D - A →
      (G - A).ofLp 0 = -((E - A).ofLp 1) →
      (G - A).ofLp 1 = (E - A).ofLp 0 →
      F = E + G - A →
      O1 = (2 : ℝ)⁻¹ • (A + C) →
      O2 = (2 : ℝ)⁻¹ • (A + F) →
      P = (2 : ℝ)⁻¹ • (B + G) →
      Q = (2 : ℝ)⁻¹ • (D + E) →
      ‖P - Q‖ = ‖O1 - O2‖ ∧
        ((P - Q).ofLp 0 * (O1 - O2).ofLp 0 +
          (P - Q).ofLp 1 * (O1 - O2).ofLp 1 = 0) ∧
        O1 + O2 = P + Q

Sources

• https://en.wikipedia.org/wiki/Finsler%E2%80%93Hadwiger_theorem.

TheoremFinsler–Hadwiger theorem for distinct squares#✓fully proved

Let \(A, B, C, D, E, F, G\) be points of the Euclidean plane \(\mathbb{R}^2\) with \(B \ne E\), and let \(\rho(x, y) = (-y, x)\) be the counterclockwise rotation by \(90^\circ\). Suppose that \(ABCD\) and \(AEFG\) are squares sharing the vertex \(A\), in the sense that \(D - A = \rho(B - A)\), \(C = B + D - A\), \(G - A = \rho(E - A)\) and \(F = E + G - A\). Let \(O_1 = (A + C)/2\) and \(O_2 = (A + F)/2\) be their centers, and let \(P = (B + G)/2\) and \(Q = (D + E)/2\). Then \(\|P - Q\| = \|O_1 - O_2\|\), the vectors \(P - Q\) and \(O_1 - O_2\) are orthogonal, \(O_1 + O_2 = P + Q\) and \(O_1 \ne O_2\); so the segments \(O_1O_2\) and \(PQ\) are nonzero, equal, perpendicular and share their midpoint, and \(O_1 P O_2 Q\) is a square.

The points \(B\) and \(E\) may equal \(A\): if, say, \(E = A\), then \(AEFG\) is the single point \(A\) and \(O_1 P O_2 Q\) is a quarter of \(ABCD\).

theorem finsler_hadwiger_of_ne (A B C D E F G O1 O2 P Q : EuclideanSpace ℝ (Fin 2))
    (hBE : B ≠ E)
    (hD0 : (D - A).ofLp 0 = -((B - A).ofLp 1)) (hD1 : (D - A).ofLp 1 = (B - A).ofLp 0)
    (hC : C = B + D - A)
    (hG0 : (G - A).ofLp 0 = -((E - A).ofLp 1)) (hG1 : (G - A).ofLp 1 = (E - A).ofLp 0)
    (hF : F = E + G - A)
    (hO1 : O1 = (2 : ℝ)⁻¹ • (A + C)) (hO2 : O2 = (2 : ℝ)⁻¹ • (A + F))
    (hP : P = (2 : ℝ)⁻¹ • (B + G)) (hQ : Q = (2 : ℝ)⁻¹ • (D + E)) :
    ‖P - Q‖ = ‖O1 - O2‖ ∧
      ((P - Q).ofLp 0 * (O1 - O2).ofLp 0 +
        (P - Q).ofLp 1 * (O1 - O2).ofLp 1 = 0) ∧
      O1 + O2 = P + Q ∧ O1 ≠ O2

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.