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)])

jcreedcmu

import Mathlib

theorem good_enough (f : ℝ → ℝ) (c : Continuous f) 
  (onRats : (y : ℚ) → f y ≥ 0) : (x : ℝ) → f x ≥ 0 :=
   by 
    by_contra px; push_neg at px; 
    let ⟨x, hx⟩ := px 
    let openset := {y : ℝ | y < 0}
    have hin : f x ∈ openset := hx
    have hio : IsOpen (f ⁻¹' openset) := c.isOpen_preimage openset (isOpen_gt' 0)