jcreedcmu

Sea snakes and leporids are undoubtedly the most wondrous and persistent creatures. Wondrous because no one has ever seen them alive, because they don't actually exist, and yet much sorrow is sacrificed to them; and persistent because they have been definitively relegated to the realm of fable a hundred times over, because in hundreds of cases the most capable breeders and also extremely serious researchers have devoted themselves specifically to breeding sea snakes for years and never achieved their goal; but the leporids, like a hydra, always manage to rise again. Do leporids exist? We want to address this question once more for a change, even though our situation today is exactly the same as it was 15 or 20 years ago, i.e., Leporids, according to our current understanding, exist only in the imagination. It may well be that successes in breeding will one day force us to revise our understanding, but this will certainly happen sooner than when definitive, irrefutable publications are available. For science a

jcreedcmu

This cost $5.43 This cost $3

This cost $5.43 This cost $

jcreedcmu

$x$
$\$$
$\\\$$

jcreedcmu

$x$
$\$$
$\\\$$

jcreedcmu

import Mathlib

class Grph (G : Type) where
  edge : G → G → Prop
open Grph

variable {G H : Type} [Grph G] [Grph H]

structure Hom (G H : Type) [Grph G] [Grph H] where
  obj : G → H

jcreedcmu

import Mathlib

/--
Do one collatz iteration
-/
def collatz (n : Nat) := 
  if n % 2 == 0 then n / 2 else 3 * n + 1

/-
Algorithmic collatz termination

jcreedcmu

{-# OPTIONS --cubical #-}

open import Cubical.Foundations.Prelude
open import Cubical.HITs.S1

module Braids1 where

{-

 Conjecture:

jcreedcmu

Let's say a function
    j : ∏(X : 𝒰). (S¹ → X) → (X → X)
is (binary relationally) parametric just in case we have
    ∏(X₁ : 𝒰). ∏(X₂ : 𝒰). ∏(R : X₁ → X₂ → U).
    ∏(η₁ : S¹ → X₁). ∏(η₂ : S¹ → X₂). (∏(s : S¹). R (η₁ s) (η₂ s)) →
    ∏(x₁ : X₁). ∏(x₂ : X₂). R x₁ x₂ →
    R (j X₁ η₁ x₁) (j X₂ η₂ x₂)
Then we can pick an arbitrary function x : X₁ → X₂ and let R be f's graph
    R x₁ x₂ ⇔ f x₁ ≡ x₂
and we obtain

jcreedcmu

cat <<"EOF" >input.txt
[ Rupert ]
(a1,b1,c1,a2,b2,c2)
0
(E a1)(E b1)(E c1) (E a2)(E b2)(E c2) [
8 a1^3 a2 b2 c1 + 8 a1 a2 b1^2 b2 c1 + 8 a1^3 b2^2 c1 + 8 a1 b1^2 b2^2 c1 + 8 a1 a2 b2 c1^3 + 8 a1 b2^2 c1^3 - 8 a1^3 a2 b1 c2 - 8 a1 a2 b1^3 c2 - 8 a1^3 b1 b2 c2 - 8 a1 b1^3 b2 c2 - 8 a1^3 b2 c1 c2 - 8 a1 b1^2 b2 c1 c2 - 8 a1 a2 b1 c1^2 c2 - 8 a1 b1 b2 c1^2 c2 - 8 a1 b2 c1^3 c2 + 8 a1^3 b1 c2^2 + 8 a1 b1^3 c2^2 + 8 a1 b1 c1^2 c2^2 - 8 a1^3 a2 b1 + 8 a1^2 a2^2 b1 - 8 a1 a2 b1^3 + 8 a2^2 b1^3 + 8 a1^3 b1 b2 - 8 a1^2 a2 b1 b2 + 8 a1 b1^3 b2 - 8 a2 b1^3 b2 + 8 a1^3 a2 c1 - 8 a1^2 a2^2 c1 + 8 a1 a2 b1^2 c1 - 8 a2^2 b1^2 c1 - 8 a1^2 b2^2 c1 - 8 b1^2 b2^2 c1 - 8 a1 a2 b1 c1^2 + 8 a2^2 b1 c1^2 + 8 a1 b1 b2 c1^2 - 8 a2 b1 b2 c1^2 + 8 a1 a2 c1^3 - 8 a2^2 c1^3 - 8 b2^2 c1^3 + 8 a1^2 b1 b2 c2 + 8 b1^3 b2 c2 + 8 a1^3 c1 c2 - 8 a1^2 a2 c1 c2 + 8 a1 b1^2 c1 c2 - 8 a2 b1^2 c1 c2 - 8 a1^2 b2 c1 c2 - 8 b1^2 b2 c1 c2 + 8 b1 b2 c1^2 c2 + 8 a1 c1^3 c2 - 8 a2 c1^3 c2 - 8 b2 c1^3 c2 + 8 a1^2 b1 c2^2 + 8 b1^3 c2^2 + 8 b1 c1^2 c2^2 + 8 a1

jcreedcmu

import re

def mat_of_quat(quat):
    [r, a, b, c] = quat
    H.<i,j,k> = QuaternionAlgebra(SR,-1,-1)
    N.<x,y,z> = QQ[]
    q = r + a * i + b * j + c * k
    qs = r - a * i - b * j - c * k
    m = q * (x * i + y * j + z * k) * qs
    return Matrix([[m[i+1].coefficient(v) for v in [x,y,z]] for i in range(3)])