Hyperdynamics.lean`

Explanation legend

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

17 declarations, 0 contain sorry, 0 axioms

Hyperdynamics

[FRAME] Indexed transformations without assuming a universal temporal axis.

This is the Lean port of the local hyperdynamics candidate. It carries the transition system and the properties that frame establishes.

The frame's central refusal is that a step is not a moment. The state carrier is a set of named states, the step relation is a set of pairs, and the index of a step is local to the system. Nothing here is a clock, nothing here is physical duration, and nothing here says that a reachable state is a state that will be reached.

What is not proved here, and cannot be, is any claim that these finite systems are the right models of change. The Python source carries the same [FRAME] classification and this port keeps it: a finite reachability result is not a foundation.

Imports (2)

Imported by 1 file

Hyperfields/AllFields.lean

structure Hyperfields.Fields.Hyperdynamics.TransitionSystem A finite transition system with its state kinds line 43 source
A finite transition system: its states, its steps, and the kind of each state.
The kinds are declared per state, exactly one per state, and the port keeps them separate from the steps. A step is a relation between two identified states; it is not an interval and it is not a position in an assumed global order.

Every state is named and carries one declared kind, so a step is between two identified states rather than between positions in an assumed sequence.

no axioms what this means
Statement uses: Nat
```
structure TransitionSystem (n : Nat) where
…
```
def Hyperfields.Fields.Hyperdynamics.TransitionSystem.kindOfState Read a state's kind line 53 source
The kind declared for a state, if any.

A state's kind is a name rather than a position, so it is read separately from the transition relation.
Prerequisites: Hyperfields.Fields.Hyperdynamics.TransitionSystem

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hyperdynamics.TransitionSystem, Fin, Option, String
Proof uses: Hyperfields.Fields.Hyperdynamics.TransitionSystem.kindOfState.match_1, Prod, List.find?, BEq.beq, Prod.fst, Hyperfields.Fields.Hyperdynamics.TransitionSystem.kindOf, Option.some, Prod.snd, Unit, Option.none
4 instances, coercions and auxiliary constants left out.
```
def TransitionSystem.kindOfState {n : Nat} (system : TransitionSystem n)
    (state : Fin n) : Option String :=
…
```
Mentions: Hyperfields.Fields.Hyperdynamics.TransitionSystem
def Hyperfields.Fields.Hyperdynamics.TransitionSystem.wellShaped The axioms a transition system must satisfy line 70 source
Whether the system satisfies the axioms.
The checks are:
1. Every step has both endpoints in the state carrier.
2. Every state has exactly one kind, and no state outside the carrier has one.
A step to a state the system does not have describes a change into nothing, and a state with two kinds is described twice.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hyperdynamics.TransitionSystem, Bool
Proof uses: Bool.and, List.all, Prod, Fin, Hyperfields.Fields.Hyperdynamics.TransitionSystem.steps, Hyperfields.Finite.mem, Prod.fst, Hyperfields.Fields.Hyperdynamics.TransitionSystem.states, Prod.snd, String, Hyperfields.Fields.Hyperdynamics.TransitionSystem.kindOf, BEq.beq, List.length, List.eraseDups, List.map
6 instances, coercions and auxiliary constants left out.
```
def TransitionSystem.wellShaped {n : Nat} (system : TransitionSystem n) : Bool :=
…
```
Mentions: Hyperfields.Fields.Hyperdynamics.TransitionSystem
def Hyperfields.Fields.Hyperdynamics.reachable What a system can reach line 91 source
The states reachable from a starting state.
Reachability is computed by a bounded forward walk over the step relation. The bound is the size of the state carrier: a state that is reachable at all is reachable within that many steps, because a shortest path never repeats a state.

A state is reachable when some path of declared steps arrives at it, and the walk is bounded by the number of states.
Prerequisites: Hyperfields.Fields.Hyperdynamics.TransitionSystem

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hyperdynamics.TransitionSystem, Fin, List
Proof uses: List.flatMap, List.map, Prod, Prod.snd, List.filter, BEq.beq, Prod.fst, Hyperfields.Fields.Hyperdynamics.TransitionSystem.steps, List.foldl, HAppend.hAppend, List.cons, List.nil, List.range, List.eraseDups
6 instances, coercions and auxiliary constants left out.
```
def reachable {n : Nat} (system : TransitionSystem n) (start : Fin n) : List (Fin n) :=
…
```
Mentions: Hyperfields.Fields.Hyperdynamics.TransitionSystem
def Hyperfields.Fields.Hyperdynamics.pathLifts Lifting a path through a partial bridge line 117 source
Whether a path lifts through a bridge.
The path must be a path in the source: every state on it is in the source carrier, and every consecutive pair is a declared step. The bridge must cover every state on the path, and the lifted sequence must be a path in the target.
The lift is computed by looking each state up in the bridge. A state the bridge does not cover makes the lift fail, and it is checked separately rather than papered over with a default value: a default would let an uncovered state masquerade as a lifted one.

A lifted path must be a path in the target, so the bridge has to carry every step of the source path into a declared step of the target.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hyperdynamics.TransitionSystem, List, Fin, Prod, Bool
Proof uses: Bool.and, List.all, Hyperfields.Finite.mem, Hyperfields.Fields.Hyperdynamics.TransitionSystem.states, List.zip, List.drop, OfNat.ofNat, Hyperfields.Fields.Hyperdynamics.TransitionSystem.steps, List.any, BEq.beq, Prod.fst, List.map, Prod.snd, Hyperfields.Fields.Hyperdynamics.pathLifts.match_1, Option, List.find?, Prod.mk, Bool.false
6 instances, coercions and auxiliary constants left out.
```
def pathLifts {m n : Nat} (source : TransitionSystem m) (target : TransitionSystem n)
    (path : List (Fin m)) (bridge : List (Fin m × Fin n)) : Bool :=
…
```
Mentions: Hyperfields.Fields.Hyperdynamics.TransitionSystem
def Hyperfields.Fields.Hyperdynamics.chainSystem A three-state transition system line 145 source
A concrete transition system: a steps to b, b steps to c, and c steps to nothing.
The two kinds are declared so that the kind condition is not vacuous: a and c share one kind and b has another.

A concrete system lets the compiler check the axioms and the reachability against something a reader can see.

standard axioms: propext what this means
Statement uses: Hyperfields.Fields.Hyperdynamics.TransitionSystem, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hyperdynamics.TransitionSystem.mk, List.cons, Fin, List.nil, Prod, Prod.mk, String
4 instances, coercions and auxiliary constants left out.
```
def chainSystem : TransitionSystem 3 where
…
```
Mentions: Hyperfields.Fields.Hyperdynamics.TransitionSystem
def Hyperfields.Fields.Hyperdynamics.cyclicSystem A system with a cycle line 159 source
A concrete transition system with a cycle: a steps to b and b steps back to a.
Reachability from a is the whole carrier, which is what makes the difference between "reachable" and "eventually arrives" visible.

A cycle makes the point that reachability is about the step relation, not about a direction of time.

standard axioms: propext what this means
Statement uses: Hyperfields.Fields.Hyperdynamics.TransitionSystem, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hyperdynamics.TransitionSystem.mk, List.cons, Fin, List.nil, Prod, Prod.mk, String
4 instances, coercions and auxiliary constants left out.
```
def cyclicSystem : TransitionSystem 3 where
…
```
Mentions: Hyperfields.Fields.Hyperdynamics.TransitionSystem
theorem Hyperfields.Fields.Hyperdynamics.chain_system_is_well_shaped The transition system satisfies the axioms line 167 source
The worked transition system satisfies the axioms.

The concrete example must clear the axioms the frame demands, or the example proves nothing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hyperdynamics.TransitionSystem.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperdynamics.chainSystem, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 168
  before
```
⊢ chainSystem.wellShaped = true
```
  after
  no goals remain
```
theorem chain_system_is_well_shaped : chainSystem.wellShaped = true := by
…
```
theorem Hyperfields.Fields.Hyperdynamics.cyclic_system_is_well_shaped The cyclic system satisfies the axioms line 173 source
The worked cyclic transition system satisfies the axioms.

A cycle in the step relation is allowed; a step to a state the system does not have is not.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hyperdynamics.TransitionSystem.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperdynamics.cyclicSystem, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 174
  before
```
⊢ cyclicSystem.wellShaped = true
```
  after
  no goals remain
```
theorem cyclic_system_is_well_shaped : cyclicSystem.wellShaped = true := by
…
```
theorem Hyperfields.Fields.Hyperdynamics.all_states_are_reachable_from_the_start Every state is reachable from the first line 179 source
Every state is reachable from the first state of the chain system.

A chain of steps reaches everything downstream, and the compiler can check the whole reachable set at once.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperdynamics.reachable, Hyperfields.Fields.Hyperdynamics.chainSystem, List.cons, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 181
  before
```
⊢ reachable chainSystem 0 = [0, 1, 2]
```
  after
  no goals remain
```
theorem all_states_are_reachable_from_the_start :
    reachable chainSystem 0 = [0, 1, 2] := by
…
```
Mentions: Hyperfields.Fields.Hyperdynamics.reachable, Hyperfields.Fields.Hyperdynamics.chainSystem
theorem Hyperfields.Fields.Hyperdynamics.a_terminal_state_reaches_only_itself A state with no outgoing step reaches only itself line 192 source
Only the last state is reachable from the last state of the chain system.
This is the case that distinguishes reachability from a claim about progress. The state 2 is a perfectly good state; it simply has no outgoing step, and nothing here says that is a defect.

Reachability is about the step relation, so a state that steps to nothing reaches nothing but itself.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperdynamics.reachable, Hyperfields.Fields.Hyperdynamics.chainSystem, List.cons, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 194
  before
```
⊢ reachable chainSystem 2 = [2]
```
  after
  no goals remain
```
theorem a_terminal_state_reaches_only_itself :
    reachable chainSystem 2 = [2] := by
…
```
Mentions: Hyperfields.Fields.Hyperdynamics.reachable, Hyperfields.Fields.Hyperdynamics.chainSystem
theorem Hyperfields.Fields.Hyperdynamics.a_cycle_reaches_back A cycle makes every state in the cycle reachable line 199 source
Every state in the cyclic system is reachable from the first.

A cycle lets a state be reached from itself by a nonempty path, which is what makes the closure of the step relation nontrivial.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperdynamics.reachable, Hyperfields.Fields.Hyperdynamics.cyclicSystem, List.cons, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 201
  before
```
⊢ reachable cyclicSystem 0 = [0, 1]
```
  after
  no goals remain
```
theorem a_cycle_reaches_back :
    reachable cyclicSystem 0 = [0, 1] := by
…
```
Mentions: Hyperfields.Fields.Hyperdynamics.reachable, Hyperfields.Fields.Hyperdynamics.cyclicSystem
theorem Hyperfields.Fields.Hyperdynamics.a_step_to_an_undeclared_state_is_rejected A step to an undeclared state is rejected line 211 source
A system with a step to a state outside its carrier is rejected.
This is the negative case. A checker that never rejects anything is not a check, and this theorem is what makes the positive cases meaningful.

A transition into a state the system does not have describes a change into nothing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hyperdynamics.TransitionSystem.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperdynamics.TransitionSystem.mk, List.cons, Fin, List.nil, Prod, Prod.mk, String, Bool.false
Proof uses: of_decide_eq_true, id, Decidable.decide, Bool.true, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 215
  before
```
⊢ { states := [0, 1], steps := [(0, 1), (1, 2)], kindOf := [(0, "phase"), (1, "phase")] }.wellShaped = false
```
  after
  no goals remain
```
theorem a_step_to_an_undeclared_state_is_rejected :
    ({ states := [0, 1],
…
```
theorem Hyperfields.Fields.Hyperdynamics.a_state_with_two_kinds_is_rejected A state with two kinds is rejected line 226 source
A system that declares two kinds for one state is rejected.
This is the second negative case, and it is independent of the step endpoints: a system can have only well-formed steps and still describe a state twice.

A state declared twice is described twice, and the frame requires exactly one kind per state.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hyperdynamics.TransitionSystem.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperdynamics.TransitionSystem.mk, List.cons, Fin, List.nil, Prod, Prod.mk, String, Bool.false
Proof uses: of_decide_eq_true, id, Decidable.decide, Bool.true, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 230
  before
```
⊢ { states := [0, 1], steps := [(0, 1)], kindOf := [(0, "phase"), (0, "other"), (1, "phase")] }.wellShaped = false
```
  after
  no goals remain
```
theorem a_state_with_two_kinds_is_rejected :
    ({ states := [0, 1],
…
```
theorem Hyperfields.Fields.Hyperdynamics.the_identity_bridge_lifts_the_path The identity bridge lifts a path line 240 source
The identity bridge lifts the chain path onto itself.
Every step of the path is preserved because the bridge carries each state to itself, so the lifted sequence is the same sequence.

A path is always a path under the identity, which is the baseline the other lifting cases are measured against.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hyperdynamics.pathLifts, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperdynamics.chainSystem, List.cons, Fin, List.nil, Prod, Prod.mk, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 242
  before
```
⊢ pathLifts chainSystem chainSystem [0, 1, 2] [(0, 0), (1, 1), (2, 2)] = true
```
  after
  no goals remain
```
theorem the_identity_bridge_lifts_the_path :
    pathLifts chainSystem chainSystem [0, 1, 2] [(0, 0), (1, 1), (2, 2)] = true := by
…
```
Mentions: Hyperfields.Fields.Hyperdynamics.pathLifts, Hyperfields.Fields.Hyperdynamics.chainSystem
theorem Hyperfields.Fields.Hyperdynamics.a_step_breaking_bridge_does_not_lift A bridge that drops a step does not lift a path line 254 source
A bridge that maps both ends of a step onto the same state does not lift the path.
The lifted sequence would be [0, 0], whose pair is not a declared step of the target, so the lift fails. This is the negative case for path lifting.

A lift must be a path in the target, so a bridge that lands the two endpoints on the same state breaks the step.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hyperdynamics.pathLifts, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperdynamics.chainSystem, List.cons, Fin, List.nil, Prod, Prod.mk, Bool.false
Proof uses: of_decide_eq_true, id, Decidable.decide, Bool.true, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 256
  before
```
⊢ pathLifts chainSystem chainSystem [0, 1] [(0, 0), (1, 0)] = false
```
  after
  no goals remain
```
theorem a_step_breaking_bridge_does_not_lift :
    pathLifts chainSystem chainSystem [0, 1] [(0, 0), (1, 0)] = false := by
…
```
Mentions: Hyperfields.Fields.Hyperdynamics.pathLifts, Hyperfields.Fields.Hyperdynamics.chainSystem
def Hyperfields.Fields.Hyperdynamics.entry Hyperdynamics explainer entry line 266 source
The canonical Hyperdynamics record used by the unified portal.

This declaration exposes the checked ecosystem record for Hyperdynamics on its own stable explainer page.
See also: Hyperfields.hyperdynamics

no axioms what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.hyperdynamics
```
def entry : Hyperfields.Entry := Hyperfields.hyperdynamics
…
```
Mentions: Hyperfields.Entry, Hyperfields.hyperdynamics