Atlas_Controls_ShearTables
DefinitionThe pulled-back control metric gCtl λ = Jᵀ h(Φ) J (h the cylinder metric, Φ the shear β ↦ β + λ sin α, J = I + λ cos α E₃₂) and its candidate inverse giCtl λ, in coordinates (T, R, α, β): g_00 = −1, g_11 = 1, g_22 = 1 + λ² cos²α sin²α, g_23 = g_32 = λ cos α sin²α, g_33 = sin²α, other entries 0; ĝ^00 = −1, ĝ^11 = 1, ĝ^22 = 1, ĝ^23 = ĝ^32 = −λ cos α, ĝ^33 = (1 + λ² cos²α sin²α)/sin²α, other entries 0 (angular block determinant sin²α). The time entry of the inverse is −1 (not +1). Generated by scripts/gen_rt_ricci.py from Atlas/Controls/shear_spec.py; the inverse is checked, not assumed (Shear.inv_pullback and the audit C3 giCtl·gCtl = 1).
中文导读。 剪切后的对照度规 gCtl λ 及候选逆 giCtl λ：角块 [[1 + λ²c²s², λcs²], [λcs², s²]]，逆角块 [[1, −λc], [−λc, (1 + λ²c²s²)/s²]]；时间分量 −1。
-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Controls/ShearTables.lean -- definition bundle: kept ExactVacuumAtlas.Controls.Shear.gCtl, ExactVacuumAtlas.Controls.Shear.giCtl import Mathlib import Definitions.Def_Atlas_Core_Basic import Definitions.Def_Atlas_Core_Lift import Definitions.Def_Atlas_Schwarzschild_Defs import Definitions.Def_Atlas_Schwarzschild_Domain set_option maxHeartbeats 4000000 set_option linter.unusedVariables false set_option linter.unusedSimpArgs false set_option linter.unusedTactic false set_option linter.unreachableTactic false /-! Generated by `scripts/gen_rt_ricci.py` from `Atlas/Controls/shear_spec.py`. Do not edit by hand. -/ open Real open ExactVacuumAtlas ExactVacuumAtlas.Schwarzschild namespace ExactVacuumAtlas.Controls.Shear variable (lam : ℝ) /-- The sheared control metric `Jᵀ h(Φ) J` with `J = I + λ cos α E₃₂`: angular block `[[1 + λ²c²s², λ c s²], [λ c s², s²]]`, `c = cos α`, `s = sin α`. -/ noncomputable def gCtl (lam : ℝ) : Metric 4 | 0, 0 => fun _ => -1 | 1, 1 => fun _ => 1 | 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 => 1 * sin (x 2) ^ 2 | _, _ => fun _ => 0 /-- Candidate inverse: angular block `[[1, −λ c], [−λ c, (1 + λ²c²s²)/s²]]` (block determinant `s²`). -/ noncomputable def giCtl (lam : ℝ) : Metric 4 | 0, 0 => fun _ => -1 | 1, 1 => fun _ => 1 | 2, 2 => fun _ => 1 | 2, 3 => fun x => -(lam * cos (x 2)) | 3, 2 => fun x => -(lam * cos (x 2)) | 3, 3 => fun x => (1 + lam ^ 2 * (cos (x 2) ^ 2 * sin (x 2) ^ 2)) / sin (x 2) ^ 2 | _, _ => fun _ => 0 end ExactVacuumAtlas.Controls.Shear
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.