Atlas_Controls_CylinderTables
Definitionexact-vacuum-atlasgeneral-relativitylean4mathlib
Two explicit metrics in coordinates (t, r, θ, φ), both with an unused real parameter M (generator interface): gCyl M = diag(−1, 1, 1, sin²θ) and the candidate inverse giCyl M = diag(−1, 1, 1, 1/sin²θ). This is the line element −dt² + dr² + dθ² + sin²θ dφ², the non-vacuum negative control of release I (R_θθ = 1, R_φφ = sin²θ, other components 0). The bundle keeps only the two definitions; the table theorems of the source module are separate nodes. Generated by scripts/gen_rt_ricci.py from Atlas/Schwarzschild/control_spec.py (untrusted generator; everything proved is kernel-checked).
中文导读。 圆柱型对照度规 −dt² + dr² + dθ² + sin²θ dφ²（非真空：R_θθ = 1、R_φφ = sin²θ）及其候选逆；参数 M 未使用。
Definition code
-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Controls/CylinderTables.lean -- definition bundle: kept ExactVacuumAtlas.Controls.Cylinder.gCyl, ExactVacuumAtlas.Controls.Cylinder.giCyl 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/Schwarzschild/control_spec.py`. Do not edit by hand. -/ open Real open ExactVacuumAtlas ExactVacuumAtlas.Schwarzschild namespace ExactVacuumAtlas.Controls.Cylinder variable (M : ℝ) /-- `-dt² + dr² + dθ² + sin²θ dφ²`; the parameter `M` is unused (generator interface). -/ noncomputable def gCyl (M : ℝ) : Metric 4 | 0, 0 => fun _ => -1 | 1, 1 => fun _ => 1 | 2, 2 => fun _ => 1 | 3, 3 => fun x => 1 * sin (x 2) ^ 2 | _, _ => fun _ => 0 noncomputable def giCyl (M : ℝ) : Metric 4 | 0, 0 => fun _ => -1 | 1, 1 => fun _ => 1 | 2, 2 => fun _ => 1 | 3, 3 => fun x => 1 / sin (x 2) ^ 2 | _, _ => fun _ => 0 end ExactVacuumAtlas.Controls.Cylinder
Source
He Wang, Exact Vacuum Atlas II, local source snapshot (public Git repository not yet available), commit 11fb317259353b71a41d6daed466c495cffd7db4; Atlas/Controls/CylinderTables.lean; SHA-256 6853c22124c397d8886c39820e0325b7348d66f0d0a916d41678b132205ebfee. 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.