Formal verification, UTC 2026-10-23T20:53:39.034242+00:00
$ lean --version
Lean (version 4.36.0-rc1, x86_64-unknown-linux-gnu, commit c9afcddf514a6772bd4d649f7cfc04eff0b9f15e, Release)
Dependency mathlib: 3d14fd9a313ac35ed4b5c653ed5d99157c9e29f6
Dependency plausible: c2d7840c65673533e15b499f25beecdc6227f7d8
Dependency LeanSearchClient: 9d39f9bb0c30aa2f6200808805ff16e6ce950890
Dependency importGraph: 19a8e822bfeace1ae4e090045aad81e0c930e6cf
Dependency proofwidgets: eef6bb95363c38103535ac2df08b6bb141f0a764
Dependency aesop: 29c64c56cc38211d39b306db2df11701e3d3de11
Dependency Qq: 6d26f8bb4b2bb78f929ad160feac508866821316
Dependency batteries: 8e746d768c73b716c7d4bc07bd8e73f2a75bdb60
Dependency Cli: 34d2efffcb6dc8d5f3537cf6a7f88bfaa999ec49
Source SHA256 BlockUniverse.lean: c14ff522258a2b2d25428497befad610b00870f927791abf14ea805f1244a2cb
Source SHA256 BlockUniverse/HigherDim.lean: cb9dcf7bbb36e84c890ab40b8aab7a7ed7c6b8736487e11258cc3e985e05c323
Source SHA256 BlockUniverse/Stein.lean: 3cf4b9d3fa891e510f1a0313ef75930f24536d1daa7c2f8e38466ec5222e941d
Source SHA256 BlockUniverse/Reciprocal.lean: d00b013cf59fe6e2a6aa64557cadcda4bddac351f0caa4237cd248926802f987
Source SHA256 BlockUniverse/ReciprocalNoDilation.lean: 0b2a4ac39b865864e12ff537ec019a2a743cae388e7bc031dbc806e0daf0983b
Source SHA256 BlockUniverse/ReciprocalThreePlusOne.lean: 379c9f89f596c3d7dd1eb98fcf4d72c2736b37644a18fd960f6e6b981188397e
Source SHA256 AxiomAuditAll.lean: f846dcef6ea53c8a23de71f2a35ee56f91780d973c93db692ce3cbec43350dda
Source SHA256 DilationCountermodel.lean: ad7772959cddb265d949c536c2b9be4a5a96102cd4449fab15ef3000e1ca2afa
$ lake build
⚠ [3096/3108] Built BlockUniverse (1.9s)
warning: BlockUniverse.lean: imports `Mathlib.Tactic.Linarith` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse.lean: imports `Mathlib.Tactic.Ring` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse.lean: imports `Mathlib.Tactic.FieldSimp` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse.lean: imports `Mathlib.Tactic.Positivity` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse.lean: imports `Mathlib.Algebra.Order.Field.Basic` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
⚠ [3097/3108] Ran BlockUniverse:irArts
warning: BlockUniverse.lean: imports `Mathlib.Tactic.Linarith` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse.lean: imports `Mathlib.Tactic.Ring` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse.lean: imports `Mathlib.Tactic.FieldSimp` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse.lean: imports `Mathlib.Tactic.Positivity` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse.lean: imports `Mathlib.Algebra.Order.Field.Basic` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
⚠ [3098/3108] Built BlockUniverse.HigherDim (2.2s)
warning: BlockUniverse/HigherDim.lean: imports `Mathlib.Tactic.Linarith` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/HigherDim.lean: imports `Mathlib.Tactic.Ring` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/HigherDim.lean: imports `Mathlib.Tactic.FieldSimp` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/HigherDim.lean: imports `Mathlib.Tactic.Positivity` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/HigherDim.lean: imports `Mathlib.Algebra.Order.Field.Basic` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/HigherDim.lean: imports `Mathlib.Algebra.Order.BigOperators.Ring.Finset` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/HigherDim.lean: imports `Mathlib.Algebra.BigOperators.Fin` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
⚠ [3099/3108] Ran BlockUniverse.HigherDim:irArts
warning: BlockUniverse/HigherDim.lean: imports `Mathlib.Tactic.Linarith` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/HigherDim.lean: imports `Mathlib.Tactic.Ring` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/HigherDim.lean: imports `Mathlib.Tactic.FieldSimp` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/HigherDim.lean: imports `Mathlib.Tactic.Positivity` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/HigherDim.lean: imports `Mathlib.Algebra.Order.Field.Basic` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/HigherDim.lean: imports `Mathlib.Algebra.Order.BigOperators.Ring.Finset` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/HigherDim.lean: imports `Mathlib.Algebra.BigOperators.Fin` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
⚠ [3100/3108] Built BlockUniverse.Stein (4.6s)
warning: BlockUniverse/Stein.lean: imports `Mathlib.Tactic.Linarith` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/Stein.lean: imports `Mathlib.Tactic.Ring` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/Stein.lean: imports `Mathlib.Tactic.FieldSimp` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/Stein.lean: imports `Mathlib.Tactic.Positivity` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/Stein.lean: imports `Mathlib.Algebra.Order.Field.Basic` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/Stein.lean:326:68: This simp argument is unused:
  false_or

Hint: Omit it from the simp argument list.
  [apply] simp only [hA, hB, hC, hD, hE, and_true, and_false, or_false] at hk

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: BlockUniverse/Stein.lean:351:37: This simp argument is unused:
  and_true

Hint: Omit it from the simp argument list.
  [apply] simp only [hA, hB, hC, hD, hE, and_false, or_false, false_or] at hk

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: BlockUniverse/Stein.lean:351:68: This simp argument is unused:
  false_or

Hint: Omit it from the simp argument list.
  [apply] simp only [hA, hB, hC, hD, hE, and_true, and_false, or_false] at hk

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: BlockUniverse/Stein.lean:408:0: automatically included section variable(s) unused in theorem `BlockUniverse.Stein.U_translate`:
  [LinearOrder K]
  [IsStrictOrderedRing K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [LinearOrder K] [IsStrictOrderedRing K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: BlockUniverse/Stein.lean:410:0: automatically included section variable(s) unused in theorem `BlockUniverse.Stein.W_translate`:
  [LinearOrder K]
  [IsStrictOrderedRing K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [LinearOrder K] [IsStrictOrderedRing K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: BlockUniverse/Stein.lean:418:0: automatically included section variable(s) unused in theorem `BlockUniverse.Stein.U_dilate`:
  [LinearOrder K]
  [IsStrictOrderedRing K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [LinearOrder K] [IsStrictOrderedRing K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: BlockUniverse/Stein.lean:420:0: automatically included section variable(s) unused in theorem `BlockUniverse.Stein.W_dilate`:
  [LinearOrder K]
  [IsStrictOrderedRing K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [LinearOrder K] [IsStrictOrderedRing K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: BlockUniverse/Stein.lean:422:0: automatically included section variable(s) unused in theorem `BlockUniverse.Stein.U_reflect`:
  [LinearOrder K]
  [IsStrictOrderedRing K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [LinearOrder K] [IsStrictOrderedRing K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: BlockUniverse/Stein.lean:424:0: automatically included section variable(s) unused in theorem `BlockUniverse.Stein.W_reflect`:
  [LinearOrder K]
  [IsStrictOrderedRing K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [LinearOrder K] [IsStrictOrderedRing K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
⚠ [3101/3108] Ran BlockUniverse.Stein:irArts
warning: BlockUniverse/Stein.lean: imports `Mathlib.Tactic.Linarith` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/Stein.lean: imports `Mathlib.Tactic.Ring` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/Stein.lean: imports `Mathlib.Tactic.FieldSimp` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/Stein.lean: imports `Mathlib.Tactic.Positivity` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/Stein.lean: imports `Mathlib.Algebra.Order.Field.Basic` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
⚠ [3102/3108] Built BlockUniverse.Reciprocal (1.6s)
warning: BlockUniverse/Reciprocal.lean:27:0: automatically included section variable(s) unused in theorem `BlockUniverse.Reciprocal.U_swap`:
  [LinearOrder K]
  [IsStrictOrderedRing K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [LinearOrder K] [IsStrictOrderedRing K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: BlockUniverse/Reciprocal.lean:28:0: automatically included section variable(s) unused in theorem `BlockUniverse.Reciprocal.W_swap`:
  [LinearOrder K]
  [IsStrictOrderedRing K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [LinearOrder K] [IsStrictOrderedRing K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: BlockUniverse/Reciprocal.lean:56:14: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: BlockUniverse/Reciprocal.lean:56:14: Unused tactic linter: `(exfalso; linarith [h1.1, h2.1])` is never executed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: BlockUniverse/Reciprocal.lean:71:6: Unused tactic linter: `skip` does not change the goal.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
⚠ [3104/3108] Built BlockUniverse.ReciprocalNoDilation (2.1s)
warning: BlockUniverse/ReciprocalNoDilation.lean: imports `Mathlib.Analysis.Real.Sqrt` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
info: BlockUniverse/ReciprocalNoDilation.lean:149:0: 'BlockUniverse.ReciprocalNoDilation.one_reciprocal_pair_forces_universal' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [3105/3108] Ran BlockUniverse.ReciprocalNoDilation:irArts
warning: BlockUniverse/ReciprocalNoDilation.lean: imports `Mathlib.Analysis.Real.Sqrt` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
⚠ [3106/3108] Built BlockUniverse.ReciprocalThreePlusOne (1.9s)
warning: BlockUniverse/ReciprocalThreePlusOne.lean: imports `Mathlib.Tactic.FinCases` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: BlockUniverse/ReciprocalThreePlusOne.lean:86:44: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: BlockUniverse/ReciprocalThreePlusOne.lean:86:40: Unused tactic linter: `<;>` can be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: BlockUniverse/ReciprocalThreePlusOne.lean:86:44: Unused tactic linter: `ring` is never executed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: BlockUniverse/ReciprocalThreePlusOne.lean:101:59: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: BlockUniverse/ReciprocalThreePlusOne.lean:101:55: Unused tactic linter: `<;>` can be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: BlockUniverse/ReciprocalThreePlusOne.lean:101:59: Unused tactic linter: `ring` is never executed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: BlockUniverse/ReciprocalThreePlusOne.lean:153:0: 'BlockUniverse.ReciprocalThreePlusOne.one_reciprocal_pair_forces_universal' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [3107/3108] Ran BlockUniverse.ReciprocalThreePlusOne:irArts
warning: BlockUniverse/ReciprocalThreePlusOne.lean: imports `Mathlib.Tactic.FinCases` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
Build completed successfully (3108 jobs).
$ lake env lean AxiomAuditAll.lean
BlockUniverse.spacelike_simulSomeFrame.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] {p q : BlockUniverse.Event.{u_1} K} (h : BlockUniverse.Spacelike.{u_1} p q) :
  BlockUniverse.SimulSomeFrame.{u_1} p q
'BlockUniverse.spacelike_simulSomeFrame' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.simulSomeFrame_spacelike_or_eq.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] {p q : BlockUniverse.Event.{u_1} K} (h : BlockUniverse.SimulSomeFrame.{u_1} p q) :
  BlockUniverse.Spacelike.{u_1} p q ∨ Eq.{u_1 + 1} p q
'BlockUniverse.simulSomeFrame_spacelike_or_eq' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.simultaneous_iff_spacelike_or_eq.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] (p q : BlockUniverse.Event.{u_1} K) :
  BlockUniverse.SimulSomeFrame.{u_1} p q ↔ BlockUniverse.Spacelike.{u_1} p q ∨ Eq.{u_1 + 1} p q
'BlockUniverse.simultaneous_iff_spacelike_or_eq' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.common_simultaneity_partner.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] (p q : BlockUniverse.Event.{u_1} K) :
  ∃ r, BlockUniverse.SimulSomeFrame.{u_1} p r ∧ BlockUniverse.SimulSomeFrame.{u_1} r q
'BlockUniverse.common_simultaneity_partner' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.rietdijk_putnam.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K]
  (R : BlockUniverse.Event.{u_1} K → BlockUniverse.Event.{u_1} K → Prop)
  (H1 : ∀ (p q : BlockUniverse.Event.{u_1} K), BlockUniverse.SimulSomeFrame.{u_1} p q → R p q)
  (H2 : ∀ (p q r : BlockUniverse.Event.{u_1} K), R p q → R q r → R p r) (p q : BlockUniverse.Event.{u_1} K) : R p q
'BlockUniverse.rietdijk_putnam' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.rietdijk_putnam_spacelike.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] (R : BlockUniverse.Event.{u_1} K → BlockUniverse.Event.{u_1} K → Prop)
  (Hrefl : ∀ (p : BlockUniverse.Event.{u_1} K), R p p)
  (H1 : ∀ (p q : BlockUniverse.Event.{u_1} K), BlockUniverse.Spacelike.{u_1} p q → R p q)
  (H2 : ∀ (p q r : BlockUniverse.Event.{u_1} K), R p q → R q r → R p r) (p q : BlockUniverse.Event.{u_1} K) : R p q
'BlockUniverse.rietdijk_putnam_spacelike' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.hypotheses_consistent.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K] :
  ∃ R,
    (∀ (p q : BlockUniverse.Event.{u_1} K), BlockUniverse.SimulSomeFrame.{u_1} p q → R p q) ∧
      ∀ (p q r : BlockUniverse.Event.{u_1} K), R p q → R q r → R p r
'BlockUniverse.hypotheses_consistent' depends on axioms: [propext, Quot.sound.{u}]
BlockUniverse.transitivity_needed.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] :
  ∃ R,
    (∀ (p q : BlockUniverse.Event.{u_1} K), BlockUniverse.SimulSomeFrame.{u_1} p q → R p q) ∧
      ¬∀ (p q : BlockUniverse.Event.{u_1} K), R p q
'BlockUniverse.transitivity_needed' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.relativity_of_reality_needed.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] :
  (∀ (p : BlockUniverse.Event.{u_1} K), BlockUniverse.CausalPast.{u_1} p p) ∧
    (∀ (p q r : BlockUniverse.Event.{u_1} K),
        BlockUniverse.CausalPast.{u_1} p q → BlockUniverse.CausalPast.{u_1} q r → BlockUniverse.CausalPast.{u_1} p r) ∧
      (¬∀ (p q : BlockUniverse.Event.{u_1} K), BlockUniverse.CausalPast.{u_1} p q) ∧
        ¬∀ (p q : BlockUniverse.Event.{u_1} K),
            BlockUniverse.SimulSomeFrame.{u_1} p q → BlockUniverse.CausalPast.{u_1} p q
'BlockUniverse.relativity_of_reality_needed' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.HigherDim.normSq_nonneg.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] {n : ℕ} (a : Fin (HAdd.hAdd.{0, 0, 0} n 1) → K) :
  LE.le.{u_1} 0 (BlockUniverse.HigherDim.normSq.{u_1} a)
'BlockUniverse.HigherDim.normSq_nonneg' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.HigherDim.normSq_zero_iff.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] {n : ℕ} (a : Fin (HAdd.hAdd.{0, 0, 0} n 1) → K) :
  Eq.{u_1 + 1} (BlockUniverse.HigherDim.normSq.{u_1} a) 0 ↔ ∀ (i : Fin (HAdd.hAdd.{0, 0, 0} n 1)), Eq.{u_1 + 1} (a i) 0
'BlockUniverse.HigherDim.normSq_zero_iff' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.HigherDim.spacelike_simulSomeFrame.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] {n : ℕ} {p q : BlockUniverse.HigherDim.Event.{u_1} n K}
  (h : BlockUniverse.HigherDim.Spacelike.{u_1} p q) : BlockUniverse.HigherDim.SimulSomeFrame.{u_1} p q
'BlockUniverse.HigherDim.spacelike_simulSomeFrame' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.HigherDim.simulSomeFrame_spacelike_or_eq.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] {n : ℕ} {p q : BlockUniverse.HigherDim.Event.{u_1} n K}
  (h : BlockUniverse.HigherDim.SimulSomeFrame.{u_1} p q) :
  BlockUniverse.HigherDim.Spacelike.{u_1} p q ∨ Eq.{u_1 + 1} p q
'BlockUniverse.HigherDim.simulSomeFrame_spacelike_or_eq' depends on axioms: [propext,
 Classical.choice.{u},
 Quot.sound.{u}]
BlockUniverse.HigherDim.simultaneous_iff_spacelike_or_eq.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] {n : ℕ} (p q : BlockUniverse.HigherDim.Event.{u_1} n K) :
  BlockUniverse.HigherDim.SimulSomeFrame.{u_1} p q ↔ BlockUniverse.HigherDim.Spacelike.{u_1} p q ∨ Eq.{u_1 + 1} p q
'BlockUniverse.HigherDim.simultaneous_iff_spacelike_or_eq' depends on axioms: [propext,
 Classical.choice.{u},
 Quot.sound.{u}]
BlockUniverse.HigherDim.dot_axisVel.{u_1} {K : Type u_1} [Field.{u_1} K] {n : ℕ} (c : K)
  (a : Fin (HAdd.hAdd.{0, 0, 0} n 1) → K) :
  Eq.{u_1 + 1} (BlockUniverse.HigherDim.dot.{u_1} (BlockUniverse.HigherDim.axisVel.{u_1} c) a)
    (HMul.hMul.{u_1, u_1, u_1} c (a 0))
'BlockUniverse.HigherDim.dot_axisVel' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.HigherDim.normSq_axisVel.{u_1} {K : Type u_1} [Field.{u_1} K] {n : ℕ} (c : K) :
  Eq.{u_1 + 1} (BlockUniverse.HigherDim.normSq.{u_1} (BlockUniverse.HigherDim.axisVel.{u_1} c))
    (HPow.hPow.{u_1, 0, u_1} c 2)
'BlockUniverse.HigherDim.normSq_axisVel' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.HigherDim.common_simultaneity_partner.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] {n : ℕ} (p q : BlockUniverse.HigherDim.Event.{u_1} n K) :
  ∃ r, BlockUniverse.HigherDim.SimulSomeFrame.{u_1} p r ∧ BlockUniverse.HigherDim.SimulSomeFrame.{u_1} r q
'BlockUniverse.HigherDim.common_simultaneity_partner' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.HigherDim.rietdijk_putnam.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] {n : ℕ}
  (R : BlockUniverse.HigherDim.Event.{u_1} n K → BlockUniverse.HigherDim.Event.{u_1} n K → Prop)
  (H1 : ∀ (p q : BlockUniverse.HigherDim.Event.{u_1} n K), BlockUniverse.HigherDim.SimulSomeFrame.{u_1} p q → R p q)
  (H2 : ∀ (p q r : BlockUniverse.HigherDim.Event.{u_1} n K), R p q → R q r → R p r)
  (p q : BlockUniverse.HigherDim.Event.{u_1} n K) : R p q
'BlockUniverse.HigherDim.rietdijk_putnam' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.HigherDim.rietdijk_putnam_spacelike.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] {n : ℕ}
  (R : BlockUniverse.HigherDim.Event.{u_1} n K → BlockUniverse.HigherDim.Event.{u_1} n K → Prop)
  (Hrefl : ∀ (p : BlockUniverse.HigherDim.Event.{u_1} n K), R p p)
  (H1 : ∀ (p q : BlockUniverse.HigherDim.Event.{u_1} n K), BlockUniverse.HigherDim.Spacelike.{u_1} p q → R p q)
  (H2 : ∀ (p q r : BlockUniverse.HigherDim.Event.{u_1} n K), R p q → R q r → R p r)
  (p q : BlockUniverse.HigherDim.Event.{u_1} n K) : R p q
'BlockUniverse.HigherDim.rietdijk_putnam_spacelike' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.HigherDim.transitivity_needed.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] {n : ℕ} :
  ∃ R,
    (∀ (p q : BlockUniverse.HigherDim.Event.{u_1} n K), BlockUniverse.HigherDim.SimulSomeFrame.{u_1} p q → R p q) ∧
      ¬∀ (p q : BlockUniverse.HigherDim.Event.{u_1} n K), R p q
'BlockUniverse.HigherDim.transitivity_needed' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.HigherDim.relativity_of_reality_needed.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] {n : ℕ} :
  (∀ (p : BlockUniverse.HigherDim.Event.{u_1} n K), BlockUniverse.HigherDim.CausalPast.{u_1} p p) ∧
    (∀ (p q r : BlockUniverse.HigherDim.Event.{u_1} n K),
        BlockUniverse.HigherDim.CausalPast.{u_1} p q →
          BlockUniverse.HigherDim.CausalPast.{u_1} q r → BlockUniverse.HigherDim.CausalPast.{u_1} p r) ∧
      (¬∀ (p q : BlockUniverse.HigherDim.Event.{u_1} n K), BlockUniverse.HigherDim.CausalPast.{u_1} p q) ∧
        ¬∀ (p q : BlockUniverse.HigherDim.Event.{u_1} n K),
            BlockUniverse.HigherDim.SimulSomeFrame.{u_1} p q → BlockUniverse.HigherDim.CausalPast.{u_1} p q
'BlockUniverse.HigherDim.relativity_of_reality_needed' depends on axioms: [propext,
 Classical.choice.{u},
 Quot.sound.{u}]
BlockUniverse.Stein.identity_iff_eq.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] (p q : BlockUniverse.Event.{u_1} K) :
  BlockUniverse.Stein.Identity.{u_1} p q ↔ Eq.{u_1 + 1} p q
'BlockUniverse.Stein.identity_iff_eq' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.Stein.causalPast'_iff.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] (p q : BlockUniverse.Event.{u_1} K) :
  BlockUniverse.Stein.CausalPast'.{u_1} p q ↔ BlockUniverse.CausalPast.{u_1} p q
'BlockUniverse.Stein.causalPast'_iff' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.Stein.R_iff_origin.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] (R : BlockUniverse.Event.{u_1} K → BlockUniverse.Event.{u_1} K → Prop)
  (hI : BlockUniverse.Stein.Invariant.{u_1} R) (p q : BlockUniverse.Event.{u_1} K) :
  R p q ↔
    R BlockUniverse.Stein.O.{u_1}
      (BlockUniverse.Stein.mk.{u_1} (BlockUniverse.Stein.U.{u_1} p q) (BlockUniverse.Stein.W.{u_1} p q))
'BlockUniverse.Stein.R_iff_origin' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.Stein.scale.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K]
  (R : BlockUniverse.Event.{u_1} K → BlockUniverse.Event.{u_1} K → Prop) (hI : BlockUniverse.Stein.Invariant.{u_1} R)
  (hsqrt : ∀ (y : K), LT.lt.{u_1} 0 y → ∃ s, LT.lt.{u_1} 0 s ∧ Eq.{u_1 + 1} (HMul.hMul.{u_1, u_1, u_1} s s) y) {a b : K}
  (ha : LT.lt.{u_1} 0 a) (hb : LT.lt.{u_1} 0 b) (u w : K) :
  R BlockUniverse.Stein.O.{u_1} (BlockUniverse.Stein.mk.{u_1} u w) →
    R BlockUniverse.Stein.O.{u_1}
      (BlockUniverse.Stein.mk.{u_1} (HMul.hMul.{u_1, u_1, u_1} a u) (HMul.hMul.{u_1, u_1, u_1} b w))
'BlockUniverse.Stein.scale' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.Stein.swap_uw.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K]
  (R : BlockUniverse.Event.{u_1} K → BlockUniverse.Event.{u_1} K → Prop) (hI : BlockUniverse.Stein.Invariant.{u_1} R)
  (u w : K) :
  R BlockUniverse.Stein.O.{u_1} (BlockUniverse.Stein.mk.{u_1} u w) →
    R BlockUniverse.Stein.O.{u_1} (BlockUniverse.Stein.mk.{u_1} w u)
'BlockUniverse.Stein.swap_uw' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.Stein.add_uw.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K]
  (R : BlockUniverse.Event.{u_1} K → BlockUniverse.Event.{u_1} K → Prop) (hI : BlockUniverse.Stein.Invariant.{u_1} R)
  (htrans : ∀ (p q r : BlockUniverse.Event.{u_1} K), R p q → R q r → R p r) (u w u' w' : K) :
  R BlockUniverse.Stein.O.{u_1} (BlockUniverse.Stein.mk.{u_1} u w) →
    R BlockUniverse.Stein.O.{u_1} (BlockUniverse.Stein.mk.{u_1} u' w') →
      R BlockUniverse.Stein.O.{u_1}
        (BlockUniverse.Stein.mk.{u_1} (HAdd.hAdd.{u_1, u_1, u_1} u u') (HAdd.hAdd.{u_1, u_1, u_1} w w'))
'BlockUniverse.Stein.add_uw' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.Stein.same_sign_ratio.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] {x y : K} (h1 : LT.lt.{u_1} 0 x ↔ LT.lt.{u_1} 0 y)
  (h2 : LT.lt.{u_1} x 0 ↔ LT.lt.{u_1} y 0) : ∃ a, LT.lt.{u_1} 0 a ∧ Eq.{u_1 + 1} (HMul.hMul.{u_1, u_1, u_1} a x) y
'BlockUniverse.Stein.same_sign_ratio' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.Stein.stein_classification.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K]
  (hsqrt : ∀ (y : K), LT.lt.{u_1} 0 y → ∃ s, LT.lt.{u_1} 0 s ∧ Eq.{u_1 + 1} (HMul.hMul.{u_1, u_1, u_1} s s) y)
  (R : BlockUniverse.Event.{u_1} K → BlockUniverse.Event.{u_1} K → Prop) (hI : BlockUniverse.Stein.Invariant.{u_1} R)
  (hrefl : ∀ (p : BlockUniverse.Event.{u_1} K), R p p)
  (htrans : ∀ (p q r : BlockUniverse.Event.{u_1} K), R p q → R q r → R p r) :
  (∀ (p q : BlockUniverse.Event.{u_1} K), R p q ↔ BlockUniverse.Stein.Identity.{u_1} p q) ∨
    (∀ (p q : BlockUniverse.Event.{u_1} K), R p q ↔ BlockUniverse.Stein.ChronPast.{u_1} p q) ∨
      (∀ (p q : BlockUniverse.Event.{u_1} K), R p q ↔ BlockUniverse.Stein.CausalPast'.{u_1} p q) ∨
        (∀ (p q : BlockUniverse.Event.{u_1} K), R p q ↔ BlockUniverse.Stein.ChronFuture.{u_1} p q) ∨
          (∀ (p q : BlockUniverse.Event.{u_1} K), R p q ↔ BlockUniverse.Stein.CausalFuture.{u_1} p q) ∨
            ∀ (p q : BlockUniverse.Event.{u_1} K), R p q ↔ BlockUniverse.Stein.Universal.{u_1} p q
'BlockUniverse.Stein.stein_classification' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.Stein.spacelike_forces_block.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K]
  (hsqrt : ∀ (y : K), LT.lt.{u_1} 0 y → ∃ s, LT.lt.{u_1} 0 s ∧ Eq.{u_1 + 1} (HMul.hMul.{u_1, u_1, u_1} s s) y)
  (R : BlockUniverse.Event.{u_1} K → BlockUniverse.Event.{u_1} K → Prop) (hI : BlockUniverse.Stein.Invariant.{u_1} R)
  (hrefl : ∀ (p : BlockUniverse.Event.{u_1} K), R p p)
  (htrans : ∀ (p q r : BlockUniverse.Event.{u_1} K), R p q → R q r → R p r) (p₀ q₀ : BlockUniverse.Event.{u_1} K)
  (hsp : BlockUniverse.Spacelike.{u_1} p₀ q₀) (h : R p₀ q₀) (p q : BlockUniverse.Event.{u_1} K) : R p q
'BlockUniverse.Stein.spacelike_forces_block' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.Stein.stein_uniqueness.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K]
  (hsqrt : ∀ (y : K), LT.lt.{u_1} 0 y → ∃ s, LT.lt.{u_1} 0 s ∧ Eq.{u_1 + 1} (HMul.hMul.{u_1, u_1, u_1} s s) y)
  (R : BlockUniverse.Event.{u_1} K → BlockUniverse.Event.{u_1} K → Prop) (hI : BlockUniverse.Stein.Invariant.{u_1} R)
  (htrans : ∀ (p q r : BlockUniverse.Event.{u_1} K), R p q → R q r → R p r)
  (hpast : ∀ (p q : BlockUniverse.Event.{u_1} K), BlockUniverse.CausalPast.{u_1} p q → R p q)
  (hnot : ¬∀ (p q : BlockUniverse.Event.{u_1} K), R p q) (p q : BlockUniverse.Event.{u_1} K) :
  R p q ↔ BlockUniverse.CausalPast.{u_1} p q
'BlockUniverse.Stein.stein_uniqueness' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.Stein.U_translate.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K]
  (a p q : BlockUniverse.Event.{u_1} K) :
  Eq.{u_1 + 1}
    (BlockUniverse.Stein.U.{u_1} (BlockUniverse.Stein.translate.{u_1} a p) (BlockUniverse.Stein.translate.{u_1} a q))
    (BlockUniverse.Stein.U.{u_1} p q)
'BlockUniverse.Stein.U_translate' depends on axioms: [propext, Quot.sound.{u}]
BlockUniverse.Stein.W_translate.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K]
  (a p q : BlockUniverse.Event.{u_1} K) :
  Eq.{u_1 + 1}
    (BlockUniverse.Stein.W.{u_1} (BlockUniverse.Stein.translate.{u_1} a p) (BlockUniverse.Stein.translate.{u_1} a q))
    (BlockUniverse.Stein.W.{u_1} p q)
'BlockUniverse.Stein.W_translate' depends on axioms: [propext, Quot.sound.{u}]
BlockUniverse.Stein.U_boost.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K]
  {l : K} (hl : LT.lt.{u_1} 0 l) (p q : BlockUniverse.Event.{u_1} K) :
  Eq.{u_1 + 1} (BlockUniverse.Stein.U.{u_1} (BlockUniverse.Stein.boost.{u_1} l p) (BlockUniverse.Stein.boost.{u_1} l q))
    (HMul.hMul.{u_1, u_1, u_1} l (BlockUniverse.Stein.U.{u_1} p q))
'BlockUniverse.Stein.U_boost' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.Stein.W_boost.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K]
  {l : K} (hl : LT.lt.{u_1} 0 l) (p q : BlockUniverse.Event.{u_1} K) :
  Eq.{u_1 + 1} (BlockUniverse.Stein.W.{u_1} (BlockUniverse.Stein.boost.{u_1} l p) (BlockUniverse.Stein.boost.{u_1} l q))
    (HDiv.hDiv.{u_1, u_1, u_1} (BlockUniverse.Stein.W.{u_1} p q) l)
'BlockUniverse.Stein.W_boost' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.Stein.U_dilate.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K]
  (c : K) (p q : BlockUniverse.Event.{u_1} K) :
  Eq.{u_1 + 1}
    (BlockUniverse.Stein.U.{u_1} (BlockUniverse.Stein.dilate.{u_1} c p) (BlockUniverse.Stein.dilate.{u_1} c q))
    (HMul.hMul.{u_1, u_1, u_1} c (BlockUniverse.Stein.U.{u_1} p q))
'BlockUniverse.Stein.U_dilate' depends on axioms: [propext, Quot.sound.{u}]
BlockUniverse.Stein.W_dilate.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K]
  (c : K) (p q : BlockUniverse.Event.{u_1} K) :
  Eq.{u_1 + 1}
    (BlockUniverse.Stein.W.{u_1} (BlockUniverse.Stein.dilate.{u_1} c p) (BlockUniverse.Stein.dilate.{u_1} c q))
    (HMul.hMul.{u_1, u_1, u_1} c (BlockUniverse.Stein.W.{u_1} p q))
'BlockUniverse.Stein.W_dilate' depends on axioms: [propext, Quot.sound.{u}]
BlockUniverse.Stein.U_reflect.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K]
  (p q : BlockUniverse.Event.{u_1} K) :
  Eq.{u_1 + 1} (BlockUniverse.Stein.U.{u_1} (BlockUniverse.Stein.reflect.{u_1} p) (BlockUniverse.Stein.reflect.{u_1} q))
    (BlockUniverse.Stein.W.{u_1} p q)
'BlockUniverse.Stein.U_reflect' depends on axioms: [propext, Quot.sound.{u}]
BlockUniverse.Stein.W_reflect.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K]
  (p q : BlockUniverse.Event.{u_1} K) :
  Eq.{u_1 + 1} (BlockUniverse.Stein.W.{u_1} (BlockUniverse.Stein.reflect.{u_1} p) (BlockUniverse.Stein.reflect.{u_1} q))
    (BlockUniverse.Stein.U.{u_1} p q)
'BlockUniverse.Stein.W_reflect' depends on axioms: [propext, Quot.sound.{u}]
BlockUniverse.Stein.causalPast_satisfies_hypotheses.{u_1} {K : Type u_1} [Field.{u_1} K] [LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] :
  BlockUniverse.Stein.Invariant.{u_1} BlockUniverse.Stein.CausalPast'.{u_1} ∧
    (∀ (p : BlockUniverse.Event.{u_1} K), BlockUniverse.Stein.CausalPast'.{u_1} p p) ∧
      ∀ (p q r : BlockUniverse.Event.{u_1} K),
        BlockUniverse.Stein.CausalPast'.{u_1} p q →
          BlockUniverse.Stein.CausalPast'.{u_1} q r → BlockUniverse.Stein.CausalPast'.{u_1} p r
'BlockUniverse.Stein.causalPast_satisfies_hypotheses' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
@BlockUniverse.Reciprocal.U_swap.{u_1} : ∀ {K : Type u_1} [inst : Field.{u_1} K] [inst_1 : LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] (p q : BlockUniverse.Event.{u_1} K),
  Eq.{u_1 + 1} (BlockUniverse.Stein.U.{u_1} q p) (Neg.neg.{u_1} (BlockUniverse.Stein.U.{u_1} p q))
'BlockUniverse.Reciprocal.U_swap' depends on axioms: [propext, Quot.sound.{u}]
@BlockUniverse.Reciprocal.W_swap.{u_1} : ∀ {K : Type u_1} [inst : Field.{u_1} K] [inst_1 : LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] (p q : BlockUniverse.Event.{u_1} K),
  Eq.{u_1 + 1} (BlockUniverse.Stein.W.{u_1} q p) (Neg.neg.{u_1} (BlockUniverse.Stein.W.{u_1} p q))
'BlockUniverse.Reciprocal.W_swap' depends on axioms: [propext, Quot.sound.{u}]
@BlockUniverse.Reciprocal.ne_UW.{u_1} : ∀ {K : Type u_1} [inst : Field.{u_1} K] [inst_1 : LinearOrder.{u_1} K]
  [IsStrictOrderedRing.{u_1} K] {p q : BlockUniverse.Event.{u_1} K},
  Ne.{u_1 + 1} p q → Ne.{u_1 + 1} (BlockUniverse.Stein.U.{u_1} p q) 0 ∨ Ne.{u_1 + 1} (BlockUniverse.Stein.W.{u_1} p q) 0
'BlockUniverse.Reciprocal.ne_UW' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
@BlockUniverse.Reciprocal.mutual_core_trivial.{u_1} : ∀ {K : Type u_1} [inst : Field.{u_1} K]
  [inst_1 : LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K] (p q : BlockUniverse.Event.{u_1} K),
  (BlockUniverse.Stein.ChronPast.{u_1} p q ∧ BlockUniverse.Stein.ChronPast.{u_1} q p → Eq.{u_1 + 1} p q) ∧
    (BlockUniverse.Stein.CausalPast'.{u_1} p q ∧ BlockUniverse.Stein.CausalPast'.{u_1} q p → Eq.{u_1 + 1} p q) ∧
      (BlockUniverse.Stein.ChronFuture.{u_1} p q ∧ BlockUniverse.Stein.ChronFuture.{u_1} q p → Eq.{u_1 + 1} p q) ∧
        (BlockUniverse.Stein.CausalFuture.{u_1} p q ∧ BlockUniverse.Stein.CausalFuture.{u_1} q p → Eq.{u_1 + 1} p q)
'BlockUniverse.Reciprocal.mutual_core_trivial' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
@BlockUniverse.Reciprocal.symmetric_classification.{u_1} : ∀ {K : Type u_1} [inst : Field.{u_1} K]
  [inst_1 : LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K],
  (∀ (y : K), LT.lt.{u_1} 0 y → ∃ s, LT.lt.{u_1} 0 s ∧ Eq.{u_1 + 1} (HMul.hMul.{u_1, u_1, u_1} s s) y) →
    ∀ (R : BlockUniverse.Event.{u_1} K → BlockUniverse.Event.{u_1} K → Prop),
      BlockUniverse.Stein.Invariant.{u_1} R →
        (∀ (p : BlockUniverse.Event.{u_1} K), R p p) →
          (∀ (p q r : BlockUniverse.Event.{u_1} K), R p q → R q r → R p r) →
            (∀ (p q : BlockUniverse.Event.{u_1} K), R p q → R q p) →
              (∀ (p q : BlockUniverse.Event.{u_1} K), R p q ↔ Eq.{u_1 + 1} p q) ∨
                ∀ (p q : BlockUniverse.Event.{u_1} K), R p q
'BlockUniverse.Reciprocal.symmetric_classification' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
@BlockUniverse.Reciprocal.reciprocal_forces_block.{u_1} : ∀ {K : Type u_1} [inst : Field.{u_1} K]
  [inst_1 : LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K],
  (∀ (y : K), LT.lt.{u_1} 0 y → ∃ s, LT.lt.{u_1} 0 s ∧ Eq.{u_1 + 1} (HMul.hMul.{u_1, u_1, u_1} s s) y) →
    ∀ (R : BlockUniverse.Event.{u_1} K → BlockUniverse.Event.{u_1} K → Prop),
      BlockUniverse.Stein.Invariant.{u_1} R →
        (∀ (p : BlockUniverse.Event.{u_1} K), R p p) →
          (∀ (p q r : BlockUniverse.Event.{u_1} K), R p q → R q r → R p r) →
            (∀ (p q : BlockUniverse.Event.{u_1} K), R p q → R q p) →
              ∀ (p₀ q₀ : BlockUniverse.Event.{u_1} K),
                Ne.{u_1 + 1} p₀ q₀ → R p₀ q₀ → ∀ (p q : BlockUniverse.Event.{u_1} K), R p q
'BlockUniverse.Reciprocal.reciprocal_forces_block' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
@BlockUniverse.Reciprocal.one_reciprocal_pair_forces_block.{u_1} : ∀ {K : Type u_1} [inst : Field.{u_1} K]
  [inst_1 : LinearOrder.{u_1} K] [IsStrictOrderedRing.{u_1} K],
  (∀ (y : K), LT.lt.{u_1} 0 y → ∃ s, LT.lt.{u_1} 0 s ∧ Eq.{u_1 + 1} (HMul.hMul.{u_1, u_1, u_1} s s) y) →
    ∀ (R : BlockUniverse.Event.{u_1} K → BlockUniverse.Event.{u_1} K → Prop),
      BlockUniverse.Stein.Invariant.{u_1} R →
        (∀ (p : BlockUniverse.Event.{u_1} K), R p p) →
          (∀ (p q r : BlockUniverse.Event.{u_1} K), R p q → R q r → R p r) →
            ∀ (p₀ q₀ : BlockUniverse.Event.{u_1} K),
              Ne.{u_1 + 1} p₀ q₀ → R p₀ q₀ → R q₀ p₀ → ∀ (p q : BlockUniverse.Event.{u_1} K), R p q
'BlockUniverse.Reciprocal.one_reciprocal_pair_forces_block' depends on axioms: [propext,
 Classical.choice.{u},
 Quot.sound.{u}]
@BlockUniverse.ReciprocalNoDilation.mutual_add : ∀ {R : BlockUniverse.Event.{0} ℝ → BlockUniverse.Event.{0} ℝ → Prop},
  BlockUniverse.ReciprocalNoDilation.NoDilationInvariant R →
    (∀ (p q r : BlockUniverse.Event.{0} ℝ), R p q → R q r → R p r) →
      ∀ {v w : BlockUniverse.Event.{0} ℝ},
        BlockUniverse.ReciprocalNoDilation.Mutual R v →
          BlockUniverse.ReciprocalNoDilation.Mutual R w →
            BlockUniverse.ReciprocalNoDilation.Mutual R (BlockUniverse.ReciprocalNoDilation.addE v w)
'BlockUniverse.ReciprocalNoDilation.mutual_add' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
@BlockUniverse.ReciprocalNoDilation.mutual_neg : ∀ {R : BlockUniverse.Event.{0} ℝ → BlockUniverse.Event.{0} ℝ → Prop},
  BlockUniverse.ReciprocalNoDilation.NoDilationInvariant R →
    ∀ {v : BlockUniverse.Event.{0} ℝ},
      BlockUniverse.ReciprocalNoDilation.Mutual R v →
        BlockUniverse.ReciprocalNoDilation.Mutual R (BlockUniverse.ReciprocalNoDilation.negE v)
'BlockUniverse.ReciprocalNoDilation.mutual_neg' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
@BlockUniverse.ReciprocalNoDilation.mutual_sub : ∀ {R : BlockUniverse.Event.{0} ℝ → BlockUniverse.Event.{0} ℝ → Prop},
  BlockUniverse.ReciprocalNoDilation.NoDilationInvariant R →
    (∀ (p q r : BlockUniverse.Event.{0} ℝ), R p q → R q r → R p r) →
      ∀ {v w : BlockUniverse.Event.{0} ℝ},
        BlockUniverse.ReciprocalNoDilation.Mutual R v →
          BlockUniverse.ReciprocalNoDilation.Mutual R w →
            BlockUniverse.ReciprocalNoDilation.Mutual R (BlockUniverse.ReciprocalNoDilation.subE v w)
'BlockUniverse.ReciprocalNoDilation.mutual_sub' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
@BlockUniverse.ReciprocalNoDilation.mutual_boost : ∀ {R : BlockUniverse.Event.{0} ℝ → BlockUniverse.Event.{0} ℝ → Prop},
  BlockUniverse.ReciprocalNoDilation.NoDilationInvariant R →
    ∀ {v : BlockUniverse.Event.{0} ℝ},
      BlockUniverse.ReciprocalNoDilation.Mutual R v →
        ∀ {l : ℝ}, LT.lt.{0} 0 l → BlockUniverse.ReciprocalNoDilation.Mutual R (BlockUniverse.Stein.boost.{0} l v)
'BlockUniverse.ReciprocalNoDilation.mutual_boost' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
@BlockUniverse.ReciprocalNoDilation.mutual_reflect : ∀
  {R : BlockUniverse.Event.{0} ℝ → BlockUniverse.Event.{0} ℝ → Prop},
  BlockUniverse.ReciprocalNoDilation.NoDilationInvariant R →
    ∀ {v : BlockUniverse.Event.{0} ℝ},
      BlockUniverse.ReciprocalNoDilation.Mutual R v →
        BlockUniverse.ReciprocalNoDilation.Mutual R (BlockUniverse.Stein.reflect.{0} v)
'BlockUniverse.ReciprocalNoDilation.mutual_reflect' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.ReciprocalNoDilation.positive_boost_difference : ∀ (s : ℝ),
  ∃ l, LT.lt.{0} 0 l ∧ Eq.{1} (HSub.hSub.{0, 0, 0} l (HDiv.hDiv.{0, 0, 0} 1 l)) s
'BlockUniverse.ReciprocalNoDilation.positive_boost_difference' depends on axioms: [propext,
 Classical.choice.{u},
 Quot.sound.{u}]
@BlockUniverse.ReciprocalNoDilation.time_to_all_space : ∀
  {R : BlockUniverse.Event.{0} ℝ → BlockUniverse.Event.{0} ℝ → Prop},
  BlockUniverse.ReciprocalNoDilation.NoDilationInvariant R →
    (∀ (p q r : BlockUniverse.Event.{0} ℝ), R p q → R q r → R p r) →
      ∀ {a : ℝ},
        Ne.{1} a 0 →
          BlockUniverse.ReciprocalNoDilation.Mutual R (BlockUniverse.ReciprocalNoDilation.timeE a) →
            ∀ (x : ℝ), BlockUniverse.ReciprocalNoDilation.Mutual R (BlockUniverse.ReciprocalNoDilation.spaceE x)
'BlockUniverse.ReciprocalNoDilation.time_to_all_space' depends on axioms: [propext,
 Classical.choice.{u},
 Quot.sound.{u}]
@BlockUniverse.ReciprocalNoDilation.space_to_all_time : ∀
  {R : BlockUniverse.Event.{0} ℝ → BlockUniverse.Event.{0} ℝ → Prop},
  BlockUniverse.ReciprocalNoDilation.NoDilationInvariant R →
    (∀ (p q r : BlockUniverse.Event.{0} ℝ), R p q → R q r → R p r) →
      ∀ {a : ℝ},
        Ne.{1} a 0 →
          BlockUniverse.ReciprocalNoDilation.Mutual R (BlockUniverse.ReciprocalNoDilation.spaceE a) →
            ∀ (x : ℝ), BlockUniverse.ReciprocalNoDilation.Mutual R (BlockUniverse.ReciprocalNoDilation.timeE x)
'BlockUniverse.ReciprocalNoDilation.space_to_all_time' depends on axioms: [propext,
 Classical.choice.{u},
 Quot.sound.{u}]
@BlockUniverse.ReciprocalNoDilation.nonzero_mutual_universal : ∀
  {R : BlockUniverse.Event.{0} ℝ → BlockUniverse.Event.{0} ℝ → Prop},
  BlockUniverse.ReciprocalNoDilation.NoDilationInvariant R →
    (∀ (p q r : BlockUniverse.Event.{0} ℝ), R p q → R q r → R p r) →
      ∀ {v : BlockUniverse.Event.{0} ℝ},
        Ne.{1} v BlockUniverse.Stein.O.{0} →
          BlockUniverse.ReciprocalNoDilation.Mutual R v → ∀ (p q : BlockUniverse.Event.{0} ℝ), R p q
'BlockUniverse.ReciprocalNoDilation.nonzero_mutual_universal' depends on axioms: [propext,
 Classical.choice.{u},
 Quot.sound.{u}]
@BlockUniverse.ReciprocalNoDilation.one_reciprocal_pair_forces_universal : ∀
  {R : BlockUniverse.Event.{0} ℝ → BlockUniverse.Event.{0} ℝ → Prop},
  BlockUniverse.ReciprocalNoDilation.NoDilationInvariant R →
    (∀ (p q r : BlockUniverse.Event.{0} ℝ), R p q → R q r → R p r) →
      ∀ (p q : BlockUniverse.Event.{0} ℝ), Ne.{1} p q → R p q → R q p → ∀ (a b : BlockUniverse.Event.{0} ℝ), R a b
'BlockUniverse.ReciprocalNoDilation.one_reciprocal_pair_forces_universal' depends on axioms: [propext,
 Classical.choice.{u},
 Quot.sound.{u}]
BlockUniverse.ReciprocalThreePlusOne.boost_zero : ∀ (i : Fin 3) (l : ℝ),
  Eq.{1} (BlockUniverse.ReciprocalThreePlusOne.boostV i l 0) 0
'BlockUniverse.ReciprocalThreePlusOne.boost_zero' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
BlockUniverse.ReciprocalThreePlusOne.halfturn_zero : ∀ (i : Fin 3),
  Eq.{1} (BlockUniverse.ReciprocalThreePlusOne.halfturnV i 0) 0
'BlockUniverse.ReciprocalThreePlusOne.halfturn_zero' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
@BlockUniverse.ReciprocalThreePlusOne.boost_mem : ∀
  {R : BlockUniverse.ReciprocalThreePlusOne.V → BlockUniverse.ReciprocalThreePlusOne.V → Prop}
  (hI : BlockUniverse.ReciprocalThreePlusOne.Invariant R)
  (htrans : ∀ (p q r : BlockUniverse.ReciprocalThreePlusOne.V), R p q → R q r → R p r) (h0 : R 0 0)
  {v : BlockUniverse.ReciprocalThreePlusOne.V},
  Membership.mem.{0, 0} (BlockUniverse.ReciprocalThreePlusOne.mutualSubgroup hI htrans h0) v →
    ∀ (i : Fin 3) {l : ℝ},
      LT.lt.{0} 0 l →
        Membership.mem.{0, 0} (BlockUniverse.ReciprocalThreePlusOne.mutualSubgroup hI htrans h0)
          (BlockUniverse.ReciprocalThreePlusOne.boostV i l v)
'BlockUniverse.ReciprocalThreePlusOne.boost_mem' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
@BlockUniverse.ReciprocalThreePlusOne.halfturn_mem : ∀
  {R : BlockUniverse.ReciprocalThreePlusOne.V → BlockUniverse.ReciprocalThreePlusOne.V → Prop}
  (hI : BlockUniverse.ReciprocalThreePlusOne.Invariant R)
  (htrans : ∀ (p q r : BlockUniverse.ReciprocalThreePlusOne.V), R p q → R q r → R p r) (h0 : R 0 0)
  {v : BlockUniverse.ReciprocalThreePlusOne.V},
  Membership.mem.{0, 0} (BlockUniverse.ReciprocalThreePlusOne.mutualSubgroup hI htrans h0) v →
    ∀ (i : Fin 3),
      Membership.mem.{0, 0} (BlockUniverse.ReciprocalThreePlusOne.mutualSubgroup hI htrans h0)
        (BlockUniverse.ReciprocalThreePlusOne.halfturnV i v)
'BlockUniverse.ReciprocalThreePlusOne.halfturn_mem' depends on axioms: [propext, Classical.choice.{u}, Quot.sound.{u}]
@BlockUniverse.ReciprocalThreePlusOne.time_to_all_axes : ∀
  {R : BlockUniverse.ReciprocalThreePlusOne.V → BlockUniverse.ReciprocalThreePlusOne.V → Prop}
  (hI : BlockUniverse.ReciprocalThreePlusOne.Invariant R)
  (htrans : ∀ (p q r : BlockUniverse.ReciprocalThreePlusOne.V), R p q → R q r → R p r) (h0 : R 0 0) {a : ℝ},
  Ne.{1} a 0 →
    Membership.mem.{0, 0} (BlockUniverse.ReciprocalThreePlusOne.mutualSubgroup hI htrans h0)
        (BlockUniverse.ReciprocalThreePlusOne.timeV a) →
      ∀ (i : Fin 3) (x : ℝ),
        Membership.mem.{0, 0} (BlockUniverse.ReciprocalThreePlusOne.mutualSubgroup hI htrans h0)
          (BlockUniverse.ReciprocalThreePlusOne.axisV i x)
'BlockUniverse.ReciprocalThreePlusOne.time_to_all_axes' depends on axioms: [propext,
 Classical.choice.{u},
 Quot.sound.{u}]
@BlockUniverse.ReciprocalThreePlusOne.axes_to_all_time : ∀
  {R : BlockUniverse.ReciprocalThreePlusOne.V → BlockUniverse.ReciprocalThreePlusOne.V → Prop}
  (hI : BlockUniverse.ReciprocalThreePlusOne.Invariant R)
  (htrans : ∀ (p q r : BlockUniverse.ReciprocalThreePlusOne.V), R p q → R q r → R p r) (h0 : R 0 0),
  (∀ (i : Fin 3) (x : ℝ),
      Membership.mem.{0, 0} (BlockUniverse.ReciprocalThreePlusOne.mutualSubgroup hI htrans h0)
        (BlockUniverse.ReciprocalThreePlusOne.axisV i x)) →
    ∀ (t : ℝ),
      Membership.mem.{0, 0} (BlockUniverse.ReciprocalThreePlusOne.mutualSubgroup hI htrans h0)
        (BlockUniverse.ReciprocalThreePlusOne.timeV t)
'BlockUniverse.ReciprocalThreePlusOne.axes_to_all_time' depends on axioms: [propext,
 Classical.choice.{u},
 Quot.sound.{u}]
@BlockUniverse.ReciprocalThreePlusOne.nonzero_mutual_universal : ∀
  {R : BlockUniverse.ReciprocalThreePlusOne.V → BlockUniverse.ReciprocalThreePlusOne.V → Prop}
  (hI : BlockUniverse.ReciprocalThreePlusOne.Invariant R)
  (htrans : ∀ (p q r : BlockUniverse.ReciprocalThreePlusOne.V), R p q → R q r → R p r) (h0 : R 0 0)
  {v : BlockUniverse.ReciprocalThreePlusOne.V},
  Ne.{1} v 0 →
    Membership.mem.{0, 0} (BlockUniverse.ReciprocalThreePlusOne.mutualSubgroup hI htrans h0) v →
      ∀ (p q : BlockUniverse.ReciprocalThreePlusOne.V), R p q
'BlockUniverse.ReciprocalThreePlusOne.nonzero_mutual_universal' depends on axioms: [propext,
 Classical.choice.{u},
 Quot.sound.{u}]
@BlockUniverse.ReciprocalThreePlusOne.one_reciprocal_pair_forces_universal : ∀
  {R : BlockUniverse.ReciprocalThreePlusOne.V → BlockUniverse.ReciprocalThreePlusOne.V → Prop},
  BlockUniverse.ReciprocalThreePlusOne.Invariant R →
    (∀ (p q r : BlockUniverse.ReciprocalThreePlusOne.V), R p q → R q r → R p r) →
      ∀ (p q : BlockUniverse.ReciprocalThreePlusOne.V),
        Ne.{1} p q → R p q → R q p → ∀ (a b : BlockUniverse.ReciprocalThreePlusOne.V), R a b
'BlockUniverse.ReciprocalThreePlusOne.one_reciprocal_pair_forces_universal' depends on axioms: [propext,
 Classical.choice.{u},
 Quot.sound.{u}]
$ lake env lean DilationCountermodel.lean
DilationCountermodel.lean:14:0: warning: automatically included section variable(s) unused in theorem `BlockUniverse.Audit.duration_reflexive`:
  [IsStrictOrderedRing K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [IsStrictOrderedRing K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
'BlockUniverse.Audit.duration_reflexive' depends on axioms: [propext, Quot.sound]
'BlockUniverse.Audit.duration_transitive' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockUniverse.Audit.duration_translate' depends on axioms: [propext, Quot.sound]
'BlockUniverse.Audit.duration_boost' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockUniverse.Audit.duration_reflect' depends on axioms: [propext, Quot.sound]
'BlockUniverse.Audit.duration_not_dilation_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
PASS: six modules; 65 named proofs; six countermodel proofs; 9 dependency revisions checked.
Audited axiom union: Classical.choice, Quot.sound, propext
