← the fiber · the atlas

three theorems, paired

each theorem twice: once for the compiler, once for the mind · house rule: no lemma without its intuition

All Lean below is quoted verbatim from MMCH.lean (533 lines) and compiles: lake env lean MMCH.lean · exit 0 · zero sorries · axioms: propext, Classical.choice, Quot.sound · Mathlib d6f48e4, Lean v4.29.0-rc1

theorem 1 · the hat-box identity

For all real θ:   cos²(θ/2) = (1 + cos θ)/2.
Intuition. A qubit prepared at polar angle θ on the Bloch sphere answers the question “excited or not?” with probability cos²(θ/2) — the Born rule. The right-hand side is the normalized height. So Born probability for a single qubit is literally a height coordinate, and Archimedes’ hat-box theorem — the area between two slices of a sphere depends only on their separation, never their position — is why probability is flat in this coordinate: state space has no crowding anywhere in p. This one-line trigonometric identity is the entry point of the entire geometry: the quantum rule that looks postulated is a cap’s area looking back at you. What it does not prove: that nature samples uniformly — that is the open dynamical clause, and the file says so.
theorem hatbox_identity (θ : ℝ) :
    Real.cos (θ / 2) ^ 2 = (1 + Real.cos θ) / 2 := by
  have h : Real.cos θ = 2 * Real.cos (θ / 2) ^ 2 - 1 := by
    have h2 := Real.cos_two_mul (θ / 2)
    have hθ : 2 * (θ / 2) = θ := by ring
    rw [hθ] at h2
    exact h2
  linarith

theorem 2 · the fixed set of the swap is a circle, not the torus

On S³ = {(z,w) : ‖z‖²+‖w‖²=1}, the fixed-point set of the outcome swap (z,w) ↦ (w,z) is the diagonal great circle {(z,z) : ‖z‖² = ½} — and the Clifford torus contains a point the swap moves.
Intuition. This is the compiler killing its founder’s claim. The working group’s charter asserted the canonical measurement cut (the Clifford torus, |c_g|=|c_e|=1/√2) was the fixed-point set of the ground ↔ excited swap. False: fixed sets of isometries are totally geodesic, and the fixed set here is a mere circle — the states equal in both components. The torus is swap-invariant as a set (the swap shuffles it onto itself) but not pointwise fixed, and the explicit witness (1/√2, i/√2) proves it — on the torus, moved by the swap. Consequence: symmetry alone does not select the cut; the surviving physical selector is the dipole (the operator’s: outcomes are the zero-dipole states; the cut is where the dipole is maximal). A wrong claim, machine-checked into a correct theorem about why it was wrong.
/-- The fixed-point set of the swap on S³ is the diagonal great circle
    {(z,z) : ‖z‖² = 1/2} — a CIRCLE, not the Clifford torus. -/
theorem swap_fixedSet_eq_diagonal :
    {p : ℂ × ℂ | p ∈ sphere3 ∧ swap p = p} =
    {p : ℂ × ℂ | p.1 = p.2 ∧ ‖p.1‖ ^ 2 = 1 / 2} := by
  ext ⟨z, w⟩
  constructor
  · rintro ⟨hs, hfix⟩
    have hwz : w = z := congrArg Prod.fst hfix
    have hs' : ‖z‖ ^ 2 + ‖w‖ ^ 2 = 1 := hs
    rw [hwz] at hs'
    refine ⟨hwz.symm, ?_⟩
    show ‖z‖ ^ 2 = 1 / 2
    linarith
  · rintro ⟨heq, hn⟩
    have heq' : z = w := heq
    have hn' : ‖z‖ ^ 2 = 1 / 2 := hn
    have hw' : ‖w‖ ^ 2 = 1 / 2 := by rw [← heq']; exact hn'
    refine ⟨?_, ?_⟩
    · show ‖z‖ ^ 2 + ‖w‖ ^ 2 = 1
      linarith
    · show swap (z, w) = (z, w)
      simp only [swap]
      rw [heq']

    by the swap. Hence the torus is strictly larger than the fixed set. -/
theorem cliffordTorus_not_pointwise_fixed :
    ∃ p ∈ cliffordTorus, swap p ≠ p := by
  refine ⟨(((1 / Real.sqrt 2 : ℝ) : ℂ), Complex.I * ((1 / Real.sqrt 2 : ℝ) : ℂ)),
    ⟨?_, ?_⟩, ?_⟩
  · show ‖((1 / Real.sqrt 2 : ℝ) : ℂ)‖ = 1 / Real.sqrt 2
    simp
  · show ‖Complex.I * ((1 / Real.sqrt 2 : ℝ) : ℂ)‖ = 1 / Real.sqrt 2
    simp
  · intro hfix
    have h1 : Complex.I * ((1 / Real.sqrt 2 : ℝ) : ℂ) = ((1 / Real.sqrt 2 : ℝ) : ℂ) :=
      congrArg Prod.fst hfix
    have hr : ((1 / Real.sqrt 2 : ℝ) : ℂ) ≠ 0 := by

theorem 3 · the entropy-clock generator identity

Define T(p) = −(2/g)·(p log p + (1−p) log(1−p)). Then on (0,1), for g > 0:   (g/2)·p(1−p)·T″(p) = −1,   with T → 0 at both ends, and T is the unique such solution (the affine kernel dies against the boundary).
Intuition. Model collapse as an unbiased random walk of the excitation probability whose noise is gated by the dipole — strength p(1−p), dying exactly at the decided states, making them absorbing. The mean time to decision then satisfies this ODE, and its unique solution is twice the Shannon entropy of the outcome distribution, per unit noise rate: deciding a maximally uncertain question takes the longest; a foregone conclusion collapses instantly. The logarithm appears for a mechanical reason — the walk crawls near the decided ends, and the traversal cost of near-certainty integrates to −p log p — the same logarithm that measures surprise prices the slow zones. It is a fingerprint, not a law: a flat gate decides the same question faster, which is exactly what makes the entropy-shape falsifiable. Honest boundary: what is machine-checked is the analytic skeleton; the probabilistic identification (that this T is the Wright–Fisher hitting time) is classical stochastic analysis, cited not formalized — the file itself declares the limit:
    OUT OF SCOPE (deliberately not attempted): the stochastic layer — the
    Dynkin / first-passage argument identifying T with the expected hitting
    time of {0,1} for the Wright–Fisher diffusion dp = √(g·p(1−p)) dW.
    Mathlib (2026-07) has Itô integrals but no Dynkin formula, no
    first-passage theory, and no 1-D diffusion boundary classification;
    formalizing that layer is a research project, not an afternoon. The
    probabilistic content stays [VERIFIED-NUM] (experiments/entropy_clock.py);
    what is machine-checked here is exactly the analytic skeleton.          -/

/-- The entropy clock: mean collapse time T(p) = -(2/g)·(p log p + (1−p) log(1−p)). -/
noncomputable def entropyClock (g p : ℝ) : ℝ :=
  -(2 / g) * (p * Real.log p + (1 - p) * Real.log (1 - p))

/-- THE GENERATOR IDENTITY (C7/Result-1 analytic core):
    (g/2)·p·(1−p)·T″(p) = −1 on (0,1). -/
theorem entropyClock_generator (g : ℝ) (hg : 0 < g) {p : ℝ} (h0 : 0 < p) (h1 : p < 1) :
    g / 2 * (p * (1 - p)) * deriv (deriv (entropyClock g)) p = -1 := by
  rw [entropyClock_deriv2 g hg h0 h1]
  have hp1 : (0 : ℝ) < 1 - p := by linarith
  field_simp

what is not here

No claim that nature runs the dipole gate (that is an experiment: outcome statistics are provably gate-blind; timing is not). No stochastic formalization (Mathlib lacks Dynkin/first-passage; saying otherwise would be a lie the compiler cannot catch). No physics words inside the Lean — atoms live in the intuition blocks only, by house rule.

a margin artifact of the jacobian conjectures · theorems compiled 2026-07-26, page 2026-07-27 · paired-artifact rule: no lemma without its intuition; no intuition without its lemma