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)

jcreedcmu

Claim: there's a bijection between prime ideals of a commutative ring R

(I is a prime ideal of R iff:
 (1) (I, +) is a subgroup of (R, +)
 (2) if r ∈ R and x ∈ I, then rx ∈ I
 (3) if ab ∈ I, then a ∈ I or b ∈ I
 (4) 1 ∉ I)

and maps f : R → 2 s.t.
(a) f(0) = 0

jcreedcmu

module PredArith where

data void : Set where

abort : {A : Set} → void → A
abort ()

postulate
  ι : Set

jcreedcmu

hg log -r 'FIREFOX_BETA_127_END::FIREFOX_128_0b1_RELEASE' --template "{rev}: {node|short} {date|isodate} {author|person} {desc|firstline}\n"

820035: 2738f5657419 2024-06-03 14:51 +0000 Mozilla Releng Treescript No bug - tagging 5d25cb332db85c8bb2cda40840be406437ec5e98 with FIREFOX_RELEASE_127_BASE a=release DONTBUILD CLOSED TREE
823723: f0900bab4570 2024-06-10 14:49 +0000 Mozilla Releng Treescript Merge old head via |hg debugsetparents af9948205327480d29bfcb960d5308ad4a2d0ce7 2738f5657419fba3ece0bc829732f8dfdce7c70a| CLOSED TREE DONTBUILD a=release
823724: 326824a2c3a7 2024-06-10 14:49 +0000 Mozilla Releng Treescript Preserve old tags after debugsetparents. CLOSED TREE DONTBUILD a=release
823725: 4926489e7390 2024-06-10 14:49 +0000 Mozilla Releng Treescript No bug - tagging 2738f5657419fba3ece0bc829732f8dfdce7c70a with FIREFOX_BETA_127_END a=release DONTBUILD CLOSED TREE
823726: 15a675544fcb 2024-06-10 14:49 +0000 Mozilla Releng Treescript no bug - Bumping Firefox l10n changesets r=release a=l10n-bump CLOSED

jcreedcmu

// A quick and dirty lil implementation of the CVM algorithm
// (https://arxiv.org/pdf/2301.10191)
//
// I put Moby Dick (https://www.gutenberg.org/cache/epub/2701/pg2701.txt) 
// into /tmp/mb.txt

const fs = require('fs');
const mb = fs.readFileSync('/tmp/mb.txt', 'utf8')
      .replace(/[^a-zA-Z-’]/g, ' ')
      .split(/\s+/);