Hypermechanics.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

23 declarations, 0 contain sorry, 0 axioms

Hypermechanics

[FRAME] Exact guarded transfers; counters have no assumed physical units.

This is the Lean port of the local hypermechanics candidate. It carries the mechanism state, the rewrite rule, and the properties that frame establishes.

The counts are exact. As in the geometry port, Lean 4 core's Rat does not reduce for decide, so the counts are held as integer numerators over one shared scale, and the conservation invariant is checked as an exact integer equality. A conservation check that used floating point would be a different claim, and a weaker one.

The conservation invariant is the frame's centre. A rewrite rule declares a weight for every place it changes, and the rule is admissible only when the weighted sum of the changes is exactly zero. That is a statement about the rule, not about the world: it says the rule is declared to conserve what it says it conserves.

What is not proved here, and cannot be, is any claim that any physical process obeys this, that these counts are quantities in any unit, or that the frame's mechanisms are the right ones. The Python source carries the same [FRAME] classification and this port keeps it.

Imports (3)

Imported by 1 file

Hyperfields/AllFields.lean

structure Hyperfields.Fields.Hypermechanics.MechanismState A state of named places holding exact counts line 52 source
A mechanism state: named places, the exact count in each, and the kind of each place.
The counts are numerators over one shared scale, so every count in one state is comparable with every other. The kinds are declared per place, exactly one per place, and the port keeps them separate from the counts: a place's kind is not a quantity.

A state is a map from named places to exact counts, and the counts carry no unit because the frame does not assign one.

no axioms what this means
Statement uses: Nat
```
structure MechanismState (n : Nat) where
…
```
def Hyperfields.Fields.Hypermechanics.MechanismState.amount Read a place's count line 62 source
The count in a place, if the place has one.

A place the state does not carry has no count, which is nothing rather than zero.
Prerequisites: Hyperfields.Fields.Hypermechanics.MechanismState

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypermechanics.MechanismState, Fin, Option, Int
Proof uses: Hyperfields.Fields.Hypermechanics.MechanismState.amount.match_1, Prod, List.find?, BEq.beq, Prod.fst, Hyperfields.Fields.Hypermechanics.MechanismState.amounts, Option.some, Prod.snd, Unit, Option.none
4 instances, coercions and auxiliary constants left out.
```
def MechanismState.amount {n : Nat} (state : MechanismState n)
    (place : Fin n) : Option Int :=
…
```
Mentions: Hyperfields.Fields.Hypermechanics.MechanismState
def Hyperfields.Fields.Hypermechanics.MechanismState.kindOfPlace Read a place's kind line 72 source
The kind of a place, if the place has one.

A kind is a name rather than a quantity, so it is read separately from the count.
Prerequisites: Hyperfields.Fields.Hypermechanics.MechanismState

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypermechanics.MechanismState, Fin, Option, String
Proof uses: Hyperfields.Fields.Hypermechanics.MechanismState.kindOfPlace.match_1, Prod, List.find?, BEq.beq, Prod.fst, Hyperfields.Fields.Hypermechanics.MechanismState.kindOf, Option.some, Prod.snd, Unit, Option.none
4 instances, coercions and auxiliary constants left out.
```
def MechanismState.kindOfPlace {n : Nat} (state : MechanismState n)
    (place : Fin n) : Option String :=
…
```
Mentions: Hyperfields.Fields.Hypermechanics.MechanismState
def Hyperfields.Fields.Hypermechanics.MechanismState.wellShaped The axioms a mechanism state must satisfy line 89 source
Whether the state satisfies the axioms.
The checks are:
1. Every count is nonnegative.
2. Every place has exactly one count and one kind, and no place outside the count carrier has one.
A state with a negative count is not a state, and a place declared twice is described twice.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypermechanics.MechanismState, Bool
Proof uses: Bool.and, List.all, Prod, Fin, Int, Hyperfields.Fields.Hypermechanics.MechanismState.amounts, Decidable.decide, LE.le, OfNat.ofNat, Prod.snd, BEq.beq, List.length, List.eraseDups, List.map, Prod.fst, String, Hyperfields.Fields.Hypermechanics.MechanismState.kindOf, List.any
9 instances, coercions and auxiliary constants left out.
```
def MechanismState.wellShaped {n : Nat} (state : MechanismState n) : Bool :=
…
```
Mentions: Hyperfields.Fields.Hypermechanics.MechanismState
structure Hyperfields.Fields.Hypermechanics.RewriteRule A guarded rewrite with an exact conservation invariant line 116 source
A rewrite rule: the guard minima, the changes, and the conservation weights.
The rule is admissible only when it conserves exactly what it says it conserves. The conservation condition is:
```
Σ weight(place) × change(place)  =  0
```
over the places the rule changes, with exact integer arithmetic. A rule whose weighted sum is nonzero is refused, not repaired.
A rule says what must be true before it fires, what it changes, and what it conserves, and the three are checked together.

no axioms what this means
Statement uses: Nat
```
structure RewriteRule (n : Nat) where
…
```
def Hyperfields.Fields.Hypermechanics.RewriteRule.weightOf Read a place's weight line 126 source
The weight of a place in a rule's invariant, if it has one.

A place the invariant does not mention has no weight, and the conservation sum skips it.
Prerequisites: Hyperfields.Fields.Hypermechanics.RewriteRule

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypermechanics.RewriteRule, Fin, Option, Int
Proof uses: Hyperfields.Fields.Hypermechanics.MechanismState.amount.match_1, Prod, List.find?, BEq.beq, Prod.fst, Hyperfields.Fields.Hypermechanics.RewriteRule.invariant, Option.some, Prod.snd, Unit, Option.none
4 instances, coercions and auxiliary constants left out.
```
def RewriteRule.weightOf {n : Nat} (rule : RewriteRule n) (place : Fin n) : Option Int :=
…
```
Mentions: Hyperfields.Fields.Hypermechanics.RewriteRule
def Hyperfields.Fields.Hypermechanics.RewriteRule.changeOf Read a place's change line 135 source
The change a rule makes to a place, if it makes one.

A place the rule does not change has no delta, which is nothing rather than a zero change.
Prerequisites: Hyperfields.Fields.Hypermechanics.RewriteRule

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypermechanics.RewriteRule, Fin, Option, Int
Proof uses: Hyperfields.Fields.Hypermechanics.MechanismState.amount.match_1, Prod, List.find?, BEq.beq, Prod.fst, Hyperfields.Fields.Hypermechanics.RewriteRule.changes, Option.some, Prod.snd, Unit, Option.none
4 instances, coercions and auxiliary constants left out.
```
def RewriteRule.changeOf {n : Nat} (rule : RewriteRule n) (place : Fin n) : Option Int :=
…
```
Mentions: Hyperfields.Fields.Hypermechanics.RewriteRule
def Hyperfields.Fields.Hypermechanics.RewriteRule.weightedChange The conservation sum line 144 source
The weighted sum of a rule's changes.

Multiplying each change by its weight and adding them gives the quantity the rule claims to conserve, and a rule is admissible only when that sum is zero.
Prerequisites: Hyperfields.Fields.Hypermechanics.RewriteRule

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypermechanics.RewriteRule, Int
Proof uses: List.foldl, Prod, Fin, Hyperfields.Fields.Hypermechanics.RewriteRule.weightedChange.match_1, Option, Hyperfields.Fields.Hypermechanics.RewriteRule.weightOf, Prod.fst, Unit, HAdd.hAdd, HMul.hMul, Prod.snd, OfNat.ofNat, Hyperfields.Fields.Hypermechanics.RewriteRule.changes
5 instances, coercions and auxiliary constants left out.
```
def RewriteRule.weightedChange {n : Nat} (rule : RewriteRule n) : Int :=
…
```
Mentions: Hyperfields.Fields.Hypermechanics.RewriteRule
def Hyperfields.Fields.Hypermechanics.RewriteRule.wellShaped The axioms a rewrite rule must satisfy line 162 source
Whether the rule satisfies the axioms.
The checks are:
1. Every guard minimum is nonnegative.
2. Every changed place has an explicit invariant coefficient, and every invariant coefficient is strictly positive.
3. The rule conserves exactly: the weighted sum of the changes is zero.
A rule that conserves nothing is not a mechanism, and a rule with a negative guard is not a guard.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypermechanics.RewriteRule, Bool
Proof uses: List.all, Prod, Fin, Int, Hyperfields.Fields.Hypermechanics.RewriteRule.guards, Decidable.decide, LE.le, OfNat.ofNat, Prod.snd, Hyperfields.Fields.Hypermechanics.RewriteRule.invariant, LT.lt, Hyperfields.Fields.Hypermechanics.RewriteRule.changes, List.any, BEq.beq, Prod.fst, Bool.and, Hyperfields.Fields.Hypermechanics.RewriteRule.weightedChange
10 instances, coercions and auxiliary constants left out.
```
def RewriteRule.wellShaped {n : Nat} (rule : RewriteRule n) : Bool :=
…
```
Mentions: Hyperfields.Fields.Hypermechanics.RewriteRule
def Hyperfields.Fields.Hypermechanics.applyRule Fire a rule line 189 source
Apply a rule to a state. -- L4DEL: title: Fire a rule -- L4DEL: intuition: A rule fires only when every guard holds and no count would go negative, and otherwise it does not fire at all. -- L4DEL: prereq: Hyperfields.Fields.Hypermechanics.MechanismState, Hyperfields.Fields.Hypermechanics.RewriteRule
The rule fires only when every guard is satisfied. The result is the state with the rule's changes applied; a change that would make a count negative means the rule does not fire.

A rule fires only when every guard holds and no count would go negative, and otherwise it does not fire at all.
Prerequisites: Hyperfields.Fields.Hypermechanics.MechanismState, Hyperfields.Fields.Hypermechanics.RewriteRule

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypermechanics.MechanismState, Hyperfields.Fields.Hypermechanics.RewriteRule, Option
Proof uses: List, Fin, HAppend.hAppend, List.map, Prod, Int, Prod.fst, Hyperfields.Fields.Hypermechanics.RewriteRule.guards, Hyperfields.Fields.Hypermechanics.RewriteRule.changes, Bool, Bool.and, List.all, bne, Hyperfields.Fields.Hypermechanics.MechanismState.amount, Option.none, Hyperfields.Fields.Hypermechanics.RewriteRule.weightedChange.match_1, Unit, Bool.false, Decidable.decide, LE.le and 13 more
13 instances, coercions and auxiliary constants left out.
```
def applyRule {n : Nat} (state : MechanismState n) (rule : RewriteRule n) : Option (MechanismState n) :=
…
```
Mentions: Hyperfields.Fields.Hypermechanics.MechanismState, Hyperfields.Fields.Hypermechanics.RewriteRule
def Hyperfields.Fields.Hypermechanics.independent Two rules are independent line 224 source
Whether two rules have disjoint footprints. -- L4DEL: title: Two rules are independent -- L4DEL: intuition: If neither rule writes a place the other writes or reads, the order they fire in cannot matter, which is a sufficient condition for them to commute. -- L4DEL: prereq: Hyperfields.Fields.Hypermechanics.RewriteRule
Two rules are independent when neither writes a place the other writes or reads, and the other does not write a place the first reads. That is a sufficient condition for the two to commute, and the Python source calls it the same thing.

If neither rule writes a place the other writes or reads, the order they fire in cannot matter, which is a sufficient condition for them to commute.
Prerequisites: Hyperfields.Fields.Hypermechanics.RewriteRule

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypermechanics.RewriteRule, Bool
Proof uses: List, Fin, List.map, Prod, Int, Prod.fst, Hyperfields.Fields.Hypermechanics.RewriteRule.changes, Hyperfields.Fields.Hypermechanics.RewriteRule.guards, Bool.not, Bool.or, List.any, Hyperfields.Finite.mem
4 instances, coercions and auxiliary constants left out.
```
def independent {n : Nat} (left right : RewriteRule n) : Bool :=
…
```
Mentions: Hyperfields.Fields.Hypermechanics.RewriteRule
def Hyperfields.Fields.Hypermechanics.twoPlaceState A two-place mechanism state line 244 source
A concrete state: place 0 holds 2 and place 1 holds 1.
The two places have different kinds, so the kind condition is not vacuous.

A concrete state lets the compiler check the axioms and the rule application against something a reader can see.

standard axioms: propext what this means
Statement uses: Hyperfields.Fields.Hypermechanics.MechanismState, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hypermechanics.MechanismState.mk, Hyperfields.Exact.Scale.mk, Int, List.cons, Prod, Fin, Prod.mk, List.nil, String
5 instances, coercions and auxiliary constants left out.
```
def twoPlaceState : MechanismState 2 where
…
```
Mentions: Hyperfields.Fields.Hypermechanics.MechanismState
def Hyperfields.Fields.Hypermechanics.transferRule A conserving rewrite rule line 259 source
A concrete rule: move one unit from place 0 to place 1.
The guard requires place 0 to hold at least one unit. The change takes one unit from place 0 and gives one to place 1. The invariant weights both places by one, so the weighted sum of the changes is -1 + 1 = 0: the rule conserves the total exactly.

A rule that moves one unit from one place to another conserves the weighted total, and the compiler can check the exact sum.

standard axioms: propext what this means
Statement uses: Hyperfields.Fields.Hypermechanics.RewriteRule, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hypermechanics.RewriteRule.mk, List.cons, Prod, Fin, Int, Prod.mk, List.nil, Neg.neg
6 instances, coercions and auxiliary constants left out.
```
def transferRule : RewriteRule 2 where
…
```
Mentions: Hyperfields.Fields.Hypermechanics.RewriteRule
def Hyperfields.Fields.Hypermechanics.emptyState A state whose first place is empty line 272 source
A state whose first place is empty.
The guard on the transfer rule requires place 0 to hold at least one unit, so the rule cannot fire here.

A concrete state that fails a guard lets the compiler check that the guard actually refuses.

standard axioms: propext what this means
Statement uses: Hyperfields.Fields.Hypermechanics.MechanismState, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hypermechanics.MechanismState.mk, Hyperfields.Exact.Scale.mk, Int, List.cons, Prod, Fin, Prod.mk, List.nil, String
5 instances, coercions and auxiliary constants left out.
```
def emptyState : MechanismState 2 where
…
```
Mentions: Hyperfields.Fields.Hypermechanics.MechanismState
def Hyperfields.Fields.Hypermechanics.creatingRule A rule that does not conserve line 285 source
A concrete rule that creates a unit, and is therefore not admissible.
The change adds one unit to place 1 and nothing takes it away, so the weighted sum is 1, not zero. The rule is refused.

A rule whose weighted sum is nonzero is refused, and this is the case that shows the conservation check can fail.

standard axioms: propext what this means
Statement uses: Hyperfields.Fields.Hypermechanics.RewriteRule, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hypermechanics.RewriteRule.mk, List.nil, Prod, Fin, Int, List.cons, Prod.mk
5 instances, coercions and auxiliary constants left out.
```
def creatingRule : RewriteRule 2 where
…
```
Mentions: Hyperfields.Fields.Hypermechanics.RewriteRule
theorem Hyperfields.Fields.Hypermechanics.a_nonconserving_rule_is_rejected The conservation check rejects a rule that creates line 293 source
The creating rule is refused, because it does not conserve.

A rule whose weighted sum is nonzero is refused, and this is the case that shows the conservation check can fail.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypermechanics.RewriteRule.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hypermechanics.creatingRule, Bool.false
Proof uses: of_decide_eq_true, id, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 295
  before
```
⊢ creatingRule.wellShaped = false
```
  after
  no goals remain
```
theorem a_nonconserving_rule_is_rejected :
    creatingRule.wellShaped = false := by
…
```
theorem Hyperfields.Fields.Hypermechanics.two_place_state_is_well_shaped The state satisfies the axioms line 300 source
The worked mechanism state 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.Hypermechanics.MechanismState.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hypermechanics.twoPlaceState, 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 301
  before
```
⊢ twoPlaceState.wellShaped = true
```
  after
  no goals remain
```
theorem two_place_state_is_well_shaped : twoPlaceState.wellShaped = true := by
…
```
theorem Hyperfields.Fields.Hypermechanics.transfer_rule_is_well_shaped The conserving rule satisfies the axioms line 306 source
The worked rewrite rule 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.Hypermechanics.RewriteRule.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hypermechanics.transferRule, 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 307
  before
```
⊢ transferRule.wellShaped = true
```
  after
  no goals remain
```
theorem transfer_rule_is_well_shaped : transferRule.wellShaped = true := by
…
```
theorem Hyperfields.Fields.Hypermechanics.the_transfer_rule_conserves The rule conserves exactly line 312 source
The worked rewrite rule's weighted change is exactly zero.

The weighted sum of the changes is zero, and the compiler checks the sum rather than trusting the declaration.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Int, Hyperfields.Fields.Hypermechanics.RewriteRule.weightedChange, OfNat.ofNat, Nat, Hyperfields.Fields.Hypermechanics.transferRule
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
5 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 314
  before
```
⊢ transferRule.weightedChange = 0
```
  after
  no goals remain
```
theorem the_transfer_rule_conserves :
    transferRule.weightedChange = 0 := by
…
```
theorem Hyperfields.Fields.Hypermechanics.applying_the_rule_moves_one_unit Applying the rule moves one unit line 324 source
Applying the conserving rule to the worked state gives place 0 holding 1 and place 1 holding 2.
The total is unchanged, which is what the invariant declared.

The guard is satisfied and the change is exact, so the result is the state with one unit moved.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Option, Int, Option.map, Hyperfields.Fields.Hypermechanics.MechanismState, OfNat.ofNat, Nat, Hyperfields.Fields.Hypermechanics.MechanismState.amount, Fin, Hyperfields.Fields.Hypermechanics.applyRule, Hyperfields.Fields.Hypermechanics.twoPlaceState, Hyperfields.Fields.Hypermechanics.transferRule, Option.some
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
10 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 326
  before
```
⊢ Option.map (fun state => state.amount 0) (applyRule twoPlaceState transferRule) = some (some 1)
```
  after
  no goals remain
```
theorem applying_the_rule_moves_one_unit :
    (applyRule twoPlaceState transferRule).map (fun state => state.amount 0) = some (some 1) := by
…
```
Mentions: Hyperfields.Fields.Hypermechanics.applyRule, Hyperfields.Fields.Hypermechanics.twoPlaceState, Hyperfields.Fields.Hypermechanics.transferRule
theorem Hyperfields.Fields.Hypermechanics.the_rule_does_not_fire_when_guarded The rule does not fire when the guard is unsatisfied line 337 source
The rule does not fire on a state whose first place is empty.
This is the negative case for guards. A checker that never refuses anything is not a check, and this theorem is what makes the positive case meaningful.

A guard is a condition on the state, and a rule that fires anyway would not be guarded.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Option, Hyperfields.Fields.Hypermechanics.MechanismState, OfNat.ofNat, Nat, Hyperfields.Fields.Hypermechanics.applyRule, Hyperfields.Fields.Hypermechanics.emptyState, Hyperfields.Fields.Hypermechanics.transferRule, Option.none
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 339
  before
```
⊢ applyRule emptyState transferRule = none
```
  after
  no goals remain
```
theorem the_rule_does_not_fire_when_guarded :
    (applyRule emptyState transferRule) = none := by
…
```
Mentions: Hyperfields.Fields.Hypermechanics.applyRule, Hyperfields.Fields.Hypermechanics.emptyState, Hyperfields.Fields.Hypermechanics.transferRule
theorem Hyperfields.Fields.Hypermechanics.a_rule_is_not_independent_of_itself A rule is not independent of itself line 351 source
A rule is not independent of itself.
The rule writes place 0 and reads place 0, so the two footprints overlap. This is the negative case for independence, and it is the minimal one: a rule that cannot commute with itself cannot be expected to commute with a copy of itself.

A rule that writes a place it also reads is not independent of itself, which is the minimal case of the disjoint-footprint criterion.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypermechanics.independent, OfNat.ofNat, Nat, Hyperfields.Fields.Hypermechanics.transferRule, Bool.false
Proof uses: of_decide_eq_true, id, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 353
  before
```
⊢ independent transferRule transferRule = false
```
  after
  no goals remain
```
theorem a_rule_is_not_independent_of_itself :
    independent transferRule transferRule = false := by
…
```
Mentions: Hyperfields.Fields.Hypermechanics.independent, Hyperfields.Fields.Hypermechanics.transferRule
def Hyperfields.Fields.Hypermechanics.entry Hypermechanics explainer entry line 363 source
The canonical Hypermechanics record used by the unified portal.

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

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