Documentation Verification Report

Basic

📁 Source: PhysLean/Relativity/Tensors/RealTensor/Vector/Causality/Basic.lean

Statistics

Metric	Count
Definitions `CausalCharacter`, `causalCharacter`, `causalDiamond`, `causallyFollows`, `causallyPrecedes`, `causallyRelated`, `causallyUnrelated`, `futureLightConeBoundary`, `instDecidableEqCausalCharacter`, `interiorFutureLightCone`, `interiorPastLightCone`, `isFutureDirected`, `isPastDirected`, `lightConeBoundary`, `pastLightConeBoundary`	15
Theorems `causalCharacter_invariant`, `neg_causalCharacter_eq_self`, `self_mem_lightConeBoundary`, `spaceLike_iff_norm_sq_neg`	4
Total	19

Lorentz.Vector

Definitions

Name	Category	Theorems
`CausalCharacter` 📖	CompData	—
`causalCharacter` 📖	CompOp	7 math math: `timeLike_iff_time_lt_space`, `timeLike_iff_norm_sq_pos`, `lightLike_iff_norm_sq_zero`, `spaceLike_iff_norm_sq_neg`, `causalCharacter_invariant`, `causalCharacter_zero`, `neg_causalCharacter_eq_self`
`causalDiamond` 📖	CompOp	—
`causallyFollows` 📖	MathDef	3 math math: `SpecialRelativity.InstantaneousTwinParadox.endPoint_causallyFollows_startPoint`, `SpecialRelativity.InstantaneousTwinParadox.endPoint_causallyFollows_twinBMid`, `SpecialRelativity.InstantaneousTwinParadox.twinBMid_causallyFollows_startPoint`
`causallyPrecedes` 📖	MathDef	1 math math: `causallyPrecedes_refl`
`causallyRelated` 📖	MathDef	—
`causallyUnrelated` 📖	MathDef	—
`futureLightConeBoundary` 📖	CompOp	—
`instDecidableEqCausalCharacter` 📖	CompOp	—
`interiorFutureLightCone` 📖	CompOp	—
`interiorPastLightCone` 📖	CompOp	—
`isFutureDirected` 📖	MathDef	—
`isPastDirected` 📖	MathDef	—
`lightConeBoundary` 📖	CompOp	1 math math: `self_mem_lightConeBoundary`
`pastLightConeBoundary` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`causalCharacter_invariant` 📖	mathematical	—	`causalCharacter` `LorentzGroup` `Lorentz.Vector` `TensorSpecies.Tensorial.smulAction` `realLorentzTensor.Color` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `instAddCommMonoid` `instModuleReal` `tensorial`	—	`minkowskiProduct_invariant`
`neg_causalCharacter_eq_self` 📖	mathematical	—	`causalCharacter` `Lorentz.Vector` `instAddCommGroup`	—	`minkowskiProduct_toCoord`
`self_mem_lightConeBoundary` 📖	mathematical	—	`Lorentz.Vector` `lightConeBoundary`	—	—
`spaceLike_iff_norm_sq_neg` 📖	mathematical	—	`causalCharacter` `CausalCharacter.spaceLike` `Lorentz.Vector` `isNormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `instAddCommGroup` `minkowskiProduct`	—	—

---

← Back to Index