IndisputableMonolith.Physics.PlanetStrataC2

   1import Mathlib
   2import IndisputableMonolith.Foundation.RSCoupledAxis
   3import IndisputableMonolith.Physics.AtmosphericPhysicsFromRS
   4import IndisputableMonolith.Physics.GeophysicsFromRS
   5import IndisputableMonolith.Physics.OceanographyFromRS
   6
   7/-!
   8# C2: Planetary 15-Stratum Direct Sum
   9
  10The planet carries three independent 5-strata stacks:
  11
  12* atmosphere,
  13* solid Earth,
  14* ocean.
  15
  16This is an RS disjoint sum, not a tensor product. A physical parcel belongs
  17to one stratum in one stack; the three stacks add to 15 = 3 x 5.
  18
  19The wave-speed phi-ratio prediction remains empirical. This module only proves
  20the finite structural claim.
  21
  22Lean status: 0 sorry, 0 axiom.
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Physics
  27namespace PlanetStrataC2
  28
  29open Foundation.RSCoupledAxis
  30open AtmosphericPhysicsFromRS
  31open GeophysicsFromRS
  32open OceanographyFromRS
  33
  34def atmosphereAxis : CoupledAxis 5 where
  35  Ix := AtmosphericLayer
  36  finite := inferInstance
  37  card_eq := atmosphericLayerCount
  38  primitive := RSPrimitive.phiLadder
  39
  40def earthAxis : CoupledAxis 5 where
  41  Ix := EarthLayer
  42  finite := inferInstance
  43  card_eq := earthLayerCount
  44  primitive := RSPrimitive.jCost
  45
  46def oceanAxis : CoupledAxis 5 where
  47  Ix := OceanLayer
  48  finite := inferInstance
  49  card_eq := oceanLayerCount
  50  primitive := RSPrimitive.sigmaCharge
  51
  52def planetStrataSum : RSDisjointSum3 5 where
  53  axis1 := atmosphereAxis
  54  axis2 := earthAxis
  55  axis3 := oceanAxis
  56  indep12 := by simp [independent, atmosphereAxis, earthAxis]
  57  indep13 := by simp [independent, atmosphereAxis, oceanAxis]
  58  indep23 := by simp [independent, earthAxis, oceanAxis]
  59
  60theorem planet_strata_total_15 :
  61    Fintype.card AtmosphericLayer + Fintype.card EarthLayer +
  62      Fintype.card OceanLayer = 15 := by
  63  rw [atmosphericLayerCount, earthLayerCount, oceanLayerCount]
  64
  65theorem planet_strata_disjoint_sum_15 :
  66    @Fintype.card planetStrataSum.axis1.Ix planetStrataSum.axis1.finite +
  67      @Fintype.card planetStrataSum.axis2.Ix planetStrataSum.axis2.finite +
  68      @Fintype.card planetStrataSum.axis3.Ix planetStrataSum.axis3.finite = 15 := by
  69  rw [disjoint_sum_card planetStrataSum]
  70
  71structure PlanetStrataCert where
  72  atmospheric_count : Fintype.card AtmosphericLayer = 5
  73  earth_count : Fintype.card EarthLayer = 5
  74  ocean_count : Fintype.card OceanLayer = 5
  75  total_15 : Fintype.card AtmosphericLayer + Fintype.card EarthLayer +
  76    Fintype.card OceanLayer = 15
  77  rs_sum_15 :
  78    @Fintype.card planetStrataSum.axis1.Ix planetStrataSum.axis1.finite +
  79      @Fintype.card planetStrataSum.axis2.Ix planetStrataSum.axis2.finite +
  80      @Fintype.card planetStrataSum.axis3.Ix planetStrataSum.axis3.finite = 15
  81
  82def planetStrataCert : PlanetStrataCert where
  83  atmospheric_count := atmosphericLayerCount
  84  earth_count := earthLayerCount
  85  ocean_count := oceanLayerCount
  86  total_15 := planet_strata_total_15
  87  rs_sum_15 := planet_strata_disjoint_sum_15
  88
  89end PlanetStrataC2
  90end Physics
  91end IndisputableMonolith
  92