Physics Planet Strata C2

Planetary layers as a counted sum

In the Recognition Science framework, a planet's physical structure is treated as three independent stacks of layers: the atmosphere, the solid Earth, and the ocean. Each stack contains exactly five layers, and the three stacks are combined as a disjoint sum, meaning a physical parcel belongs to one layer in one stack, never to two at once. The total is therefore 3 × 5 = 15 distinct strata.

The module named PlanetStrataC2 establishes this finite structural claim as a theorem. It defines the three five-layer axes, proves that each has exactly five layers, and proves that the disjoint sum of the three axes has exactly fifteen layers. The proof is machine-checked with no gaps and no additional axioms.

This is a structural result, not a physical prediction. The module explicitly states that the wave-speed phi-ratio prediction remains empirical; it only proves the counting claim. In plain language: if you accept the framework's definition of five layers per stack, the arithmetic that three stacks make fifteen is forced and verified.

The three stacks are not identical in kind. The atmosphere axis uses a phi-ladder primitive, the solid Earth axis uses the j-cost primitive, and the ocean axis uses a sigma-charge primitive. These are different internal structures, but they share the same layer count of five. The disjoint sum treats them as independent, with no mixing between stacks.

def atmosphereAxis : CoupledAxis 5 where
  Ix := AtmosphericLayer
  finite := inferInstance
  card_eq := atmosphericLayerCount
  primitive := RSPrimitive.phiLadder

def earthAxis : CoupledAxis 5 where
  Ix := EarthLayer
  finite := inferInstance
  card_eq := earthLayerCount
  primitive := RSPrimitive.jCost

def oceanAxis : CoupledAxis 5 where
  Ix := OceanLayer
  finite := inferInstance
  card_eq := oceanLayerCount
  primitive := RSPrimitive.sigmaCharge

theorem planet_strata_disjoint_sum_15 :
    @Fintype.card planetStrataSum.axis1.Ix planetStrataSum.axis1.finite +
      @Fintype.card planetStrataSum.axis2.Ix planetStrataSum.axis2.finite +
      @Fintype.card planetStrataSum.axis3.Ix planetStrataSum.axis3.finite = 15 := by
  rw [disjoint_sum_card planetStrataSum]

What this page does not claim

The module does not prove that the five-layer structure is physically real. The module does not derive the wave-speed phi-ratio prediction. The three stacks are not claimed to be interchangeable or identical in structure.

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/Physics/PlanetStrataC2.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: