text:
Inference with Sets in Type Theory

It’s been quite a while since I did any meaningful writing on type theory. I spent a lot of time introducing the basic concepts, and trying to explain the intuition behind them. I also spent some time describing what I think of as the platform: stuff like arity theory, which we need for talking about type construction. But once we move beyond the basic concepts, I ran into a bit of a barrier – no so much in understanding type theory, but in finding ways of presenting it that will be approacha ble.

I’ve been struggling to figure out how to move forward in my exploration of type theory. The logical next step is working through the basics of intuitionistic logic with type theory semantics. The problem is, that’s pretty dry material. I’ve tried to put together a couple of approaches that skip over this, but it’s really necessary.

For someone like me, coming from a programming language background, type theory really hits its stride when we look at type systems and particularly type inference. But you can’t understand type inference without understanding the basic logic. In fact, you can’t describe the algorithm for type inference without referencing the basic inference rules of the underlying logic. Type inference is nothing but building type theoretic proofs based on a program.

So here we are: we need to spend some time looking at the basic logic of type theory. We’ve looked at the basic concepts that underlie the syntax and semantics, so what we need to do next is learn the basic rules that we use to build logical statements in the realm of type theory. (If you’re interested in more detail, this is material from chapter 5 of “Programming in Martin-Löof’s Type Theory”, which is the text I’m using to learn this material.)

Martin Löoff’s type theory is a standard intuitionistic predicate logic, so we’ll go through the rules using standard sequent notation. Each rule is a sequence which looks sort-of like a long fraction. The “numerator” section is a collection of things which we already know are true; the “denominator” is something that we can infer given those truths. Each statement has the form $A[\Gamma]$, where A is a statement, and B is a set of assumptions. For example, $F(a) [a \in A, \Delta]$ means that $F(a)$ is true, provided we’re in a context that includes $a \in A$.

Personally, I find that this stuff feels very abstract until you take the logical statements, and interpret them in terms of programming. So throughout this post, I’ll do that for each of the rules.

With that introduction out of the way, let’s dive in to the first set of rules.

Simple Introductions

We’ll start off with a couple of really easy rules, which allow us to introduce a variable given a type, or a type given a variable.

Introducing Elements

$\frac{A \,\text{type}}{a \in A \,[a \in A]}$

This is an easy one. It says that if we know that A is a type, then we can introduce the statement that $a \in A$, and add that as an assumption in our context. What this means is also simple: since our definition of type says that it’s only a type if it has an element, then if we know that A is a type, we know that there must be an element of A, and so we can write statements using it.

If you think of this in programming terms, the statement $A \text{type}$ is saying that $A$ is a type. To be a valid type, there must be at least one value that belongs to the type. So you’re allowed to introduce a variable that can be assigned a value of the type.

Introducing Propositions as Types

$\frac{a \in A \, []}{A \, \text{true}}$

This is almost the mirror image of the previous. A type and a true proposition are the same thing in our type theory: a proposition is just a type, which is a set with at least one member. So if we know that there’s a member of the set A, then A is both a type and a true proposition.

Equality Rules

We start with the three basic rules of equality: equality is reflexive, symmetric, and transitive.

Reflexivity

$\frac{a \in A}{a = a \in A}$

$\frac{A \, \text{type}}{A = A}$

If $a$ is an element of a type $A$, then $a$ is equal to itself in type $A$; and if $A$ is a type, then $A$ is equal to itself.

The only confusing thing about this is just that when we talk about an object in a type, we make reference to the type that it’s a part of. This makes sense if you think in terms of programming: you need to declare the type of your variables. “3: Int” doesn’t necessarily mean the same object as “3: Real”; you need the type to disambiguate the statement. So within type theory, we always talk about values with reference to the type that they’re a part of.

Symmetry

$\frac{a = b \in A}{b = a \in A}$

$\frac{A = B}{B = A}$

No surprises here – standard symmetry.

Transitivity

$\frac{a = b \in A \quad b = c \in A}{a = c \in A}$

$\frac{A = B \quad B = C}{A = C}$

Type Equality

$\frac{a \in A \quad A = B}{a \in B}$

$\frac{a = b \in A \quad A = B}{a = b \in B}$

These are pretty simple, and follow from the basic equality rules. If we know that $a$ is a member of the type $A$, and we know that the type $A$ equals the type $B$, then obviously $a$ is also a member of $B$. Along the same lines, if we know that $a=b$ in type $A$, and $A$ equals $B$, then $a=b$ in the type $B$.

Substitution Rules

We’ve got some basic rules about how to formulate some simple meaningful statements in the logic of our type theory. We still can’t do any interesting reasoning; we haven’t built up enough inference rules. In particular, we’ve only been looking at simple, atomic statements using parameterless predicates.

We can use those basic rules to start building upwards, to get to parametric statements, by using substitution rules that allow us to take a parametric statement and reason with it using the non-parametric rules we talked about above.

For example, a parametric statement can be something like $C(x) \, \text{type} [x \in A]$, which says that applying $C$ to a value $x$ which is a member of type $A$ produces a value which is a type. We can use that to produce new inference rules like the ones below.

$\frac{C(x) \, \text{type} [x \in A] \quad a \in A}{C(a) \, \text{type}}$

This says that if we know that given a of type $A$, $C$ will produce a type; and we know that the value $a$ is of type $A$, then $C(a)$ will be a type. In logical terms, it’s pretty straightforward; in programming terms it’s even clearer: if $C$ is a function on type $A$, and we pass it a value of type $A$, it will produce a result. In other words, $C(a)$ is defined for all values of type $A$.

$\frac{C(x) \, \text{type}[x \in A] \quad a = b \in A}{C(a) = C(b)}$

This is even simpler: if $C$ is a function on type $A$, then given two values that are equal in type $A$, $C$ will produce the same result for those values.

Of course, I’m lying a bit. In this stuff, $C$ isn’t really a function. It’s a logical statement; $C(x)$ isn’t quite a function. It’s a logical stamement which includes the symbol $x$; when we say $C(a)$, what we mean is the logical statement $C$, with the object $a$ substituted for the symbol $x$. But I think the programming metaphors help clarify what it means.

Using those two, we can generate more:

$\frac{c(x) \in C(x) [x \in A] \quad a \in A}{c(a) \in C(A)}$

This one becomes interesting. $C(x)$ is a proposition which is parametric in $x$. Then $c(x)$ is a proof-element: it’s an instance of $C(x)$ which proves that $C(X)$ is a type, and we can see $c$ as a computation which, given an element of $a$ produces a instance of $C$. Then what this judgement says is that given an instance $a$ of type $A$, we know that $c(a)$ is an instance of type $C(a)$. This will become very important later on, when we really get in to type inference and quantification and parametric types.

$\frac{c(x) \in C(x) [x \in A] \quad a = b}{c(a)=c(b)\in C(a)}$

This is just a straightforward application of equality to proof objects.

There’s more of these kinds of rules, but I’m going to stop here. My goal isn’t to get you to know every single judgement in the intuitionistic logic of type theory, but to give you a sense of what they mean.

That brings us to the end of the basic inference rules. The next things we’ll need to cover are ways of constructing new types or types from existing ones. The two main tools for that are enumeration types (basically, types consisting of a group of ordered values), and cartesian products of multiple types. With those, we’ll be able to find ways of constructing most of the types we’ll want to use in programming languages.

A Gentle Explanation of the Intel Speculative Execution CPU Bug

There’s a lot of talk today about the recent discovery of a significant bug in the Intel CPUs that so many of us use every day. It’s an interesting problem, and understanding it requires knowing a little bit about how CPUs work, so I thought I’d take a shot at writing an explainer.

Let me start with a huge caveat: this involves a lot of details about how CPUs work, and in order to explain it, I’m going to simplify things to an almost ridiculous degree in order to try to come up with an explanation that’s comprehensible to a lay person. I’m never deliberately lying about how things work, but at times, I’m simplifying enough that it will be infuriating to an expert. I’m doing my best to explain my understanding of this problem in a way that most people will be able to understand, but I’m bound to oversimplify in some places, and get details wrong in others. I apologize in advance.

It’s also early days for this problem. Intel is still trying to keep the exact details of the bug quiet, to make it harder for dishonest people to exploit it. So I’m working from the information I’ve been able to gather about the issue so far. I’ll do my best to correct this post as new information comes out, but I can only do that when I’m not at work!

That said: what we know so far is that the Intel bug involves non-kernel code being able to access cached kernel memory through the use of something called speculative execution.

To an average person, that means about as much as a problem in the flux thruster atom pulsar electrical ventury space-time implosion field generator coil.

The CPU, in simple terms, the brain of a computer. It’s the component that actually does computations. It reads a sequence of instructions from memory, and then follows those instructions to perform some computation on some values, which are also stored in memory. This is a massive simplification, but basically, you can think of the CPU as a pile of hardware than runs a fixed program:

def simplified_cpu_main_loop():
IP = 0
while true:
(op, in1, in2, out) = fetch(IP)
val1 = fetch(in1)
val2 = fetch(in2)
result, IP = perform(op, in1, in2)
store(result, out)

There’s a variable called the instruction pointer (abbreviated IP) built-in to the CPU that tells it where to fetch the next instruction from. Each time the clock ticks, the CPU fetches an instruction from the memory address stored in the instruction pointer, fetches the arguments to that instruction from cells in memory, performs the operation on those arguments, and then stores the result into another cell in the computer memory. Each individual operation produces both a result, and a new value for the instruction pointer. Most of the time, you just increment the instruction pointer to look at the next instruction, but for comparisons or branches, you can change it to something else.

What I described above is how older computers really worked. But as CPUs got faster, chipmaker ran into a huge problem: the CPU can perform its operations faster and faster every year. But retrieving a value from memory hasn’t gotten faster at the same rate as executing instructions. The exact numbers don’t matter, but to give you an idea, a modern CPU can execute an instruction in less than one nanosecond, but fetching a single value from memory takes more than 100 nanoseconds. In the scheme we described above, you need to fetch the instruction from memory (one fetch), and then fetch two parameters from memory (another two fetches), execute the instruction (1 nanosecond), and then store the result back into memory (one store). Assuming a store is no slower than a fetch, that means that for one nanosecond of computation time, the CPU needs to do 3 fetches and one store for each instruction. That means that the CPU is waiting, idle, for at least 400ns, during which it could have executed another 400 instructions, if it didn’t need to wait for memory.

That’s no good, obviously. There’s no point in making a fast CPU if all it’s going to do is sit around and wait for slow memory. But designers found ways to work around that, by creating ways to do a lot of computation without needing to pause to wait things to be retrieved from/stored to memory.

Expanding on the idea of putting memory into the CPU, they added ways of reducing the cost of working with memory by creating copies of the active memory regions on the CPU. These are called caches. When you try to retrieve something from memory, if it’s in the cache, then you can access it much faster. When you access something from a memory location that isn’t currently in the cache, the CPU will copy a chunk of memory including that location into the cache.

You might ask why, if you can make the cache fast, why not just make all of memory like the cache? The answer is that the time it takes in hardware to retrieve something from memory increases with amount of memory that you can potentially access. Pointing at a cache with 1K of memory is lightning fast. Pointing at a cache with 1 megabyte of memory is much slower that the 1K cache, but much faster that a 100MB cache; pointing at a cache with 100MB is even slower, and so on.

So what we actually do in practice is have multiple tiers of memory. We have the registers (a very small set – a dozen or so memory cells, which can be accessed instantly); a level-0 cache (on the order of 8k in Intel’s chips), which is pretty fast; a level-1 cache (100s of kilobytes), an L2 cache (megabytes), L3 (tens of megabytes), and now even L4 (100s of megabytes). If something isn’t in L0 cache, then we look for it in L1; if we can’t find it in L1, we look in L2, and so on, until if we can’t find it in any cache, we actually go out to the main memory.

There’s more we can do to make things faster. In the CPU, you can’t actually execute an entire instruction all at once – it’s got multiple steps. For a (vastly simplified) example, in the pseudocode above, you can think of each instruction as four phases: (1) decode the instruction (figuring out what operation it performs, and what its parameters are), (2) fetch the parameters, (3) perform the operations internal computation, and (4) write out the result. By taking advantage of that, you can set up your CPU to actually do a lot of work in parallel. If there are three phases to executing an instruction, then you can execute phase one of instruction one in one cycle; phase one of instruction two and phase two of instruction one in the next cycle; phase one of instruction three, phase two of instruction two, and phase three of instruction one in the third cycle. This process is called pipelining.

To really take advantage of pipelining, you need to keep the pipeline full. If your CPU has a four-stage pipeline, then ideally, you always know what the next four instructions you’re going to execute are. If you’ve got the machine code version of an if-then-else branch, when you start the comparison, you don’t know what’s going to come next until you finish it, because there are two possibilities. That means that when you get to phase 2 of your branch instruction, you can’t start phase one of the next instruction. instruction until the current one is finished – which means that you’ve lost the advantage of your pipeline.

That leads to another neat trick that people play in hardware, called branch prediction. You can make a guess about which way a branch is going to go. An easy way to understand this is to think of some numerical code:

def run_branch_prediction_demo():
for i in 1 to 1000:
for j in 1 to 1000:
q = a[i][j] * sqrt(b[i][j])

After each iteration of the inner loop, you check to see if j == 1000. If it isn’t, you branch back to the beginning of that loop. 999 times, you branch back to the beginning of the loop, and one time, you won’t. So you can predict that you take the backward branch, and you can start executing the early phases of the first instructions of the next iteration. That may, most of the time you’re running the loop, your pipeline is full, and you’re executing your computation quickly!

The catch is that you can’t execute anything that stores a result. You need to be able to say “Oops, everything that I started after that branch was wrong, so throw it away!”. Alongside with branch prediction, most CPUs also provide speculative execution, which is a way of continuing to execute instructions in the pipeline, but being able to discard the results if they’re the result of an incorrect branch prediction.

Ok, we’re close. We’ve got to talk about just another couple of basic ideas before we can get to just what the problem is with these Intel chips.

We’re going to jump up the stack a bit, and instead of talking directly about the CPU hardware, we’re going to talk about the operating system, and how it’s implemented on the CPU.

An operating system is just a program that runs on your computer. The operating system can load and run other programs (your end-user applications), and it manages all of the resources that those other programs can work with. When you use an application that allocates memory, it sent a request called a syscall to the operating system asking it to give it some memory. If your application wants to read data from a disk drive, it makes a syscall to open a file and read data. The operating system is responsible for really controlling all of those resources, and making sure that each program that’s running only accesses the things that it should be allowed to access. Program A can only use memory allocated by program A; if it tries to access memory allocated by program B, it should cause an error.

The operating system is, therefore, a special program. It’s allowed to touch any piece of memory, any resource owned by anything on the computer. How does that work?

There are two pieces. First, there’s something called memory protection. The hardware provides a mechanism that the CPU can use to say something like “This piece of memory is owned by program A”. When the CPU is running program A, the memory protection system will arrange the way that memory looks to the program so that it can access that piece of memory; anything else just doesn’t exist to A. That’s called memory mapping: the system memory of the computer is mapped for A so that it can see certain pieces of memory, and not see others. In addition to memory mapping, the memory protection system can mark certain pieces of memory as only being accessible by privileged processes.

Privileged processes get us to the next point. In the CPU, there’s something called an execution mode: programs can run in a privileged mode (sometimes called kernel space execution), or it can run in a non-privileged mode (sometimes called user-space execution). Only code that’s running in kernel-space can do things like send commands to the memory manager, or change memory protection settings.

When your program makes a syscall, what really happens is that your program puts the syscall parameters into a special place, and then sends a signal called an interrupt. The interrupt switches the CPU into system space, and gives control to the operating system, which reads the interrupt parameters, and does whatever it needs to. Then it puts the result where the user space program expects it, switches back to user-space, and then allows the user space program to continue.

That process of switching from the user space program to the kernel space, doing something, and then switching back is called a context switch. Context switches are very expensive. Implemented naively, you need to redo the memory mapping every time you switch. So the interrupt consists of “stop what you’re doing, switch to privileged mode, switch to the kernel memory map, run the syscall, switch to the user program memory map, switch to user mode”.

Ok. So. We’re finally at the point where we can actually talk about the Intel bug.

Intel chips contain a trick to make syscalls less expensive. Instead of having to switch memory maps on a syscall, they allow the kernel memory to be mapped into the memory map of every process running in the system. But since kernel memory can contain all sorts of secret stuff (passwords, data belonging to other processes, among other things), you can’t let user space programs look at it – so the kernel memory is mapped, but it’s marked as privileged. With things set up that way, a syscall can drop the two “switch memory map” steps in the syscall scenario. Now all a syscall needs to do is switch to kernel mode, run the syscall, and switch back to user mode. It’s dramatically faster!

Here’s the problem, as best I understand from the information that’s currently available:

Code that’s running under speculative execution doesn’t do the check whether or not memory accesses from cache are accessing privileged memory. It starts running the instructions without the privilege check, and when it’s time to commit to whether or not the speculative execution should be continued, the check will occur. But during that window, you’ve got the opportunity to run a batch of instructions against the cache without privilege checks. So you can write code with the right sequence of branch instructions to get branch prediction to work the way you want it to; and then you can use that to read memory that you shouldn’t be able to read.

With that as a starting point, you can build up interesting exploits that can ultimately allow you to do almost anything you want. It’s not a trivial exploit, but with a bit of work, you can use a user space program to make a sequence of syscalls to get information you want into memory, and then write that information wherever you want to – and that means that you can acquire root-level access, and do anything you want.

The only fix for this is to stop doing that trick where you map the kernel memory into every user space memory map, because there’s no way to enforce the privileged memory property in speculative execution. In other words, drop the whole syscall performance optimization. That’ll avoid the security issue, but it’s a pretty expensive fix: requiring a full context switch for every syscall will slow down the execution of user space programs by something between 5 and 30 percent.

Zombie Math in the Vortex

Paul Krugman has taken to calling certain kinds of economic ideas zombie economics, because no matter how many times they’re shown to be false, they just keep coming back from the dead. I certainly don’t have stature that compares in any way to Krugmant, but I’m still going to use his terminology for some bad math. There are some crackpot ideas that you just can’t kill.

For example, vortex math. I wrote about vortex math for the first time in 2012, again in early 2013, and again in late 2013. But like a zombie in a bad movie, it’s fans won’t let it stay dead. There must have been a discussion on some vortex-math fan forum recently, because over the last month, I’ve been getting comments on the old posts, and emails taking me to task for supposedly being unfair, closed-minded, ignorant, and generally a very nasty person.

Before I look at any of their criticisms, let’s start with a quick refresher. What is vortex math?

We’re going to create a pattern of single-digit numbers using multiples of 2. Take the number 1. Multiply it by 2, and you get 2. Multiple it by 2, and you get 4. Again, you get 8. Again, and you get 16. 16 is two digits, but we only want one-digit numbers, so we add them together, getting 7. Double, you get 14, so add the digits, and you get 5. Double, you get 10, add the digits, and you get 1. So you’ve got a repeating sequence: 1, 2, 4, 8, 7, 5, …

Take the numbers 1 through 9, and put them at equal distances around the perimeter of a circle. Draw an arrow from a number to its single-digit double. You end up with something that looks kinda-sorta like the infinity symbol. You can also fit those numbers onto the surface of a torus.

That’s really all there is to vortex math. This guy named Marco Rodin discovered that there’s a repeating pattern, and if you draw it on a circle, it looks kinda-like the infinity symbol, and that there must be something incredibly profound and important about it. Launching from there, he came up with numerous claims about what that means. According to vortex math, there’s something deeply significant about that pattern:

1. If you make metallic windings on a toroidal surface according to that pattern and use it as a generator, it will generate free energy.
2. Take that same coil, and run a current through it, and you have a perfect, reactionless space drive (called “the flux thruster atom pulsar electrical ventury space time implosion field generator coil”).
3. If you use those numbers as a pattern in a medical device, it will cure cancer, as well as every other disease.
4. If you use that numerical pattern, you can devise better compression algorithms that can compress any string of bits.
5. and so on…

Essentially, according to vortex math, that repeated pattern of numbers defines a “vortex”, which is the deepest structure in the universe, and it’s the key to understanding all of math, all of physics, all of metaphysics, all of medicine. It’s the fundamental pattern of everything, and by understanding it, you can do absolutely anything.

As a math geek, the problem with stuff like vortex math is that it’s difficult to refute mathematically, because even though Rodin calls it math, there’s really no math to it. There’s a pattern, and therefore magic! Beyond the observation that there’s a pattern, there’s nothing but claims of things that must be true because there’s a pattern, without any actual mathematical argument.

Let me show you an example, from one of Rodin’s followers, named Randy Powell.

I call my discovery the ABHA Torus. It is now the full completion of how to engineer Marko Rodin’s Vortex Based Mathematics. The ABHA Torus as I have discovered it is the true and perfect Torus and it has the ability to reveal in 3-D space any and all mathematical/geometric relationships possible allowing it to essentially accomplish any desired functional application in the world of technology. This is because the ABHA Torus provides us a mathematical framework where the true secrets of numbers (qualitative relationships based on angle and ratio) are revealed in fullness.

This is why I believe that the ABHA Torus as I have calculated is the most powerful mathematical tool in existence because it presents proof that numbers are not just flat imaginary things. To the contrary, numbers are stationary vector interstices that are real and exhibiting at all times spatial, temporal, and volumetric qualities. Being stationary means that they are fixed constants. In the ABHA Torus the numbers never move but the functions move through the numbers modeling vibration and the underlying fractal circuitry that natures uses to harness living energy.

The ABHA Torus as revealed by the Rodin/Powell solution displays a perfectly symmetrical spin array of numbers (revealing even prime number symmetry), a feat that has baffled countless scientists and mathematicians throughout the ages. It even uncovers the secret of bilateral symmetry as actually being the result of a diagonal motion along the surface and through the internal volume of the torus in an expanding and contracting polarized logarithmic spiral diamond grain reticulation pattern produced by the interplay of a previously unobserved Positive Polarity Energetic Emanation (so-called ‘dark’ or ‘zero-point’ energy) and a resulting Negative Polarity Back Draft Counter Space (gravity).

If experimentally proven correct such a model would for example replace the standard approach to toroidal coils used in energy production today by precisely defining all the proportional and angular relationships existent in a moving system and revealing not only the true pathway that all accelerated motion seeks (be it an electron around the nucleus of an atom or water flowing down a drain) but in addition revealing this heretofore unobserved, undefined point energetic source underlying all space-time, motion, and vibration.

Lots of impressive sounding words, strung together in profound sounding ways, but what does it mean? Sure, gravity is a “back draft” of an unobserved “positive polarity energetic emanatation”, and therefore we’ve unified dark energy and gravity, and unified all of the forces of our universe. That sounds terrific, except that it doesn’t mean anything! How can you test that? What evidence would be consistent with it? What evidence would be inconsistent with it? No one can answer those questions, because none of it means anything.

As I’ve said lots of times before: there’s a reason for the formal framework of mathematics. There’s a reason for the painful process of mathematical proof. There’s a reason why mathematicians and scientists have devised an elaborate language and notation for expressing mathematical ideas. And that reason is because it’s easy to string together words in profound sounding ways. It’s easy to string together reasoning in ways that look like they might be compelling if you took the time to understand them. But to do actual mathematics or actual science, you need to do more that string together something that sounds good. You need to put together something that is precise. The point of mathematical notation and mathematical reasoning is to take complex ideas and turn them into precisely defined, unambiguous structures that have the same meaning to everyone who looks at them.

“positive polarity energetic emanation” is a bunch of gobbledegook wordage that doesn’t mean anything to anyone. I can’t refute the claim that gravity is a back-draft negative polarity energetic reaction to dark energy. I can’t support that claim, either. I can’t do much of anything with it, because Randy Powell hasn’t said anything meaningful. It’s vague and undefined in ways that make it impossible to reason about in any way.

And that’s the way that things go throughout all of vortex math. There’s this cute pattern, and it must mean something! Therefore… endless streams of words, without any actual mathematical, physical, or scientific argument.

There’s so much wrong with vortex math, but it all comes down to the fact that it takes some arbitrary artifacts of human culture, and assigns them deep, profound meaning for no reason.

There’s this pattern in the doubling of numbers and reducing them to one digit. Why multiple by two? Because we like it, and it produces a pretty pattern. Why not use 3? Well, because in base-10, it won’t produce a good pattern: [1, 3, 9, 9, 9, 9, ….] But we can pick another number like 7: [1, 7, 5, 8, 2, 5, 8, 2, 5, ….], and get a perfectly good series: why is that series less compelling than [1, 4, 8, 7, 2, 5]?

There’s nothing magical about base-10. We can do the same thing in base-8: [1, 2, 4, 1, 2, 4…] How about base-12, which was used for a lot of stuff in Egypt? [1, 2, 4, 8, 5, 10, 9, 7, 3, 6, 1] – that gives us a longer pattern! What makes base-10 special? Why does the base-10 pattern mean something that other bases, or other numerical representations, don’t? The vortex math folks can’t answer that. (Note: I made an arithmetic error in the initial version of the base-12 sequence above. It was pointed out in comments by David Wallace. Thanks!)

If we plot the numbers on a circle, we get something that looks kind-of like an infinity symbol! What does that mean? Why should the infinity symbal (which was invented in the 17th century, and chosen because it looked sort of like a number, and sort-of like the last letter of the greek alphabet) have any intrinsic meaning to the universe?

It’s giving profound meaning to arbitrary things, for unsupported reasons.

So what’s in the recent flood of criticism from the vortex math guys?

Well, there’s a lot of “You’re mean, so you’re wrong.” And there’s a lot of “Why don’t you prove that they’re wrong instead of making fun of them?”. And last but not least, there’s a lot of “Yeah, well, the fibonacci series is just a pattern of numbers too, but it’s really important”.

On the first: Yeah, fine, I’m mean. But I get pretty pissed at seeing people get screwed over by charlatans. The vortex math guys use this stuff to take money from “investors” based on their claims about producing limitless free energy, UFO space drives, and cancer cures. This isn’t abstract: this kind of nonsense hurts people. They people who are pushing these scams deserve to be mocked, without mercy. They don’t deserve kindness or respect, and they’re not going to get it from me.

I’d love to be proved wrong on this. One of my daughter’s friends is currently dying of cancer. I’d give up nearly anything to be able to stop her, and other children like her, from dying an awful death. If the vortex math folks could do anything for this poor kid, I would gladly grovel and humiliate myself at their feet. I would dedicate the rest of my life to nothing but helping them in their work.

But the fact is, when they talk about the miraculous things vortex math can do? At best, they’re delusional; more likely, they’re just lying. There is no cure for cancer in [1, 2, 4, 8, 7, 5, 1].

As for the Fibonacci series: well. It’s an interesting pattern. It does appear to show up in some interesting places in nature. But there are two really important differences.

1. The Fibonacci series shows up in every numeric notation, in every number base, no matter how you do numbers.
2. It does show up in nature. This is key: there’s more to it than just words and vague assertions. You can really find fragments of the Fibonacci series in nature. By doing a careful mathematical analysis, you can find the Fibonacci series in numerous places in mathematics, such as the solutions to a range of interesting dynamic optimization problems. When you find a way of observing the vortex math pattern in nature, or a way of producing actual numeric solutions for real problems, in a way that anyone can reproduce, I’ll happily give it another look.
3. The Fibonacci series does appear in nature – but it’s also been used by numerous crackpots to make ridiculous assertions about how the world must work!


text:
# NAG Library Function Document

## 1Purpose

nag_running_median_smoother (g10cac) computes a smoothed data sequence using running median smoothers.

## 2Specification

 #include #include
 void nag_running_median_smoother (Nag_Smooth_Type smoother, Integer n, const double y[], double smooth[], double rough[], NagError *fail)

## 3Description

Given a sequence of $n$ observations recorded at equally spaced intervals, nag_running_median_smoother (g10cac) fits a smooth curve through the data using one of two smoothers. They are based on the use of running medians and averages to summarise the overlapping segments. The fit is called the smooth, the residuals the rough and they obey the following:
Data = Smooth + Rough
The two smoothers are :
 1 4253H, twice consisting of a running median of 4, then 2, then 5, then 3 followed by Hanning. Hanning is a running weighted average, the weights being 1/4, 1/2 and 1/4. The result of this smoothing is then reroughed by computing residuals, applying the same smoother to them and adding the result to the smooth of the first pass. 2 3RSSH, twice consisting of a running median of 3, two splitting operations named S to improve the smooth sequence, each of which is followed by a running median of 3, and finally Hanning. The end points are dealt with using the method described by Velleman and Hoaglin (1981). The full smoother 3RSSH, twice is produced by reroughing as described above.
The compound smoother 4253H, twice is recommended. The smoother 3RSSH, twice is popular when calculating by hand as it requires simpler computations and is included for comparison purposes.

## 4References

Tukey J W (1977) Exploratory Data Analysis Addison–Wesley
Velleman P F and Hoaglin D C (1981) Applications, Basics, and Computing of Exploratory Data Analysis Duxbury Press, Boston, MA

## 5Arguments

1:    $\mathbf{smoother}$Nag_Smooth_TypeInput
On entry: smoother must specify the method to be used.
${\mathbf{smoother}}=\mathrm{Nag_4253H}$
4253H, twice is used.
${\mathbf{smoother}}=\mathrm{Nag_3RSSH}$
Constraint: ${\mathbf{smoother}}=\mathrm{Nag_4253H}$ or $\mathrm{Nag_3RSSH}$.
2:    $\mathbf{n}$IntegerInput
On entry: the number, $n$, of the observations.
Constraint: ${\mathbf{n}}>6$.
If ${\mathbf{n}}\le 6$ then the sequence is not long enough to carry out smoothing.
3:    $\mathbf{y}\left[{\mathbf{n}}\right]$const doubleInput
On entry: the sample observations.
4:    $\mathbf{smooth}\left[{\mathbf{n}}\right]$doubleOutput
On exit: contains the smooth.
5:    $\mathbf{rough}\left[{\mathbf{n}}\right]$doubleOutput
On exit: contains the rough.
6:    $\mathbf{fail}$NagError *Input/Output
The NAG error argument (see Section 3.7 in How to Use the NAG Library and its Documentation).

## 6Error Indicators and Warnings

On entry, argument smoother had an illegal value.
NE_INT_ARG_LE
On entry, ${\mathbf{n}}=〈\mathit{\text{value}}〉$.
Constraint: ${\mathbf{n}}>6$.

Not applicable.

## 8Parallelism and Performance

nag_running_median_smoother (g10cac) is not threaded in any implementation.

### 9.1Internal Changes

Internal changes have been made to this function as follows:
• At Mark 25: nag_running_median_smoother (g10cac) is a smoothing function with two possible smoothing methods. The function was previously using the incorrect method (i.e., if you asked for method A you would get method B, and vice versa).
For details of all known issues which have been reported for the NAG Library please refer to the Known Issues list.

## 10Example

The example program reads in a sequence of 49 data taken from Tukey (1977), above. Results are obtained using the two smoothing methods described.

### 10.1Program Text

Program Text (g10cace.c)

### 10.2Program Data

Program Data (g10cace.d)

### 10.3Program Results

Program Results (g10cace.r)

© The Numerical Algorithms Group Ltd, Oxford, UK. 2017

format: plain


text:
## Stream: new members

### Topic: Double Negation and Proof by Contradiction

#### Dan Knight (Apr 26 2020 at 03:34):

Hi All - I've done a little bit of formal mathematics in uni and have started with the publicly available "Logic and Proof" course using Lean. I'm looking for some help with proofs that prove the negation of a proposition (-A) by contradiction.

My problem arises as the type checker expects the negation of the already negated proposition (--A) to lead to false, rather than just the proposition (A) itself. If I use the have keyword to prove A from --A, my text then type checks to ... -> A -> -A and fails given this extra step (pseudo example at the bottom).

Is there a way around this double negation problem? I've tried rewriting the proofs but can't seem to do quite a few of the exercises without something of this form. Any all help would be greatly appreciated it. Moreover, apologize for the noob question, this has been quite the humbling evening/afternoon

-Example-
(assume hNNA : \not \not A,
have hA : A, from ...
show false, h? hA)
-Error-
type mismatch at application
A→ false
but is expected to have type
¬¬A → false

#### Shing Tak Lam (Apr 26 2020 at 03:38):

There is theorem not_not [decidable a] : ¬¬a ↔ a, which might be useful. Although it may be helpful if you post example code?

#### Donald Sebastian Leung (Apr 26 2020 at 04:37):

To add to this: use triple backticks to get formatted code, e.g.

lean
example : 1 + 1 = 2 := rfl

#### Shing Tak Lam (Apr 26 2020 at 04:40):

Donald Sebastian Leung said:

To add to this: use triple backticks to get formatted code, e.g.

lean
example : 1 + 1 = 2 := rfl

(You don't need the lean part anymore since this update, the default here is that three backticks is Lean, and you need to explicitly state when it is monospace text with text. Obviously using lean won't break anything)

#### Dan Knight (Apr 26 2020 at 20:18):

Shing Tak Lam said:

There is theorem not_not [decidable a] : ¬¬a ↔ a, which might be useful. Although it may be helpful if you post example code?

Thanks Shing I appreciate the thought! That theorem helped and I was able to debug it! Thank you!

Last updated: May 13 2021 at 05:21 UTC


text:
Friday, July 10, 2015

Part VII : High Precision Photometry of Transiting Exoplanets as I currently know it

In Part IV, I posed the following questions but forgot to give my brief answer for it:
"So, how does MINERVA (a ground-based observatory) differ from the Kepler Mission?  Furthermore, why am I looking for 'High Precision' measurements from this MINERVA observatory and not the space-based Kepler data?  "

Both telescopes have a purpose to detect exoplanets.  When discerning that Kepler is a space-based telescope and MINERVA is ground-based, your first impression might be that Kepler is better than MINERVA.  However here are a few facts about MINERVA that indicate why it is simply different than Kepler as opposed to being inferior:
• A multi-telescope array allows for simultaneous exposure of primary bright star and its comparison stars (for which satisfactory comparison stars may sometimes not be in the same field of view for 1 telescope alone).
• Despite how related this concept is to my project specifically, this concept is also very related to differential photometry research in general.  Differential photometry is an immensely beneficial and widely used form of research. I think it's cool that an observatory was made to ameliorate this form of research practice.

• A primary purpose of MINERVA is to ALWAYS achieve a measured Doppler Shift precision of 0.8 m/s or less.
• Radial Velocity Curves will have small error bars!
• This is great for confirming exoplanet candidates as true exoplanet detections that have been observed by Kepler.
• This is also great for confirming false-positive exoplanet detections made by Kepler.  A false-positive detection is when the measurements seem to infer that an exoplanet was observed, however after further observations and/or analysis that object was verified to be something else--such as an eclipsing binary star.

• MINERVA was also built for being capable of detecting super-Earths (exoplanets with 2-5R$$_{\oplus}$$)  within their respective habitable zones.  After being detected with radial velocity measurements, these super-Earths can be characterized further with multi-band photometry.  This feat requires a broadband photometric precision < 1 mmag in the optical wavelengths.
• Aside: remember R$$_{\oplus}$$ represents 1 Earth's radius as if it is a unit of measurement, like the meter.  It is a convenient way to compare the size of other objects to an object (the Earth) that we are familiar with. Furthermore, I will elaborate on multi-band photometry and 1 mmag precision at a later time.

• Now that MINERVA can do such a great job at confirming exoplanet candidates initially observed by Kepler, humanity can move quicker in finding planets that may already harbor Life.  Surely, planets that have satisfactory conditions to sustain life will be the first among a list of destinations that astronauts will travel to when long distance space travel becomes more common and feasible.

• Another primary purpose of MINERVA is to detect and confirm exoplanets with small radii.  This is difficult to do because of how small the "dip" of a light curve is for small transiting exoplanets.  In Part IV,  I stated "there are more planets with a radius < 4R$$_{\oplus}$$ than there are larger ones in our Milky Way Galaxy.  This means that a project dedicated to finding exoplanets should certainly be equipped to find planets with a relatively small radius (~Earth size) and low mass."
• This is one reason why the MINERVA project is so focused on achieving high precision measurements.

• It's a ground based telescope.  It costs MUCH less to construct.  It costs MUCH less operate.  Therefore... More astronomers have access to use it for their specific research purposes.  This means students of all ages have a better chance at earning time on this telescope for their research needs as well!
How great is it that I, an undergraduate, can use highly sophisticated technology partially owned by Harvard University to conduct research that will actually benefit the astronomy community at large!  It is because of the access that telescopes like MINERVA provide to the younger astronomy community that makes a young person like me be able to make discoveries that are actually relevant and significant to this well-respected field of highly-educated philosophers of the Universe. Yay! for Opportunity.  And speaking of "access", the MINERVA (Planewave CDK 0.7m) telescopes were made to be wheelchair accessible.  Yay! for social justice and awareness of abilism.  Yay! for the astronomy community respecting the ideas and research of its youngest members.

Sorry for the spontaneous outbursts of celebrations.  I guess I was in a grateful mood.  I think now is as good of a time as any to tweet what the Adler Planetarium deems #science4everyone.


text:
# Evaluating $\lim_\limits{x\to 3}\left(\frac{\left(x!-2x\right)}{x-3}\right)$

$$\lim_\limits{x\to 3}\left(\frac{\left(x!-2x\right)}{x-3}\right)$$

I tried substituting $$x(x-1)$$ in place for $$x!$$ as the limit approaches $$3$$, giving the limit $$3$$ by factorization.
But while plotting graph on Desmos calculator, it showed a weird gamma function graph, giving the answer around 5.5 like this
But when I plotted graph substituting $$x(x-1)$$ in place for $$x!$$, the graph was a straight line and gave limit $$3$$. like this

• How would you define $x!$ without the gamma function? Keeping in mind that the function needs to be defined for all $x$ in an interval like $(2.99,3.01)$? Anyway, looks like the derivative of gamma should come out. Either by l'Hospital (if allowed) or possibly by using the functional equation of gamma. – Jyrki Lahtonen May 5 '20 at 4:19
• How did you get your original answer by factorisation? You still get an indeterminate form. Better check your working. You need an extension of the factorial valid for non-integers for this, and the most commonly used one is the gamma function. – Deepak May 5 '20 at 4:47
• I tried substituting x(x−1) in place for x!, giving x^2-x – Aatmaj May 5 '20 at 5:00

I believe the first answer is correct. Mathematica gives the answer as $$9 - 6\gamma$$, where $$\gamma$$ is the Euler-Mascheroni constant. The reason for this has to do with the fact that the (generalized) factorial can be expressed in terms the Gamma function \begin{align*} \Gamma(z) = \int_0^\infty x^{z-1}e^{-x}dx, \end{align*} when $$\Re z > 0$$. This function has the property that $$\Gamma(n) = (n-1)!$$ for all positive integers $$n$$ and so it is the natural extension of the factorial. Using this, we can replace $$x! = \Gamma(x+1) = \int_0^\infty y^{x}e^{-y}dy$$. The Wikipedia page for the gamma function presents a nice form for its derivative when $$x$$ is an integer:

\begin{align*} \Gamma'(x+1) =x!\left(-\gamma+\sum_{k=1}^x\frac{1}{k}\right) \end{align*}

Now applying L'Hopital's rule and use the above formula for the derivative we get: \begin{align*} \lim_{x \rightarrow 3} \frac{x!-2x}{x-3} &= \lim_{x \rightarrow 3} \frac{\Gamma(x+1)-2x}{x-3} = \lim_{x \rightarrow 3} \Gamma'(x+1)-2 = \Gamma'(4) - 2\\ &= 3!\left(-\gamma + 1 + \frac{1}{2} + \frac{1}{3}\right) - 2 = 9-6\gamma \approx 5.5. \end{align*}

Not sure why you're using $$x(x-1)$$ in place of $$x!$$. It is much easier to consider the gamma function $$\Gamma$$ and, its "logarithmic derivative", the digamma function $$\psi$$. In particular, the property

$$\psi(x) = \frac{\Gamma'(x)}{\Gamma(x)},$$

holds. This gives us the quite handy identity that

$$\Gamma'(x) = \Gamma(x) \psi(x).$$

Let the limit be denoted as $$L$$. Then,

$$L = \lim_{x \to 3} \frac{\Gamma(x+1) - 2x}{x - 3}.$$

This has a $$0/0$$ indeterminate form, so you can use L'Hopital's rule to obtain

$$L = \lim_{x \to 3} (\Gamma'(x+1) - 2),$$

with which we have

$$L = \lim_{x \to 3} (\psi(x+1) \Gamma(x+1) - 2) = \psi(4)\Gamma(4) - 2.$$

Here, $$\Gamma(4) = 3! = 6$$. The digamma function is given by

$$\psi(x) = -\gamma + \sum_{n=1}^{x-1} \frac1n$$

for integers $$x$$. The constant $$\gamma$$ is the Euler-Mascheroni constant so $$\psi(4) = 1 + 1/2 + 1/3 - \gamma$$. Thus

$$L = 9 - \gamma.$$

$$\lim_\limits{x\to 3}\left(\frac{\left(x!-2x\right)}{x-3}\right)=\lim_\limits{y\to 0}\left(\frac{\Gamma (y+4)-2 (y+3)}{y}\right)$$ $$\Gamma (y+4)=6+(11-6 \gamma ) y+\frac{1}{2} \left(12-22 \gamma +6 \gamma ^2+\pi ^2\right) y^2+O\left(y^3\right)$$ $$\frac{\Gamma (y+4)-2 (y+3)}{y}=(9-6 \gamma )+\frac{1}{2} \left(12-22 \gamma +6 \gamma ^2+\pi ^2\right) y+O\left(y^2\right)$$ which shows the limit and how it is approached.
Using this for $$x=\pi$$ would give $$6.32750$$ while the exact value would be $$6.39085$$


text:
grelgroup - Help

grelgroup

represent a group by generators and relations

 Calling Sequence grelgroup(gens, rels)

Parameters

 gens - set of names taken to be the generators of the group rels - set of relations among the generators which define the group

Description

 • The function grelgroup is used as a procedure and an unevaluated procedure call. As a procedure, grelgroup checks its arguments and then either exits with an error or returns the unevaluated grelgroup call.
 • The first argument is a set of Maple names which stand for the generators of the group. The second argument is a set of words'' in the generators. A word'' is a list of generators and/or inverses of generators representing a product.  The inverse of a generator $g$ is represented by $\frac{1}{g}$. An empty list represents the identity element.  The words w1, w2, ..., wn in rels are such that the relations $\mathrm{w1}=\mathrm{w2}=\mathrm{...}=\mathrm{wn}=1$ define the group.

Examples

 > $\mathrm{grelgroup}\left(\left\{a,b\right\},\left\{\left[a,a,a\right],\left[b,b\right],\left[a,b,\frac{1}{a},\frac{1}{b}\right]\right\}\right)$
 ${\mathrm{grelgroup}}{}\left(\left\{{a}{,}{b}\right\}{,}\left\{\left[{b}{,}{b}\right]{,}\left[{a}{,}{a}{,}{a}\right]{,}\left[{a}{,}{b}{,}\frac{{1}}{{a}}{,}\frac{{1}}{{b}}\right]\right\}\right)$ (1)

the following will give an error:

 > $\mathrm{grelgroup}\left(\left\{a,b\right\},\left\{\left[a,\frac{1}{c},a\right],\left[b,a\right]\right\}\right)$


text:
# What is the measure in degrees of the angle A=(7pi)/6?

Remembering that $\pi$ is "like" 180°, than:
A=7/6*180°=210°.


text:
# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

Example 5.2.6.11. Let $n \geq 0$ and let $\overrightarrow {X}: [n] \rightarrow \operatorname{Set_{\Delta }}$ be a diagram of simplicial sets which we denote by

$X(0) \rightarrow X(1) \rightarrow X(2) \rightarrow \cdots \rightarrow X(n).$

For each integer $0 \leq i \leq n$, let $\Delta ^ n_{\geq i}$ denote the nerve of the linearly ordered set $\{ i < i+1 < \cdots < n \}$, which we regard as a simplicial subset of $\Delta ^ n$. Applying Remark 5.2.6.9 repeatedly, we can identify the mapping simplex $M( \overrightarrow {X} )$ with the iterated pushout

$(\Delta ^ n \times X(0)) \coprod _{ ( \Delta ^{n}_{\geq 1} \times X(0)) } (\Delta ^{n}_{\geq 1} \times X(1) ) \coprod _{ ( \Delta ^{n}_{\geq 2} \times X(1))} \cdots \coprod _{ (\{ n\} \times X(n-1))} (\{ n\} \times X(n)).$


text:
Subscribe
(PrePrints)
ISSN: 1545-5971
Regular Papers
Hannes Holm , The Royal Institute of Technology, Stockholm
Noman Mohammed , McGill University, Montreal
Dima Alhadidi , Concordia University, Montreal
Benjamin C. M. Fung , Concordia University, Montreal
Mourad Debbabi , Concordia University, Montreal
Satya Gautam Vadlamudi , Indian Institute of Technology Kharagpur, Kharagpur
Partha Pratim Chakrabarti , Indian Institute of Technology Kharagpur, Kharagpur
Lingyu Wang , Concordia University, Montreal
Sushil Jajodia , George Mason University, Fairfax
Anoop Singhal , National Institute of Standards and Technology, Gaithersburg
Pengsu Cheng , Concordia University, Montreal
Steven Noel , George Mason University, Fairfax
Papers
Libor Polcak , Brno University of Technology, Brno
Jakub Jirasek , Brno University of Technology, Brno
Petr Matousek , Brno University of Technology, Brno
Hussain M.J. Almohri , Virginia Tech, Blacksburg
Danfeng Daphne Yao , Virginia Tech, Blacksburg
Dennis Kafura , Virginia Tech, Blacksburg
Regular Papers
Leandro Fiorin , Faculty of Lugano, Lugano
Mariagiovanna Sami , Politecnico di Milano, Milano
Nicola Basilico , University of California, Merced
Nicola Gatti , Politecnico di Milano, Milan
Mattia Monga , Università degli Studi di Milano, Milan
Sabrina Sicari , Università degli Studi dell'Insubria, Varese
Papers
Qinghua Li , The Pennsylvania State University, University Park
Guohong Cao , The Pennsylvania State University, University Park
Thomas F. La Porta , The Pennsylvania State University, University Park
Kizito Salako , City University London, London
Lorenzo Strigini , City University London, London
Yang Qin , FaceBook, Menlo Park
Dijiang Huang , Arizona State University, Tempe
Bing Li , Arizona State University, Tempe
Gorrell P. Cheek , University of North Carolina at Charlotte, Charlotte
Mohamed Shehab , University of North Carolina at Charlotte, Charlotte
Xun Yi , Victoria University, Melbourne
Elisa Bertino , Purdue University, West Lafayette
Jaideep Vaidya , Rutgers University, Newark
Chaoping Xing , Nanyang Technological University, Singapore
José Fonseca , Institute Polytechnic of Guarda, Guarda and University of Coimbra, Coimbra
Nuno Seixas , University of Coimbra, Coimbra
Marco Vieira , University of Coimbra, Coimbra
Henrique Madeira , University of Coimbra, Coimbra
jing zhao , Harbin Engineering University, Harbin
Kishor S. Trivedi , Duke University, Durham
Michael Grottke , Friedrich-Alexander-Universität Erlangen-Nürnberg, Nürnberg
Javier Alonso , Duke University, Durham
Yanbin Wang , Harbin Institude of Technology, Harbin
Silvio Cesare , Deakin University, Burwood
Yang Xiang , Deakin University, Burwood
Wanlei Zhou , Deakin University, Burwood
Puneet Gupta , Google, Inc., Mountain View
Scott D. Stoller , Stony Brook University, Stony Brook
Zhongyuan Xu , Stony Brook University, Stony Brook
Jaideep Vaidya , Rutgers University, Newark
Basit Shafiq , Lahore University of Management Sciences, Lahore
Wei Fan , Huawei Noah's Ark Lab, Hong Kong
Danish Mehmood , Lahore University of Management Sciences, Lahore
David Lorenzi , Rutgers University, Newark
Kwantae Cho , Electronics and Telecommunications Research Institute, Daejeon
Byung-Gil Lee , Electronics and Telecommunications Research Institute, Daejeon
Dong Hoon Lee , Korea University, Seoul
Salmin Sultana , Purdue University, West Lafayette
Gabriel Ghinita , University of Massachusetts, Boston
Elisa Bertino , Purdue University, West Lafayette
Mohamed Shehab , University of North Carolina at Charlotte, Charlotte
José Fonseca , UDI of the Institute Polytechnic of Guarda, Guarda and the CISUC
Marco Vieira , University of Coimbra, Coimbra
Henrique Madeira , University of Coimbra, Coimbra
Marc Liberatore , University of Massachusetts Amherst, Amherst
Brian Neil Levine , University of Massachusetts Amherst, Amherst
Clay Shields , Georgetown University, Washington
Brian Lynn , University of Massachusetts Amherst, Amherst
Pietro Colombo , Università degli Studi dell'Insubria, Varese
Elena Ferrari , Università degli Studi dell'Insubria, Varese
Shu Yin , Hunan University, Changsha
Xiaojun Ruan , West Chester University of Pennsylvania, West Chester
Adam Manzanares , California State University - Chico, Chico
Xiao Qin , Auburn University, Auburn
Kenli Li , Hunan University, Changsha
Ruofan Xia , Duke university, Durham
Xiaoyan Yin , Duke University, Durham
Javier Alonso , Duke University, Durham
Fumio Machida , NEC Corporation, Kawasaki
Kishor S. Trivedi , Duke University, Durham
Sheng Wen , Deakin University, Melbourne
Wei Zhou , Deakin University, Melbourne
Jun Zhang , Deakin University, Melbourne
Yang Xiang , Deakin University, Melbourne
Wanlei Zhou , Deakin University, Melbourne
Weijia Jia , City University of Hong Kong, Hong Kong
Cliff C. Zou , University of Central Florida, Orlando
Adam Skillen , Carleton University, Ottawa and Concordia University, Montreal
Mohammad Mannan , Concordia University, Montreal
Kyuseung Han , Seoul National University, Seoul
Ganghee Lee , Samsung Electronics Co., Gyeonggi
Kiyoung Choi , Seoul National University, Seoul
Fengwei Zhang , George Mason University, Fairfax
Jiang Wang , Riverbed Technology, Sunnyvale
Kun Sun , George Mason University, Fairfax
Angelos Stavrou , George Mason University, Fairfax
Yogachandran Rahulamathavan , City University London, London
Raphael C.-W. Phan , Multimedia University, Cyberjaya
Suresh Veluru , City University London, London
Kanapathippillai Cumanan , Newcastle University, Newcastle upon tyne
Muttukrishnan Rajarajan , City University London, London
Reza Shokri , ETH Zurich, Zurich
George Theodorakopoulos , Cardiff University, Cardiff
Ehsan Kazemi , EPFL, Lausanne
Jean-Pierre Hubaux , EPFL, Lausanne
Wenhong Tian , University of Electronic Science and Technology of China, Chengdu
Yu Chen , University of Electronic Science and Technology of China, Chengdu
Xinyang Wang , University of Electronic Science and Technology of China, Chengdu
Yi Xu , University of North Carolina at Chapel Hill, Chapel Hill
Gerardo Reynaga , Carleton University, Ottawa
Sonia Chiasson , Carleton University, Ottawa
Jan-Michael Frahm , University of North Carolina at Chapel Hill, Chapel Hill
Fabian Monrose , University of North Carolina at Chapel Hill, Chapel Hill
Paul Van Oorschot , Carleton University, Ottawa
Christopher S. Gates , Purdue University, West Lafayette
Jing Chen , Purdue University, West Lafayette
Ninghui Li , Purdue University, West Lafayette
Robert W. Proctor , Purdue University, West Lafayette
Yury Zhauniarovich , Yury Zhauniarovich is with the University of Trento, Trento, 38123, Italy (email: yury.zhauniarovich@unitn.it).
Jin Tang , J. Tang is with AT&T Labs.(email:jin.tang@att.com)
Srikar Tati , Srikar Tati is with the Pennsylvania State University, (Email: tati@cse.psu.edu).
Jonghyuk Song , Jonghyuk Song is with the Department of Computer Science and Engineering, Pohang University of Science and Technology (POSTECH), Pohang, Republic of Korea.(email:freestar@postech.ac.kr)
Antonio Martinez-Alvarez , Antonio Martínez-Alvarez is with the Department of Computer Technology, University of Alicante, Carretera San Vicente del Raspeig s/n, 03690 Alicante, Spain (E-mail: amartinez@dtic.ua.es).
Aditya Sood , A.K. Sood is with the Department of Computer Science and Engineering, Michigan State University, East Lansing, USA, 48824- 1226.(email:soodadit@msu.edu)
Hui Shen , H. Shen is with Department of Computer Science, University of Texas at San Antonio, Texas, TX 78249 (Email: huishen12@gmail.com).
Song Fang , Song Fang is with the Department of Computer Science and Engineering, University of South Florida, Tampa, FL.(email:songf@mail.usf.edu)
Michael Backes , Michael Backes is with CISPA, Saarland University Germany.(email:backes@cs.uni-saarland.de)
Shaoquan Jiang , Shaoquan Jiang is with the Institute of Information Security, Mianyang Normal University, Mianyang, China 621000.(email:shaoquan.jiang@gmail.com)
Xun Yi , Xun Yi is with the School of Computer Science and Information Technology, RMIT University, Melbourne, Victoria 3001, Australia. (email: xun.yi@rmit.edu.au)
Yuan Cheng , Yuan Cheng is with the University of Texas at San Antonio, USA. (email: yuan@ycheng.org)
Imran Erguler , Imran Erguler is with the National Research Institute of Electronics & Cryptology TUBITAK-BILGEM, 41470 Gebze, Kocaeli, Turkey. (email: imran.erguler@tubitak.gov.tr)
Hongwei Li , Hongwei Li is with the School of Computer Science and Engineering, University of Electronic Science and Technology of China, Chengdu, Sichuan, China.(email; hongweili@uestc.edu.cn)
Hussain Almohri , Hussain M.J. Almohri is with the Department of Computer Science, Kuwait University, Kuwait. (email: almohri@cs.ku.edu.kw.)
Markus Riek , Markus Riek is with the Institute of Computer Science, University of Innsbruck, Austria. (e-mail: Markus.Riek@uibk.ac.at).
Stijn Volckaert , Stijn Volckaert is with the Computer Systems Lab, Department of Electronics and Information Systems, Ghent University, Sint- Pietersnieuwstraat 41, 9000 Gent, Belgium. (email: stijn.volckaert@elis.ugent.be)
Zhi Yang , Zhi Yang is with the Department of Electrical and Computer Engineering, Peking University, Beijing 80071, P.R. China. (e-mail: yangzhiatpku@gmail.com).
Lianshan Sun , Lianshan Sun is with Shaanxi Univ. of Science and Technology, China; (e-mail: sunlianshan@gmail.com).
Arcangelo Castiglione , Arcangelo Castiglione is with the Dipartimento di Informatica, Universita di Salerno, Fisciano, Salerno, 84084, Italy
Xian Pan , Xian Pan is with the SimpliVity Corporation, Westborough, MA 01581. (email: panxian1212@gmail.com.)
Bharath Samanthula , Bharath K. Samanthula is with the Department of Computer Science, Purdue University, 305 N. University Street, West Lafayette, IN 47907. (E-mail: bsamanth@purdue.edu)
Chi-Wei Wang , Chi-Wei Wang is with the Department of Computer Science and Information Engg., National Chiao tung University, Taiwan(Email: cwwangabc@gmail.com )
Ali Fattaholmanan , Ali Fattaholmanan is with the Department of Computer Engineering, Sharif University of Technology (SUT). (email: fattah@ce.sharif.edu)
Feng Hao , Feng Hao is with the School of Computing Science, Newcastle University, UK. (email: feng.hao@ncl.ac.uk)
Pradhumna Shrestha , Pradhumna L. Shrestha is with the Department of Computer and Electronics Engineering, University of Nebraska-Lincoln, 1110 S. 67th St., Omaha, NE 68182, USA. (email: shrestha.pradhumna@huskers.unl.edu)
Kerem Kaynar , Kerem Kaynar is with the GT-ARC, TU Berlin, Berlin, 10587,GERMANY. (email: kerem.kaynar@dai-labor.de)
Xianping Mao , Xianping Mao is with the Department of Computer Science and Engineering, Shanghai Jiao Tong University, Shanghai 200240, China.(Email: maoxp@sjtu.edu.cn)
Yang Liu , Yang Liu is with the Department of Electrical and Computer Engineering, Iowa State University, Ames, IA, 50010.(email: yangl@iastate.edu)
Gregory Levitin , Gregory Levitina is with the Collaborative Autonomic Computing Laboratory, School of Computer Science, University of Electronic Science and Technology of China (email: levitin@iec.co.il).
Ing-Ray Chen , Ing-Ray Chen is with the Department of Computer Science, Virginia Tech, Falls Church, VA 22043 (e-mail: irchen@vt.edu).
Marie Vasek , Marie Vasek is with the Darwin Deason Institute for Cyber Security, Southern Methodist University, Dallas, TX.(email: mvasek@smu.edu)
Rajkumar P.V. , Rajkumar P.V is a postdoctoral fellow in the Institute for Cyber Security, University of Texas at San Antonio, TX 78249, USA. (email: rajkumarpv@gmail.com)
Christoph Borchert , Christoph Borchert is with the Department of Computer Science 12, Technische Universität Dortmund, Germany. (email: christoph.borchert@tu-dortmund.de)
Barbara Carminati , Barbara Carminati is with the Department of Theoretical and Applied Science University of Insubria, Varese, Italy. (email:
Min-Te Sun , Min-Te Sun is with the Department of Computer Science and Information Engineering, National Central University, Taoyuan 320, Taiwan. (email: msun@csie.ncu.edu.tw)
Kazuya Sakai , Min-Te Sun is with the Department of Computer Science and Information Engineering, National Central University, Taoyuan 320, Taiwan. (email: msun@csie.ncu.edu.tw)
Javier Camara , J. Camara is with the Institute for Software Research, Carnegie MellonUniversity, USA.(email:jcmoreno@cs.cmu.edu)
Yi Han , Yi Han is with the Department of Computing and Information Systems, The University of Melbourne, Melbourne, Australia 3010. (email:an-drew.hanyi@gmail.com)
Yuchang Mo , Yuchang Mo is with the Department of Computer Science and Technology, Zhejiang Normal University, Jinhua 321004, China.(Email: myc@zjnu.cn)
Chunhua Su , C. Su is with School of Information Science, Japan Advanced Institute of Science and Technology, 1-1 Asahidai, Nomi, Ishikawa, 923-1292 Japan, and State Key Laboratory of Cryptology, P. O. Box 5159, Beijing, 100878,China.(email:chsu@jaist.ac.jp)
Hossein Pilaram , Hossein Pilaram is with Department of Electrical Engineering, Sharif University of Technology, Tehran, Iran.(email:h pilaram@ee.sharif.edu)
Yuan Zhang , Yuan Zhang is with State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210023, China. Sheng Zhong is the corresponding author.(email:zhangyuan05@gmail.com)
Yang Liu , Yang Liu is with the Department of Electrical and Computer Engineering, Michigan Technological University, Houghton, MI, 49931, USA (e-mail: yliu18@mtu.edu).
Adel El-Atawy , A. El-Atawy is with the School of Computing, DePaul Unviersity, Chicago, IL, 60604 USA.(email:aelatawy@cs.depaul.edu)
Zhi-jun Wu , Zhi-jun Wu is with the Tianjin Key Laboratory for Advanced Signal Processing, Civil Aviation University of China. (e-mail: zjwu@cauc.edu.cn).
James Anderson , J. W. Anderson is with the Department of Computer Science and Engineering, University of California San Diego.(email:jwanderson@cs.ucsd.edu)
Hyungon Moon , Hyungon Moon is with the Seoul National University (e-mail: hgmoon@sor.snu.ac.kr).
Wooguil Pak , W. Pak is with the Computer Engineering Department, Keimyung University, Daegu, Korea.(email:wooguilpak@kmu.ac.kr
Kaihe Xu , Kaihe Xu is with the Department of Electrical and Computer Engineering, Gainesville, FL 32611, USA. (e-mail: xukaihe@ufl.edu).
Jin Bum Hong , Jin B. Hong is with the Department of Computer Science and Software Engineering, University of Canterbury, New Zealand. (e-mail: jho102@uclive.ac.nz)
Stanislav Ponomarev , Stanislav Ponomarev is with the Ph.D. candidate with the College of Engineering and Science, Louisiana Tech University, Ruston, LA 71272 (e-mail: spo013@latech.edu).
Jingwei Li , Jingwei Li is with the College of Computer and Control Engineering, Nankai University, P.R. China (email: lijw1987@gmail.com)
Mohammad Ashiqur Rahman , Mohammad Ashiqur Rahman is with the Department of Software and Information Systems, University of North Carolina at Charlotte, North Carolina, USA. (email: mrahman4@uncc.edu)
Raphael Barazzutti , Emanuel Onica is with Alexandru Ioan Cuza University of Ia¸si, Romania; other authors are with the Institute of Computer Science, Universite de Neuchatel, Switzerland.(email:eonica@info.uaic.ro)
AbdelRahman Abdou , A. Abdou is with the Department of Systems and Computer Engineering, Carleton University.
Guanyu Tian , Guanyu Tian is with the Department of Mathematics and Computer Science, Fontbonne University, Clayton, MO, 63105, USA (email: gtian@fontbonne.edu)
Zhenhai Duan , Guanyu Tian is with the Department of Mathematics and Computer Science, Fontbonne University, Clayton, MO, 63105, USA (email: gtian@fontbonne.edu)
Todd Baumeister , Guanyu Tian is with the Department of Mathematics and Computer Science, Fontbonne University, Clayton, MO, 63105, USA (email: gtian@fontbonne.edu)
Yingfei Dong , Guanyu Tian is with the Department of Mathematics and Computer Science, Fontbonne University, Clayton, MO, 63105, USA (email: gtian@fontbonne.edu)
Yogachandran Rahulamathavan , Yogachandran Rahulamathavan is with the Information Security Group, School of Engineering and Mathematical Sciences, City University London, EC1V 0HB, London, U.K. Email:-yogachandran. rahulamathavan.1@city.ac.uk
Muttukrishnan Rajarajan , Yogachandran Rahulamathavan is with the Information Security Group, School of Engineering and Mathematical Sciences, City University London, EC1V 0HB, London, U.K. Email:-yogachandran. rahulamathavan.1@city.ac.uk
EHAB ELMALLAH , Ehab S. Elmallah is with the Department of Computing Science, University of Alberta, Edmonton, T6G 2E8, Canada.
Mohamed Gouda , Ehab S. Elmallah is with the Department of Computing Science, University of Alberta, Edmonton, T6G 2E8, Canada.
Michael Watson , Michael R. Watson is with the School of Computing and Communications at Lancaster University, UK.(Email: mrmrwat@gmail.com)
Brian Krupp , Brian Krupp is with the Computer Science Department, Baldwin Wallace University. E-mail: bkrupp@bw.edu
Nigamanth Sridhar , Brian Krupp is with the Computer Science Department, Baldwin Wallace University. E-mail: bkrupp@bw.edu
Wenbing Zhao , Brian Krupp is with the Computer Science Department, Baldwin Wallace University. E-mail: bkrupp@bw.edu
Khaled Rabieh , Khaled Rabieh is with the Department of Electrical & Computer Engineering, Tennessee Tech University, Cookeville, TN 38505 USA. (e-mail: kmrabieh42@students.tntech.edu).
Marco Tiloca , Marco Tiloca is with the SICS Swedish ICT AB, Kista, Sweden (email: marco@sics.se).
Md Bhuiyan , Md Zakirul Alam Bhuiyan is with the School of Information Science and Engineering, Central South University, Changsha, China, 410083.(Email: zakirulalam@gmail.com)
Yao Zheng , Yao Zheng is with the Department of Computer Science, Virginia Tech, USA.(Email: zhengyao@vt.edu)
Hongbo Liu , Hongbo Liu is with the Department of Computer Information and Graphics Technology, Indiana University Purdue University at Indianapolis, IN 46202.(email:hl45@iupui.edu)
Daibin Wang , D. Wang is with the Services Computing Technology and System Lab, Cluster and Grid Computing Lab, School of Computer Science and Technology, Huazhong University of Science and Technology, Wuhan, 430074, China.(email:daibinwang@hust.edu.cn)
Manuel Egele , Manuel Egele is with Boston University.(email:megele@bu.edu)
Basit Shafiq , Basit Shafiq is with the Department of Computer Science, Lahore University of Management Sciences, Pakistan.(email:basit@lums.edu.pk)
Shouling Ji , S. Ji, is with the School of Electrical and Computer Engineering, Georgia Institute of Technology, Atlanta, GA, 30332.(email:sji@gatech.edu)
Shams Zawoad , Shams Zawoad is with the Department of Computer and Information Science, University of Alabama at Birmingham, Birmingham, AL 35294-1170 USA. (email: zawoad@uab.edu)
Ji Zhang , Ji Zhang is with the University of Southern Queensland, Australia.(Email: zhangji77@gmail.com)
Slawomir Goryczka , Slawomir Goryczka is with the Department of Mathematics & Computer Science, Emory University, Atlanta, GA, USA.(Email: sgorycz@alumni.emory.edu)
SeongHan Shin , SeongHan Shin is with the Research Institute for Secure Systems (RISEC), National Institute of Advanced Industrial Science and Technology (AIST), Ibaraki, 305-8568 Japan. (email: seonghan.shin@aist.go.jp)
Qi Li , Qi Li is with the Graduate School at Shenzhen, Tsinghua University, Shenzhen China 518055, and Institute for Cyber Security, The University of Texas at San Antonio, San Antonio, TX 78249 (e-mail: leechqli@gmail.com).
Tassos Dimitriou , Tassos Dimitriou is with the Computer Engineering Dept. Kuwait University, Kuwait. Research supported by Kuwait University, Research grant no. QE02/13 (e-mail: tassos.dimitriou@ieee.org).
Pietro Colombo , Pietro Colombo is with Dipartimento di Scienze Teoriche e Applicate Universit a degli Studi dell’Insubria, Varese, Italy.(email:pietro.colombo@uninsubria.it)
George Bissias , George Bissias is with the College of Information and Computer Sciences at the University of Massachusetts Amherst.(email:gbiss@cs.umass.edu)
Peng Zhang , Peng Zhang is with Dept. of Computer Science and Technology, Xi’an Jiaotong University, Xi’an, China.(email:p-zhang@xjtu.edu.cn)
Alptekin Kupcu , Alptekin Kupcu is with the Koc University. (email: akupcu@ku.edu.tr)
Marco Bonola , Marco Bonola is with the University of Rome Tor Vergata.(Email: marco.bonola@uniroma2.it)
Hui Ma , Hui Ma is with the State Key Laboratory of Information Security, Institute of Information Engineering, Chinese Academy of Sciences, Beijing 100093, China.(Email: mahui@iie.ac.cn)
Zequ Yang , Zequ Yang is with the State Key Laboratory of Industrial Control Technology, Zhejiang University, Hangzhou, China.(email: yzqcjdtc@gmail.com)
Yuchang Mo , Yuchang Mo is with the Department of Computer Science and Technology, Zhejiang Normal University, Jinhua 321004, China. (e-mail: myc@zjnu.cn).
Reza Azarderakhsh , R. Azarderakhsh is with the Department of Computer Engineering, Rochester Institute of Technology, Rochester, New York, USA.(email:rxaeec@rit.edu)
Fumio Machida , Fumio Machida is with the NEC Corporation, Kawasaki, Kanagawa, 211-8666, JAPAN.(email: f-machida@ab.jp.nec.com)
Dongdong Zhao , Dongdong Zhao is with the University of Science and Technology of China, School of Computer Science and Technology, Hefei, Anhui, China. (email: zdd@mail.ustc.edu.cn)
Peng Zhou , Peng Zhou is with the Shanghai University, The Hong Kong Polytechnic University (e-mail: pzhou@shu.edu.cn).
Arash Nourian , Arash Nourian is with the Massachusetts Institute of Technology (MIT), Cambridge, MA, USA.(Email: nourian@mit.edu)
Saurabh Shintre , Saurabh Shintre is with CyLab and the Department of Electrical and Computer Engineering, Carnegie Mellon University, Pittsburgh, PA 15217 as well as Instituto de Telecomunicacoes and the Department of Electrical and Computer Engineering, Universidade do Porto, Porto, 4200-393, Portugal.
Virgil Gligor , Saurabh Shintre is with CyLab and the Department of Electrical and Computer Engineering, Carnegie Mellon University, Pittsburgh, PA 15217 as well as Instituto de Telecomunicacoes and the Department of Electrical and Computer Engineering, Universidade do Porto, Porto, 4200-393, Portugal.
Joao Barros , Saurabh Shintre is with CyLab and the Department of Electrical and Computer Engineering, Carnegie Mellon University, Pittsburgh, PA 15217 as well as Instituto de Telecomunicacoes and the Department of Electrical and Computer Engineering, Universidade do Porto, Porto, 4200-393, Portugal.
Amit Datta , Amit Datta is with the Department of Electrical and Computer Engineering, Carnegie Mellon University, Pittsburgh.(Email: amitdatta@cmu.edu)
Jiaojiao Jiang , J. Jiang is with the School of Information Technology, Deakin University, VIC 3125, Australia.(email:jjiaoj@deakin.edu.au)
Domenico Cotroneo , Domenico Cotroneo is with the Department of Electrical Engineering and Information Technologies (DIETI), Federico II University of Naples, Italy.(email:cotroneo@unina.it)
Papers
Xin Li , George Mason University, Fairfax
Xinyuan Wang , George Mason University, Fairfax
Wentao Chang , George Mason University, Fairfax
16 ms
(Ver 2.0)

Marketing Automation Platform


text:
> > What is the integral of x times the square root of 3-7x squared?

# What is the integral of x times the square root of 3-7x squared?

## What is the integral of x times the square root of 3-7x squared?

191 Views

### What is the integral of x times the square root of 3-7x squared?

What is the integral of x times the square root of 3-7x squared?

$$\int x \sqrt{3-7 x^2} dx = -\frac{(\sqrt{3-7 x^2})^3}{21} +const.$$


text:
# Homework Help: Find all solutions of the equation 2^x+3^y=z^2

1. Feb 23, 2012

### .d9n.

1. The problem statement, all variables and given/known data

Find all solutions in non-negative integers x, y, z of the equation
2^x + 3^y= z^2

2. Relevant equations

3. The attempt at a solution
not entirely sure how to go about it, im assuming maybe logarithms?

2=log(base Z) (2^x+3^y)

or maybe substitution

let
u=2^x so x=log(base 2)(u)
v=3^y so y=log(base 3)(v)
w=z^2 so 2=log(base z)(w)

u+v=w → 2^(log(base 2)(u))+3^(log(base 3)(v))=2^(log(base z)(w))

2. Feb 23, 2012

### morphism

Where is this from? The first thing I tried worked, but it produced a fairly long-winded solution so I'm reluctant to share it in case there's a simpler method... But here goes: Begin by considering your equation modulo 8, keeping in mind that z can't be divisible by 2.

3. Mar 1, 2012

### .d9n.

wasn't too sure what you mean with the modulo 8,
but this is what i have so far
so z cant be even as its equal to an odd plus an even number = odd
so when z=0, x=3 then z=3 and when y=2, x=4 then z=5
so if z^2-3^y has to be a perfect square then y has to be even and a power of 2 i.e.
2^x=z^2-3^y → 2^x = (z-3^2^w)^2

4. Mar 2, 2012

### .d9n.

so far i have

2^x + 3^y = z^2 [1]
where x, y, and z are non-negative integers.
We can see that [1] is a congruence modulo 8:
3^y = z^2 (mod 8) [2]
When z=1 and and y=2 we have
3^2 = 1 (mod 8) [3]
and by Fermat's theorem. So this means that y must be even.
As y is even, we can write y = 2k for some integer k. So we have:
3^2k + 2^x = z^2
z^2 - 3^2k = 2^x
(z + 3^k)(z - 3^k) = 2^x [4]
This means that the left hand side must be a power of 2, and therefore each factor i.e. (z+3^k) must also be a power of 2. But its not possible to have both factors on the left hand side divisible by 8, as this would imply that their difference
(z + 3^k) - (z - 3^k) = 2*3^k
would be divisible by 8, which is clearly impossible. The only power of 8 that is not a multiple of 8 is 8^0 = 1. So therefore one of the factors must be 1, and this is obviously the smaller factor; we have:
z- 3^k = 1
z = 3^k + 1 [5]
If we substitute that into [4], we obtain:
(3^k+1+3^k )(3^k+1-3^k )=2^x
2∙3^k + 1 = 2^x
2∙3^k = 2^x - 1 [6]
and this means that 2^x - 1 must be twice a power of 3.
So if k = 0, we have 2^x - 1 = 2, which doesn’t work. If k = 1, we have:
6 = 2^x - 1
where the LHS comes out even and the RHS comes out odd, so think i may have gone wrong somewhere, any ideas?

5. Mar 9, 2012

### morphism

Sorry, I'm too tired to read all that, so let me indicate what I'd meant with my hint.

Looking at the equation mod 8 and mod 3, and using the fact that $2\nmid z$ and $3\nmid z$, we can conclude that x and y must be even. Thus the equation $$(2^{x/2})^2 + (3^{y/2})^2 = z^2$$ is primitive Pythagorean, and the solutions to such equations are fully known (google it).

If you write down a parametrization for these Pythagorean triples, and use the fact that the only integer solutions to $$2^a = 3^b + 1$$ are $(a,b) \in \{(1,0), (2,1)\}$ (easy to prove), you should be able to obtain all positive integral solutions (x,y,z) to the original equation. (I got (3,0,3) and (4,2,5) as the only solutions.)

6. Mar 12, 2012

### .d9n.

this is what i have so far, but think i may have gone wrong somewhere, any ideas?

We are looking for solutions of:
2^x + 3^y = z^2 [1]
where x, y, and z are non-negative integers.
We can see that [1] is a congruence modulo 8:
3^y = z^2 (mod 8) [2]
When z=1 and and y=2 we have
3^2 = 1 (mod 8) [3]
and by Fermat's theorem. So this means that y must be even.
As y is even, we can write y = 2k for some integer k. So we have:
3^2k + 2^x = z^2
z^2 - 3^2k = 2^x
(z + 3^k)(z - 3^k) = 2^x
We can see that [1] is a congruence modulo 3:
2^x = z^2 (mod 3) [4]
When z=1 and and y=2 we have
2^x = 1 (mod 3) [5]
and by Fermat's theorem. So this means that x must be even.
As x is even, we can write x = 2k for some integer l. So we have:
3^y + 2^2l = z^2
z^2 - 2^2l = 3^y
(z + 2^l)(z - 2^l) = 3^y
So we are left with
2^2l + 3^2k = z^2
(2^l )^2+ (3^k )^2=z^2 [6]
Which is a Pythagorean triple, where a^2+b^2=c^2. Where a=2^(x/2),b=3^(y/2) and c=z, we can assume that a,b,c are coprime due to Fermat’s Lemma.
We know that c has to be odd because if we assume c is even, then there exists another value C such that c=2∙C. Also that c^2 is divisible by 4 since
c^2=(2C)^2 =4C^2
We know a and b must be odd because a,b,c are coprime. As a and b are odd there must exist values A and B such that
a=2A+1,b=2B+1
but a^2+b^2 cannot be divisible by 4 since
a^2+b^2=(2A+1)^2+(2B+1)^2=4A^2+4A+1+4B^2+4B+1=4(A^2+A+B^2+B)+2
we have a contradiction so c is odd.
So we have a^2=(c+b)(c-b)and c+b and c-b must be even since c and b are odd. So therefore there must exist u,v,w such that
a=2u,c+b=2v,c-b=2w
which means that (2u)^2=(2v)(2w) dividing both sides by 4 gives us u^2=vw.
If we assume v and w are not coprime, then there exists d such that d>1 and d divides both v,w, then d divides both v+w and v-w, but
c+b +c-b=2v+2w
so 2c=2v+2w which means that c=v+w so d divides c.
Also c+b-(c+b)=2v-2w. So 2b=2v-2w which means that b=v-w, so d divides b. Which is a contradiction as c and b are coprime from [6].
So we reject our assumption and v and w are coprime. By properties of coprimes we know that v and w are squares of themselves. So there exists p,q such that
v=p^2,w=q^2
and we have our solutions since
c=v+w=p^2+q^2
b=v-w=p^2-q^2
a=2u=2pq (As u^2=vw which means u=pq)
We know p,q are relatively prime and opposite parity as z is odd, so we are left with.
(p^2+q^2)=(2pq)^2+(p^2-q^2 )^2

so z=c=v+w=p^2+q^2,3^(y/2)=b=v-w=p^2-q^2 and 2^((x/2) )=a=2u=2pq

7. Mar 28, 2012

### morphism

Okay, so we know that 2^(x/2), 3^(y/2) and z are a primitive Pythagorean triple. This means that we can write 2^(x/2)=2nm, 3^(y/2)=n^2-m^2 and z=n^2+m^2 for some integers n and m, with only n even (say). From the first of these equations we find that m=1 and n=2^(x/2 - 1). But then the second equation becomes 3^(y/2) = 2^(x-2) - 1.

This is an equation of the form 2^a = 3^b + 1, and we are looking for integral solutions to such an equation. This forces $b\geq0$ (for otherwise 2^a won't be an integer), which in turn implies that $a\geq1$. I claim that $a \leq 2$ as well. Indeed, if a>2, then 3^b+1=0 mod 8, and this leads to a contradiction. Thus a is either 1 or 2. From here it's easy to see that the only possible solutions (a,b) are (1,0) and (2,1).

Returning to our problem, we see that $(x-2,y/2) \in \{(1,0), (2,1)\}$. You can take it from here.


text:
# Publications

2018
Dutt, Avik, Chaitanya Joshi, Xingchen Ji, Jaime Cardenas, Yoshitomo Okawachi, Kevin Luke, Alexander L. Gaeta, and Michal Lipson. “On-chip dual-comb source for spectroscopy.” Science Advances 4, no. 3 (2018). Publisher's Version Abstract
Dual-comb spectroscopy is a powerful technique for real-time, broadband optical sampling of molecular spectra, which requires no moving components. Recent developments with microresonator-based platforms have enabled frequency combs at the chip scale. However, the need to precisely match the resonance wavelengths of distinct high quality-factor microcavities has hindered the development of on-chip dual combs. We report the simultaneous generation of two microresonator combs on the same chip from a single laser, drastically reducing experimental complexity. We demonstrate broadband optical spectra spanning 51 THz and low-noise operation of both combs by deterministically tuning into soliton mode-locked states using integrated microheaters, resulting in narrow (< 10 kHz) microwave beat notes. We further use one comb as a reference to probe the formation dynamics of the other comb, thus introducing a technique to investigate comb evolution without auxiliary lasers or microwave oscillators. We demonstrate high signal-to-noise ratio absorption spectroscopy spanning 170 nm using the dual-comb source over a 20-μs acquisition time. Our device paves the way for compact and robust spectrometers at nanosecond time scales enabled by large beat-note spacings (> 1 GHz).
2017
Stern, Brian, Xingchen Ji, Avik Dutt, and Michal Lipson. “Compact narrow-linewidth integrated laser based on a low-loss silicon nitride ring resonator.” Optics Letters 42, no. 21 (2017): 4541-4544. Publisher's Version Abstract
We design and demonstrate a compact, narrow-linewidth integrated laser based on low-loss silicon nitride waveguides coupled to a III-V gain chip. By using a highly confined optical mode, we simultaneously achieve compact bends and ultra-low loss. We leverage the narrowband backreflection of a high-Q microring resonator to act as a cavity output mirror, a single-mode filter, and a propagation delay all in one. This configuration allows the ring to provide feedback and obtain a laser linewidth of 13 kHz with 1.7 mW output power around 1550 nm. This demonstration realizes a compact sub-millimeter silicon nitride laser cavity with a narrow linewidth.
Yu, Mengjie, Jae K Jang, Yoshitomo Okawachi, Austin G Griffith, Kevin Luke, Steven A Miller, Xingchen Ji, Michal Lipson, and Alexander L Gaeta. “Breather soliton dynamics in microresonators.” Nature Communications 8 (2017): 14569. Publisher's Version Abstract
The generation of temporal cavity solitons in microresonators results in coherent low-noise optical frequency combs that are critical for applications in spectroscopy, astronomy, navigation or telecommunications. Breather solitons also form an important part of many different classes of nonlinear wave systems, manifesting themselves as a localized temporal structure that exhibits oscillatory behaviour. To date, the dynamics of breather solitons in microresonators remains largely unexplored, and its experimental characterization is challenging. Here we demonstrate the excitation of breather solitons in two different microresonator platforms based on silicon nitride and on silicon. We investigate the dependence of the breathing frequency on pump detuning and observe the transition from period-1 to period-2 oscillation. Our study constitutes a significant contribution to understanding the soliton dynamics within the larger context of nonlinear science.
Miller, Steven A, Mengjie Yu, Xingchen Ji, Austin G Griffith, Jaime Cardenas, Alexander L Gaeta, and Michal Lipson. “Low-Loss Silicon Platform for Broadband Mid-Infrared Photonics.” arXiv:1703.03517 (2017). Publisher's Version Abstract
Broadband mid-infrared (mid-IR) spectroscopy applications could greatly benefit from today's well-developed, highly scalable silicon photonics technology; however, this platform lacks broadband transparency due to its reliance on absorptive silicon dioxide cladding. Alternative cladding materials have been studied, but the challenge lies in decreasing losses while avoiding complex fabrication techniques. Here, in contrast to traditional assumptions, we show that silicon photonics can achieve low-loss propagation in the mid-IR from 3 - 6 um wavelength, thus providing a highly scalable, well-developed technology in this spectral range. We engineer the waveguide cross section and optical mode interaction with the absorptive cladding oxide to reduce loss at mid-IR wavelengths. We fabricate a microring resonator and measure an intrinsic quality (Q) factor of 10^6 at wavelengths from 3.5 to 3.8 um. This is the highest Q demonstrated on an integrated mid-IR platform to date. With this high-Q silicon microresonator, we also demonstrate a low optical parametric oscillation threshold of 5.2 mW, illustrating the utility of this platform for nonlinear chip-scale applications in the mid-IR.
Ji, Xingchen, Felippe AS Barbosa, Samantha P Roberts, Avik Dutt, Jaime Cardenas, Yoshitomo Okawachi, Alex Bryant, Alexander L Gaeta, and Michal Lipson. “Ultra-low-loss on-chip resonators with sub-milliwatt parametric oscillation threshold.” Optica 4, no. 6 (2017): 619. Publisher's Version Abstract
On-chip optical resonators have the promise of revolutionizing numerous fields including metrology and sensing; however, their optical losses have always lagged behind their larger discrete resonator counterparts based on crystalline materials and flowable glass. Silicon nitride (Si3N4) ring resonators open up capabilities for optical routing, frequency comb generation, optical clocks and high precision sensing on an integrated platform. However, simultaneously achieving high quality factor and high confinement in Si3N4 (critical for nonlinear processes for example) remains a challenge. Here, we show that addressing surface roughness enables us to overcome the loss limitations and achieve high-confinement, on-chip ring resonators with a quality factor (Q) of 37 million for a ring with 2.5 {\mu}m width and 67 million for a ring with 10 {\mu}m width. We show a clear systematic path for achieving these high quality factors. Furthermore, we extract the loss limited by the material absorption in our films to be 0.13 dB/m, which corresponds to an absorption limited Q of at least 170 million by comparing two resonators with different degrees of confinement. Our work provides a chip-scale platform for applications such as ultra-low power frequency comb generation, high precision sensing, laser stabilization and sideband resolved optomechanics.
2016
Joshi, Chaitanya, Jae K. Jang, Kevin Luke, Xingchen Ji, Steven A. Miller, Alexander Klenner, Yoshitomo Okawachi, Michal Lipson, and Alexander L. Gaeta. “Thermally controlled comb generation and soliton modelocking in microresonators.” Opt. Lett. 41 (2016): 2565–2568. Publisher's Version Abstract
We report, to the best of our knowledge, the first demonstration of thermally controlled soliton mode-locked frequency comb generation in microresonators. By controlling the electric current through heaters integrated with silicon nitride microresonators, we demonstrate a systematic and repeatable pathway to single- and multi-soliton mode-locked states without adjusting the pump laser wavelength. Such an approach could greatly simplify the generation of mode-locked frequency combs and facilitate applications such as chip-based dual-comb spectroscopy.
Jang, Jae K., Yoshitomo Okawachi, Mengjie Yu, Kevin Luke, Xingchen Ji, Michal Lipson, and Alexander L. Gaeta. “Dynamics of mode-coupling-induced microresonator frequency combs in normal dispersion.” Optics Express 24, no. 25 (2016): 28794 - 28803. Publisher's Version Abstract
We experimentally and theoretically investigate the dynamics of microresonator-based frequency comb generation assisted by mode coupling in the normal group-velocity dispersion (GVD) regime. We show that mode coupling can initiate intracavity modulation instability (MI) by directly perturbing the pump-resonance mode. We also observe the formation of a low-noise comb as the pump frequency is tuned further into resonance from the MI point. We determine the phase-matching conditions that accurately predict all the essential features of the MI and comb spectra, and extend the existing analogy between mode coupling and high-order dispersion to the normal GVD regime. We discuss the applicability of our analysis to the possibility of broadband comb generation in the normal GVD regime.
Dutt, Avik, Chaitanya Joshi, Xingchen Ji, Jaime Cardenas, Yoshitomo Okawachi, Kevin Luke, Alexander L. Gaeta, and Michal Lipson. “On-chip dual comb source for spectroscopy.” arXiv:1611.07673 [physics] (2016). Publisher's Version Abstract
Dual-comb spectroscopy is a powerful technique for real-time, broadband optical sampling of molecular spectra which requires no moving components. Recent developments with microresonator-based platforms have enabled frequency combs at the chip scale. However, the need to precisely match the resonance wavelengths of distinct high-quality-factor microcavities has hindered the development of an on-chip dual comb source. Here, we report the first simultaneous generation of two microresonator combs on the same chip from a single laser. The combs span a broad bandwidth of 51 THz around a wavelength of 1.56 \$\textbackslashmu\$m. We demonstrate low-noise operation of both frequency combs by deterministically tuning into soliton mode-locked states using integrated microheaters, resulting in narrow (\$\textless\$ 10 kHz) microwave beatnotes. We further use one mode-locked comb as a reference to probe the formation dynamics of the other comb, thus introducing a technique to investigate comb evolution without auxiliary lasers or microwave oscillators. We demonstrate broadband high-SNR absorption spectroscopy of dichloromethane spanning 170 nm using the dual comb source over a 20 \$\textbackslashmu\$s acquisition time. Our device paves the way for compact and robust dual-comb spectrometers at nanosecond timescales.


text:
Transport Capacity of Distributed Wireless CSMA Networks

Select |

Print

Yang, Tao; Mao, Guoqiang; Zhang, Wei; Tao, Xiaofeng

2014-11-02

Journal Article

IEEE Transaction on Wireless Communications

13

10

5635-5647

In this paper, we study the transport capacity of large multi-hop wireless CSMA networks. Different from previous studies which rely on the use of centralized scheduling algorithm and/or centralized routing algorithm to achieve the optimal capacity scaling law, we show that the optimal capacity scaling law can be achieved using entirely distributed routing and scheduling algorithms. Specifically, we consider a network with nodes Poissonly distributed with unit intensity on a $\sqrt{n}\times\sqrt{n}$ square $B_{n}\subset\Re^{2}$. Furthermore, each node chooses its destination randomly and independently and transmits following a CSMA protocol. By resorting to the percolation theory and by carefully tuning the three controllable parameters in CSMA protocols, i.e. transmission power, carrier-sensing threshold and count-down timer, we show that a throughput of $\Theta\left(\frac{1}{\sqrt{n}}\right)$ is achievable in distributed CSMA networks. Furthermore, we derive the pre-constant preceding the order of the transport capacity by giving an upper and a lower bound of the transport capacity. The tightness of the bounds is validated using simulations.

Data61; NICTA; Capacity; per-node throughput; CSMA; wireless networks

English

nicta:8166

Yang, Tao; Mao, Guoqiang; Zhang, Wei; Tao, Xiaofeng. Transport Capacity of Distributed Wireless CSMA Networks. IEEE Transaction on Wireless Communications. 2014-11-02; 13(10):5635-5647. https://doi.org/10.1109/TWC.2014.2325899