Foundation Pair Kernel Newtonian3 Angular Fourier Leaf First Coord Of Archimedes

The Archimedes leaf

The declaration angular_fourier_leaf_firstCoord_of_archimedes is a proved theorem inside the framework's machine-checked library of formal mathematics. It establishes a specific angular identity: the first-coordinate marginal of the unit sphere's surface measure, a quantity Archimedes himself could have computed, is the input to a Fourier integral that later steps in the framework use. In plain terms, the theorem pins down how the surface area of a sphere is distributed when you look at it along one coordinate axis, and it does so without invoking any physics, lattice, or recognition machinery.

The result belongs to a larger proof campaign that isolates the factor 4π as a fact of pure three-dimensional geometry. The unit sphere in three-dimensional space has surface area 4π, and three times the volume of the unit ball is also 4π. The theorem in question takes one slice of that geometry: the measure you get by pushing the sphere's surface measure onto the first coordinate. That push-forward has total mass 4π and is supported on the interval from -1 to 1. The angular Fourier leaf then computes the Fourier transform of that marginal, giving a clean one-dimensional integral that later steps can use.

What the declaration does not claim is just as important as what it proves. The theorem does not assert that the first-coordinate marginal has density 2π on the interval; that statement, called Coord0ArchimedesMarginal, is explicitly stated but not proved in the same module. The theorem also does not establish the Newtonian Fourier target, the identity that would connect this geometry to an inverse-square law. That target is stated as a goal for a later rung, not proved here. The framework's discipline is precise: this declaration proves one angular identity, and it leaves the physical bridge open.

In Recognition Science, this result matters because it separates a geometric fact from a physical one. The 4π that appears in Newton's law of gravitation, the 4π that shows up in Coulomb's law, is here shown to be a property of three-dimensional space itself, not of any particular force or carrier. The theorem is a step toward reducing a constant of physics to a constant of geometry. But the step is deliberately narrow: it proves the angular identity, and it does not claim the bridge from geometry to force is complete.

private abbrev E2 := Fin 2 → ℝ

/-- The surface measure on the unit sphere in `ℝ³`, as obtained from Lebesgue
measure by Mathlib's generalized polar-coordinate construction. -/
abbrev sphereMeasure3 : Measure S2 := (volume : Measure E3).toSphere

/-- The push-forward of surface measure along the first coordinate. -/
abbrev coord0Marginal : Measure ℝ := Measure.map coord0 sphereMeasure3

What this page does not claim

The declaration does not prove that the first-coordinate marginal has density 2π on the interval. The declaration does not establish the Newtonian Fourier target identity. The declaration does not connect the geometric 4π to any physical force law.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PairKernelNewtonian3.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: