The harmonic carries no resistance

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 harmonic point is the one that never had any: at the fixed point the resistance is zero before any folding, which is what makes it the edge rather than a side.

Proposition

resistance 5 = 0

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_harmonic_carries_no_resistance

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 sides are equal and exchanged
• The coin is two sides and one edge
• Every bit of resistance drains
• The whole surface sums to zero
• The drain is exact at every scale

All machine-checked theorems