The sides are equal and exchanged

NOT A NOVELTY CLAIM. This is a machine-checked formalisation, decided 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.

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. The kernel reduces the proposition and reports no axiom dependency.

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