The sides are equal and exchanged

NOT A NOVELTY CLAIM. This is a machine-checked formalisation, checked by the Lean 4 kernel and depending on no axiom. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.

The first form of this said `∀ d ∈ below, σ d ∈ above` — membership as the PREDICATE — and the kernel reported it dependent on propext and Quot.sound. The axiom-freedom gate refused it, and the restatement is stronger for it: naming the image list says WHICH element goes where, not merely that each lands somewhere on the other side.

Proposition

below.length = above.length ∧ below.map σ = above.reverse ∧ above.map σ = below.reverse

Proof

By decide in coin.lean. Checked by the Lean kernel: it depends on no axiom.

Sources and identifiers

• Lean source · src/pair/formal/proofs/coin.lean
• Typeset paper · src/research/lean-theorems.tex
• Repository deposit · doi:10.5281/zenodo.21787144
• Author · ORCID 0009-0000-7312-9778
• Deposit record · coin--the_sides_are_equal_and_exchanged

Proved in the same file

• The coin is an involution
• The harmonic is the only fixed point
• All that is not harmonic is moved
• The coin is two sides and one edge
• Every bit of resistance drains
• The harmonic carries no resistance
• The whole surface sums to zero
• The drain is exact at every scale

All machine-checked theorems