Parikshit Padole

I came across a LinkedIn post by a postdoctoral researcher working on something interesting. The first thing that caught my eye was his list of research interests. I always thought someone should focus on one specific domain like biology or physics and explore subfields within that. But this researcher was working at the intersection of mathematics, physics, and computer science.

That one word “intersection” clicked something in me. I realized it was possible to combine different interests in a meaningful way. I messaged him on LinkedIn, not really expecting a reply. After all, I was an undergrad from a different background, and he must have gotten a lot of messages. But to my surprise, he responded within minutes.

We scheduled a Zoom call for March 27th, 2025, and though I was excited, I had no clue what “Lean” was, or what “theorem proving” meant. I asked a few friends studying physics at Imperial to explain, and after some Googling, it started to make sense.

So, What Is Lean and Theorem Proving?

Let me explain it the way it started to make sense to me.

Take something simple:

“Every time I flip this switch, the light turns on.”

In everyday life, we’d just accept that as true. We’ve seen it happen. But a theorem prover  like Lean  doesn’t take your word for it.

It’s like a robot that says:

“Prove it. Show me the wiring, the power source, the bulb, the laws of electricity. No skipping.”

If you can explain every single logical step, it’ll say:

“Yes, this is probably true.”

But if something’s missing:

“Nope. Try again.”

It feels like overkill at first. But it starts to make sense when you think about systems where guessing or assuming just isn’t good enough.

Where Is This Actually Used?

Imagine the light switch isn’t just in your bedroom, it’s a switch on a rocket.

• “If the engine overheats, it shuts down safely.”
• “If a pacemaker detects a problem, it responds in under a second.”
• “If someone tries to hack the system, no data is leaked.”

In cases like these, ‘it worked when we tested it’ isn’t always enough. You need guarantees. That’s where formal verification and tools like Lean 4 comes in.

Meeting Dr. Joseph and Learning About PhysLean

That first Zoom call with Dr. Joseph really stayed with me. He turned out to be kind, welcoming, and genuinely interested in helping someone new understand the field. I thought the call might last 15 minutes. We ended up talking for over an hour. He even shared stories about his work at Reykjavik University in Iceland.

That conversation is what led me to PhysLean.

What Is PhysLean?

If you’ve heard of mathlib, the formal math library built using Lean  PhysLean is like its physics counterpart.

It’s an open-source library being developed in Lean 4, aiming to formalize major areas of physics in a way that computers can read, check, and reason through. It already includes areas like electromagnetism, condensed matter physics, classical mechanics, and quantum field theory and continues to grow.

The goal is to create a structured, formal foundation for physics where:

• Every law is written in a language a computer can understand
• Every equation is logically derived from first principles
• Every assumption is made explicit

Physics, as practiced, often hides small errors, forgotten approximations, missing units, implicit assumptions. Famously, NASA lost a $125 million Mars orbiter due to a simple unit conversion error.

Why It Matters

PhysLean is still in development, its potential spans research, engineering, and education:

• In self-driving cars, control systems could be proven safe, not just empirically tested.
• In quantum research, highly complex models could be logically verified.
• In education, students wouldn’t just use formulas, they’d see the logic behind them, step by step.

It’s not about replacing physics research, it’s about strengthening it.

What’s Next?

Since that first call, I’ve had more conversations with Dr. Joseph. We finally met in person at Imperial College London on June 13th. He shared that from September 2025, he’ll be joining the University of Bath as an Assistant Professor, where he plans to continue developing PhysLean and growing a lab around it.

It’s still early days for me, but that one LinkedIn post really did shift how I think about physics, programming, and what research can look like at the intersection of different fields.

Learn More

There’s much more to come with PhysLean. You can find more information below:
PhysLean Website: https://physlean.com/

GitHub: https://github.com/HEPLean/PhysLean

Dr. Joseph Tooby – Smith’s website: https://josephtoobysmith.com/

Read How I Ended Up Talking Physics with a Theorem Prover in full

Hello again! Welcome to the follow-up blog from the previous one where we discussed How Solar Radiation Pressure Affects Satellites: Calculating Instantaneous Force and Acceleration. As the title suggests, this time we’ll dive deeper into understanding how to calculate long-term orbital perturbations due to solar radiation pressure.

This is a vast topic, but my goal is to simplify it as much as possible for everyone. These blogs are aimed at providing a foundational introduction to the fascinating realm of orbital mechanics.

Now, I have a confession—if you’re a mathematician or physicist, can we have a video call? Sometimes I wonder if I should have pursued Astrophysics instead of diving into AI and Robotics. ? Just kidding! I’m much better in this field, and I can’t imagine myself knee-deep in equations with Einstein-style hair. At least, I like to think I’m cool… Please don’t get offended by my nerdy jokes!

Alright, enough yapping—let’s get back to the topic. To quickly recap what we discussed in the last blog:

Solar radiation pressure is the force exerted by photons emitted by the Sun when they strike a satellite’s surface. The magnitude of this pressure depends on:

• The satellite’s cross-sectional area exposed to sunlight,
• The reflectivity of its surfaces,
• Its orientation relative to the Sun,
• And its distance from the Sun (though for low Earth orbit, this is usually assumed constant).

While the force from solar radiation pressure is small, over time it can cause significant changes in a satellite’s orbital elements. In the last blog, we focused on calculating the immediate effect of this pressure, but not how it accumulates and affects the spacecraft over time.

This blog will cover exactly that.

To make it more realistic and understandable, we’ll use EIRSAT-1 as a case study—one of the most well-known student-led CubeSat missions, launched by the students of University College Dublin as part of the European Space Agency’s Fly Your Satellite! programme.

I didn’t find extensive details about the mission (Wikipedia had some info, but we all know how trustworthy that is), so I gathered what I could from official publications and real-time data from the n2yo website. As always, I’ll provide links below for anyone who wants to fact-check.

Now, let’s get all the information down properly and begin!

EIRSAT-1 Satellite Data
Latitude	-41.18°
Longitude	74.18°
Altitude	481.19 km (299 mi)
Speed	7.62 km/s (4.73 mi/s)
Azimuth	232.0° SW
Elevation	-55°
Right Ascension	07h 51m 50s
Declination	-60° 20′ 10”
Launch Mass	2.305 kg
Dimensions	10.67 cm × 10.67 cm × 22.7 cm (4.20 in × 4.20 in × 8.94 in)
Satellite Period	94 minutes

 

Now we have the data let’s try to understand how and what steps are we going to take also before that let’s list down the factors to consider when calculating the effect of solar radiation pressure on an object:

Factors to Consider for Solar Radiation Pressure Calculations:

Orbital Elements:

• Semi-major axis
• Eccentricity
• Inclination
• Right Ascension of Ascending Node (RAAN)
• Argument of Perigee
• True Anomaly
• Mean Anomaly
• Eccentric Anomaly

Satellite Geometry:

• Cross-sectional area
• Reflectivity data

Material Properties:

• Absorptivity and emissivity
• Degradation rates over time

Orientation Data:

• The satellite’s attitude and orientation over time

Distance to the Sun:

• Updated regularly throughout the year to account for orbital variations

 

Step-by-Step Calculation

Solar Radiation Pressure Calculation

We already know the formula for calculating solar radiation pressure:

 

Determine the Cross-Sectional Area: Using the dimensions of

EIRSAT-1 (10.67 cm × 10.67 cm × 22.7 cm), the cross-sectional area facing the Sun (depending on its orientation) could be approximated. For the largest face:

 

Force on the Satellite Due to Solar Radiation Pressure

We’ll calculate the force exerted by solar radiation pressure using the following formula:

 

Instantaneous Acceleration on the Satellite Due to Solar Radiation Pressure

We can calculate the acceleration using Newton’s second law:

 

Atmospheric Drag Force Formula

F_D is the drag force in Newtons,

C_D is the drag coefficient (typically between 2.0 and 2.5 for satellites),

A is the cross-sectional area of the satellite (0.00024228 m²),

ρ is the atmospheric density at the satellite’s altitude,

v² is the satellite’s velocity relative to the atmosphere (7.69 km/s).

 

Now we don’t know what is Atmospheric Density for that point of time so I used

NRLMSISE 2.0 is an empirical, global reference atmospheric model of the Earth from ground to space. It models the temperatures and densities of the atmosphere’s components.

Now we get,

 

let’s substitute it in the formula

 

Acceleration due to Drag

 

 

Now Finally,

Lagrange’s Planetary Equations:

You might wonder why we still need to use Lagrange’s planetary equations when we’ve already calculated the forces acting on the satellite. These equations allow us to determine how the orbital elements of a satellite (such as semi-major axis, eccentricity, inclination, and others) change over time due to external forces.

Since the focus of this blog is to calculate long-term orbital perturbations, Lagrange’s planetary equations provide a structured way to analyse the cumulative effects of small forces like solar radiation pressure (SRP) and atmospheric drag. They give us a clear picture of how a satellite’s orbit evolves over extended periods.

 

Above are the formulas for the  Lagrange’s Planetary Equations where

ȧ is the Semi-major Axis

ė is the Eccentricity

i̇ is the Inclination

ω̇ is the Argument of Perigee

Ω̇ is the Right Ascension of the Ascending Node

Ṫ is the Time (Orbital Period)

I will be creating a separate blog dedicated to solving these equations in detail. If you have the necessary data for your own satellite, you’ll be able to input it into the equations and follow along to solve for long-term orbital changes.

Disclaimer: I am not a mathematician or physicist; the information presented here is sourced from various online references, which I have linked below. If you have any suggestions or feedback, feel free to reach out to me at ppadole@imperial.ac.uk ?

References

General Perturbation Theory – Lagrange’s Planetary Equations, LibreTexts

Lagrange’s Planetary Equations, ASU Control Systems

EIRSAT-1 Conferences, EIRSAT-1 Official Website

Development, Description, and Validation of the Operations Manual for EIRSAT-1, Journal of Astronomical Telescopes, Instruments, and Systems

NRLMSIS Atmosphere Model

Read Long-Term Orbital Perturbations of Satellites Due to Solar Radiation Pressure in full

First of all, hello again! Apologies for the long break—final year kept me busy, along with my part-time work, so I didn’t have much time to post. But now that things have settled down, I’m excited to start sharing the blogs I’ve been planning. I’ll be posting regularly, starting with today’s topic.
In this blog, we’ll dive into Solar Radiation Pressure and explore how it affects satellites.
Let’s begin!
In space, even the smallest forces can have significant effects on satellites over time. One of the key forces acting on a satellite is solar radiation pressure.

What is Solar Radiation Pressure?
Solar radiation pressure is the force exerted by photons from the Sun as they strike and reflect off the surface of a satellite. While seemingly insignificant, the pressure can considerably impact a satellite’s orbit, particularly its perigee height especially over long durations.

This force depends on:

1. The satellite’s distance from the Sun.
2. The satellite’s cross-sectional area facing the Sun.
3. The reflective properties of the satellite’s surface

In the May 1960 paper, “The Influence of the Solar Radiation Pressure on the Motion of an Artificial Satellite,” researchers focused on the Vanguard I satellite, launched into Earth orbit on 17 March 1958. This satellite, intended for geodetic measurements, was designed with a diameter of 16.5 cm and a mass of 1.47 kg. Early orbit analyses of Vanguard I revealed unexpected discrepancies between the observed and predicted perigee heights.

The researchers explored solar radiation pressure as a potential cause for these deviations. Their investigation, using analytical methods to model the effects of solar radiation pressure on satellite orbits, indicated that this pressure significantly contributed to the observed perturbations in Vanguard I’s perigee height. This finding highlighted that even though solar radiation pressure is a relatively small force, it could cause substantial orbital deviations, particularly for satellites with a high area-to-mass ratio like Vanguard I.

So, how do we calculate solar radiation pressure and its effect on a satellite’s motion? Below, we’ll walk through the key steps and formulas that help determine the instantaneous force and acceleration on a satellite caused by this pressure.

Let’s break it down:

Step 1: Calculating Solar Radiation Pressure

Solar radiation pressure at Earth’s distance from the Sun is given by the following formula:

Where

P is the solar radiation pressure.

L is the Sun’s luminosity (3.828 ×10^26 W) .

r is the distance from the Sun (Earth’s distance is 1.496 × 10^11 m )

c is the speed of light (3×10^8 m/s)

 

Substituting Earth’s distance into this equation gives us a solar radiation pressure at Earth:
P ≈4.56 × 10^(-6) N/m^2

This value will be used to calculate the force acting on a satellite.

 

Step 2: Calculating the Force on the Satellite

Once we know the solar radiation pressure, we can calculate the force on the satellite. The force depends on the satellite’s cross-sectional area (A) and its reflectivity(ρ). The formula for the force is:

Where:

F is the force exerted on the satellite.

A is the satellite’s cross-sectional area in square meters.

ρ is the reflectivity coefficient (ranging from 0 for a perfectly absorbing surface to 1 for a perfectly reflective surface).

 

Example Calculation:

Let’s say a satellite has a cross-sectional area of 10 m² and reflects 30% of the radiation

(i.e ρ=0.3 ). The force acting on this satellite would be:

So, the instantaneous force acting on the satellite due to solar radiation pressure is F=5.928 ×10^(-4) N

 

Step 3: Calculating the Acceleration on the Satellite

Next, we calculate the acceleration on the satellite due to the solar radiation pressure. Acceleration is simply the force divided by the satellite’s mass ( ):

Where:

a is the acceleration

F is the force due to solar radiation pressure.

m is the mass of the satellite in kilograms.

Example Calculation:

For a satellite with a mass of 500 kg, the acceleration would be:

Although the force and acceleration caused by solar radiation pressure are small, they are persistent. Over time, they can lead to measurable changes in the satellite’s trajectory, especially for satellites with large area-to-mass ratios. For lightweight satellites, like CubeSats, solar radiation pressure can become a dominant factor affecting their orbits.

In terms of application this force can be utilised for example in solar sails the force from solar radiation pressure can be used  for propulsion, enabling satellites to move without fuel.

Conclusion

Solar radiation pressure, while small, exerts a continuous force on satellites. By calculating the instantaneous force and acceleration due to this pressure, we can understand how sunlight can gradually change a satellite’s orbit.

In future blogs, we will explore how this force can affect a satellite’s orbit over time, including resonant orbits and eccentricity changes

 

Disclaimer: I am not a mathematician or physicist; the information presented here is sourced from various online references, which I have linked below. If you have any suggestions or feedback, feel free to reach out to me at ppadole@imperial.ac.uk ?

Source List 

Comet Tails and Solar Radiation Pressure

NASA’s Explanation of Sunlight Exerting Pressure

Luminosity from Britannica

Photon Mass and Physics

Scientific Article on Solar Radiation Pressure

NASA Technical Report on Solar Radiation

Solar Radiation Pressure in Engineering

NSSDC Spacecraft Data on Vanguard I

SRP Image ESA

Read How Solar Radiation Pressure Affects Satellites: Calculating Instantaneous Force and Acceleration in full