Atlas Controls Shear
DefinitionAtlas_Controls_Shearexact-vacuum-atlasgeneral-relativitylean4mathlib
shear λ (T,R,α,β) = (T, R, α, β + λ sin α) and its inverse shearInv λ (β ↦ β − λ sin α); jacShear λ x = I + λ cos α E₃₂ (row 3 = output β, column 2 = input α) and the right inverse jacShearInv λ x = I − λ cos α E₃₂; ctlR λ, the expected Ricci components (R_22 = 1 + λ²c²s², R_23 = R_32 = λ c s², R_33 = s², all others 0; c = cos α, s = sin α); pt = (0, 1, π/4, 0). The map is not affine for λ ≠ 0 (∂_α J³_α = −λ sin α ≠ 0 on domEF); λ = 0 is the identity. The module docstring (kept in the bundle) states the two routes and the witness; the theorems themselves are separate nodes.
Definition code
-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Controls/Shear.lean
-- definition bundle: kept ExactVacuumAtlas.Controls.Shear.ctlR, ExactVacuumAtlas.Controls.Shear.jacShear, ExactVacuumAtlas.Controls.Shear.jacShearInv, ExactVacuumAtlas.Controls.Shear.pt, ExactVacuumAtlas.Controls.Shear.shear, ExactVacuumAtlas.Controls.Shear.shearInv
import Mathlib
import Definitions.Def_Atlas_Controls_CylinderTables
import Definitions.Def_Atlas_Controls_ShearTables
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Certificate
import Definitions.Def_Atlas_Core_Lift
import Definitions.Def_Atlas_Core_Relation
import Definitions.Def_Atlas_Schwarzschild_Defs
import Definitions.Def_Atlas_Schwarzschild_Domain
import Definitions.Def_Atlas_Transport_Connection
import Definitions.Def_Atlas_Transport_Curvature
import Definitions.Def_Atlas_Transport_MatrixCalc
set_option maxHeartbeats 4000000
/-!
# Non-vacuum, nonlinear control for the Ricci transformation law (ATLAS-II)
Old metric `h = −dt² + dr² + dθ² + sin²θ dφ²` (`Controls.Cylinder.gCyl 0`, first release; `R_θθ = 1`,
`R_φφ = sin²θ`, not vacuum). Coordinate change on `U = V = domEF = {R > 0, 0 < α < π}`:
`Φ(T, R, α, β) = (T, R, α, β + λ sin α)`, inverse `β ↦ β − λ sin α`, `J = I + λ cos α E₃₂`.
`Φ` is not affine for `λ ≠ 0` (`∂_α J³_α = −λ sin α`, nonzero on `domEF` where `sin α > 0`; `λ = 0` is the identity), so the Christoffel transformation carries a genuine
second-derivative term. The pulled-back metric `gCtl λ = Jᵀ h(Φ) J` has the angular block
`[[1 + λ²c²s², λ c s²], [λ c s², s²]]` and the mixed Ricci component `R₂₃ = R₃₂ = λ c s²`, **nonzero exactly when `λ ≠ 0` and `cos α ≠ 0`**.
Two independent routes to the same 16 values `ctlR λ`:
* `ricci_direct`: the generated tables `Atlas/Controls/ShearTables.lean` (pd, Christoffel with the
closed forms of `shear_spec.py`, pd Christoffel, Ricci), i.e. the registered `ricciOf` evaluated directly;
* `ricci_transport`: the general law `ricciOf_transform` applied to the first-release cylinder values.
Witness (`λ = 1`, `α = π/4`): `R₂₃ = √2/4 ≠ 0` (`mixed_witness`). Negative checks (wrong index placement,
missing Jacobian factor) live in `audit/atlas_ii/shear_negative.lean`, not here.
-/
open Real
open scoped ContDiff
open Matrix
open ExactVacuumAtlas ExactVacuumAtlas.Schwarzschild
namespace ExactVacuumAtlas.Controls.Shear
variable (lam : ℝ)
/-- The nonlinear shear `(T, R, α, β) ↦ (T, R, α, β + λ sin α)`. -/
noncomputable def shear (x : Pt 4) : Pt 4 := ![x 0, x 1, x 2, x 3 + lam * sin (x 2)]
/-- Its inverse `β ↦ β − λ sin α`. -/
noncomputable def shearInv (y : Pt 4) : Pt 4 := ![y 0, y 1, y 2, y 3 - lam * sin (y 2)]
/-- Jacobian `I + λ cos α E₃₂` (row 3 = output `β`, column 2 = input `α`). -/
noncomputable def jacShear (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ :=
!![1, 0, 0, 0; 0, 1, 0, 0; 0, 0, 1, 0; 0, 0, lam * cos (x 2), 1]
/-- Right inverse `I − λ cos α E₃₂`. -/
noncomputable def jacShearInv (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ :=
!![1, 0, 0, 0; 0, 1, 0, 0; 0, 0, 1, 0; 0, 0, -(lam * cos (x 2)), 1]
/-- The expected Ricci components of the control metric (`R₂₂ = g₂₂`, `R₂₃ = R₃₂ = g₂₃`, `R₃₃ = g₃₃`, rest `0`). -/
noncomputable def ctlR : Metric 4
| 2, 2 => fun x => 1 + lam ^ 2 * (cos (x 2) ^ 2 * sin (x 2) ^ 2)
| 2, 3 => fun x => lam * (cos (x 2) * sin (x 2) ^ 2)
| 3, 2 => fun x => lam * (cos (x 2) * sin (x 2) ^ 2)
| 3, 3 => fun x => sin (x 2) ^ 2
| _, _ => fun _ => 0
/-- Witness point `(0, 1, π/4, 0)`. -/
noncomputable def pt : Pt 4 := ![0, 1, π / 4, 0]
end ExactVacuumAtlas.Controls.Shear
Source
He Wang, Exact Vacuum Atlas II, local source snapshot (public Git repository not yet available), commit 11fb317259353b71a41d6daed466c495cffd7db4; Atlas/Controls/Shear.lean; SHA-256 219b8cea95eaf75ce7002541a89f6bcd6bdaeacb3ba69ac402eaacd84c242ddc. Mathematical background: See mission/PHYSICS_BOUNDARY.md §A-F for registered definitions and literature references (Wald, Müller-Grave arXiv:0904.4184, Visser arXiv:0706.0622, Martel-Poisson gr-qc/0001069).
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.