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

Hyperorganization

[FRAME] The ordinal phase of a graph of reliance, and the arithmetic of amendment.

This is the Lean port of the core results in hyperoptimization's entrenchment and family modules. It carries three results:

The ordinal phase of a graph of reliance. A node's phase is 0 if it relies on nothing, one more than the largest phase among what it relies on, and ω if its reliance never bottoms out.
Protection, the weakest link. A rule's protection is the price of the cheapest procedure among the rules above it. This is Ross's paradox: a clause an ordinary majority can amend is protected by an ordinary majority, whatever the clause says of itself.
Authority height. The number of governors above a rule before the chain ends, or ω when it never does.

Every result is finite and mechanical. A graph over a carrier of known size is a list of edges, and the phase is computed by the same round-by-round peeling the Python source uses. So the compiler can check the result against a concrete graph.

What is not proved here, and cannot be, is any claim that the graphs these results are applied to are the right ones, that a citation is a dependence, or that a phase means anything outside the graph. The Python source makes the same refusals: a citation is evidence that one repository mentions another, not that it needs it. This port keeps the [FRAME] classification.

Imports (2)

Imported by 1 file

Hyperfields/AllFields.lean

inductive Hyperfields.Fields.Hyperorganization.Phase A phase of an organization line 53 source
The phase of a node: a natural number, or ω when the node's reliance never bottoms out.
The omega case is not a large number. It says the node lies on a cycle, or relies on something that does, and so has no finite rank.

A phase is a stage a rule passes through, and its ordinal position is what the protection and authority measures read.

no axioms what this means
```
inductive Phase where
…
```
def Hyperfields.Fields.Hyperorganization.phases The phase of a node in a graph of reliance line 72 source
The phase of every node of a graph of reliance.
The graph is given as a list of edges (source, target) read as source relies on target. The phase is computed by peeling rounds: round 0 takes every node whose dependencies were all taken in earlier rounds (which means a node that relies on nothing), round 1 takes the rest, and so on. A node never taken lies on a cycle or relies on one, and gets ω.
This is the same round-by-round computation the Python source uses, so the two agree by construction rather than by inspection.

A node that relies on nothing has phase 0, a node that relies on finite-phase nodes has one more than the largest of them, and a node whose reliance never bottoms out has no finite phase at all.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Prod, Fin, Hyperfields.Fields.Hyperorganization.Phase
Proof uses: Hyperfields.Finite.carrier, List.map, Prod.snd, List.filter, BEq.beq, Prod.fst, List.foldl, Bool.and, Bool.not, List.any, List.all, HAppend.hAppend, Prod.mk, List.nil, List.range, HAdd.hAdd, OfNat.ofNat, Hyperfields.Fields.Hyperorganization.phases.match_1, Option, List.find? and 3 more
9 instances, coercions and auxiliary constants left out.
```
def phases {n : Nat} (edges : List (Fin n × Fin n)) : List (Fin n × Phase) :=
…
```
Mentions: Hyperfields.Fields.Hyperorganization.Phase
def Hyperfields.Fields.Hyperorganization.phaseOf Read a rule's phase line 94 source
The phase of one node.

A rule the table does not place has no phase, which is nothing rather than a default stage.
Prerequisites: Hyperfields.Fields.Hyperorganization.Phase

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Prod, Fin, Hyperfields.Fields.Hyperorganization.Phase
Proof uses: Hyperfields.Fields.Hyperorganization.phaseOf.match_1, Option, List.find?, BEq.beq, Prod.fst, Hyperfields.Fields.Hyperorganization.phases, Prod.snd, Unit, Hyperfields.Fields.Hyperorganization.Phase.omega
4 instances, coercions and auxiliary constants left out.
```
def phaseOf {n : Nat} (edges : List (Fin n × Fin n)) (node : Fin n) : Phase :=
…
```
Mentions: Hyperfields.Fields.Hyperorganization.Phase
def Hyperfields.Fields.Hyperorganization.Phase.isFinite A phase is finite line 103 source
Whether a node's phase is finite.

A finite phase has a natural-number position, which is what separates it from a phase that has run past every finite stage.
Prerequisites: Hyperfields.Fields.Hyperorganization.Phase

no axioms what this means
Statement uses: Hyperfields.Fields.Hyperorganization.Phase, Bool
Proof uses: Hyperfields.Fields.Hyperorganization.instReprPhase.repr.match_1, Nat, Bool.true, Unit, Bool.false
```
def Phase.isFinite : Phase → Bool
  | .finite _ => true
  | .omega => false

/-!
## Governance: the arithmetic of amendment
-/

-- L4DEL: title: A rule and the rule that governs it
-- L4DEL: intuition: A rule carries the price of the procedure that changes it and names the rule that governs it, and the two together decide how hard the rule is to change.
/--
A rule: the price in bits of the procedure that changes it, and the rule
```
Mentions: Hyperfields.Fields.Hyperorganization.Phase
structure Hyperfields.Fields.Hyperorganization.Rule A rule and the rule that governs it line 120 source
A rule: the price in bits of the procedure that changes it, and the rule that governs it.
The governor is optional. A rule with no governor is unamendable, and that is what an apex is.

A rule carries the price of the procedure that changes it and names the rule that governs it, and the two together decide how hard the rule is to change.

no axioms what this means
Statement uses: Nat
```
structure Rule (n : Nat) where
…
```
def Hyperfields.Fields.Hyperorganization.chainAbove The rules above a rule, following governors line 141 source
The rules above a rule, in order, and whether the chain ended.
The chain ends when it reaches a rule nothing governs. It does not end when it returns to a rule it has already met, and that is exactly the distinction between a finite authority height and ω.
The walk is a bounded iteration rather than a recursive function. A governance chain in a set of n rules visits at most n distinct rules before it must either end or repeat, so n steps settle it. The bounded form is also what lets the compiler check the result: a recursive function would need a termination proof, and a bounded scan is decidable outright.

Protection and authority are both about the chain of governors above a rule, so that chain is the shared object both results compute from.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Hyperfields.Fields.Hyperorganization.Rule, Fin, Prod, Bool
Proof uses: Option, Hyperfields.Fields.Hyperorganization.chainAbove.match_1, List.find?, BEq.beq, Hyperfields.Fields.Hyperorganization.Rule.index, Hyperfields.Fields.Hyperorganization.Rule.governedBy, Unit, Option.none, Hyperfields.Fields.Hyperorganization.chainAbove.match_3, Hyperfields.Fields.Hyperorganization.chainAbove.match_2, Prod.mk, ite, Eq, List.any, Bool.true, Option.some, HAppend.hAppend, List.cons, List.nil, List.foldl and 6 more
10 instances, coercions and auxiliary constants left out.
```
def chainAbove {n : Nat} (rules : List (Rule n)) (start : Fin n) :
    List (Fin n) × Bool :=
…
```
Mentions: Hyperfields.Fields.Hyperorganization.Rule
def Hyperfields.Fields.Hyperorganization.protection How much a rule is protected line 182 source
The protection of a rule: the price of the cheapest procedure among the rules above it.
This is the weakest link in the chain of authority. To change a rule you may satisfy the procedure of its governor, or first change the governor and then change the rule for nothing. The cheapest way is therefore the cheapest procedure anywhere above the rule, which is what the minimum computes.
Around a cycle every member is above every other, so every member has the same protection: the cheapest procedure on the cycle. That is Ross's paradox, and it is a consequence of the formula rather than an extra assumption.

A rule is protected only as far as the weakest rule beneath it, so the measure is the minimum over its dependencies.
Prerequisites: Hyperfields.Fields.Hyperorganization.Phase

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Hyperfields.Fields.Hyperorganization.Rule, Fin, Option
Proof uses: Hyperfields.Fields.Hyperorganization.protection.match_2, Prod, Bool, Hyperfields.Fields.Hyperorganization.chainAbove, List.filterMap, Hyperfields.Fields.Hyperorganization.chainAbove.match_1, List.find?, BEq.beq, Hyperfields.Fields.Hyperorganization.Rule.index, Option.some, Hyperfields.Fields.Hyperorganization.Rule.price, Unit, Option.none, Hyperfields.Fields.Hyperorganization.protection.match_1, List.foldl, ite, LT.lt
6 instances, coercions and auxiliary constants left out.
```
def protection {n : Nat} (rules : List (Rule n)) (start : Fin n) : Option Nat :=
…
```
Mentions: Hyperfields.Fields.Hyperorganization.Rule
def Hyperfields.Fields.Hyperorganization.authorityHeight How high a rule stands line 204 source
The authority height of a rule: the number of governors above it before the chain ends.
The height is finite exactly when the chain ends at a rule that nothing governs. If every rule has a governor, then in a finite set every chain returns to itself and every height is ω: a constitution that obeys the no-apex rule has no finite rank for validity at all.

Authority height is the ordinal position a rule occupies, and a cycle gives every member the same height because none is above another.
Prerequisites: Hyperfields.Fields.Hyperorganization.Phase

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Hyperfields.Fields.Hyperorganization.Rule, Fin, Hyperfields.Fields.Hyperorganization.Phase
Proof uses: Hyperfields.Fields.Hyperorganization.protection.match_2, Prod, Bool, Hyperfields.Fields.Hyperorganization.chainAbove, ite, Eq, Bool.true, Hyperfields.Fields.Hyperorganization.Phase.finite, List.length, Hyperfields.Fields.Hyperorganization.Phase.omega
1 instances, coercions and auxiliary constants left out.
```
def authorityHeight {n : Nat} (rules : List (Rule n)) (start : Fin n) : Phase :=
…
```
Mentions: Hyperfields.Fields.Hyperorganization.Rule, Hyperfields.Fields.Hyperorganization.Phase
def Hyperfields.Fields.Hyperorganization.chainEdges A three-node chain of reliance line 220 source
A concrete graph: 0 relies on 1, 1 relies on 2, and 2 relies on nothing.
The phases are the obvious ones, and the compiler checks them.

A concrete graph lets the compiler check the phases against something a reader can see.

standard axioms: propext what this means
Statement uses: List, Prod, Fin, OfNat.ofNat, Nat
Proof uses: List.cons, Prod.mk, List.nil
4 instances, coercions and auxiliary constants left out.
```
def chainEdges : List (Fin 3 × Fin 3) := [(0, 1), (1, 2)]
```
def Hyperfields.Fields.Hyperorganization.cyclicEdges A graph with a cycle line 230 source
A concrete graph with a cycle: 0 relies on 1 and 1 relies on 0.
Neither node has a finite phase, because neither one's reliance bottoms out.

A cycle is the case where reliance never bottoms out, and the compiler has to be able to see that it does not.

standard axioms: propext what this means
Statement uses: List, Prod, Fin, OfNat.ofNat, Nat
Proof uses: List.cons, Prod.mk, List.nil
4 instances, coercions and auxiliary constants left out.
```
def cyclicEdges : List (Fin 2 × Fin 2) := [(0, 1), (1, 0)]
```
def Hyperfields.Fields.Hyperorganization.aboveCycleEdges A node that relies on a cycle line 241 source
A concrete graph where one node relies on a cycle.
Node 0 relies on 1, and 1 and 2 rely on each other. Node 0 is not itself on the cycle, but it relies on one, so its reliance never bottoms out either.

A node above a cycle never bottoms out, and the compiler has to be able to see the phase propagate.

standard axioms: propext what this means
Statement uses: List, Prod, Fin, OfNat.ofNat, Nat
Proof uses: List.cons, Prod.mk, List.nil
4 instances, coercions and auxiliary constants left out.
```
def aboveCycleEdges : List (Fin 3 × Fin 3) := [(0, 1), (1, 2), (2, 1)]
```
def Hyperfields.Fields.Hyperorganization.constitution A constitution with an apex line 251 source
A concrete constitution: rule 0 is governed by rule 1, rule 1 is governed by rule 2, and rule 2 is governed by nothing.
Rule 2 is the apex. The authority heights are 2, 1, and 0.

A constitution with an unamendable rule at the top has finite authority heights, and the compiler can check the exact numbers.

standard axioms: propext what this means
Statement uses: List, Hyperfields.Fields.Hyperorganization.Rule, OfNat.ofNat, Nat
Proof uses: List.cons, Hyperfields.Fields.Hyperorganization.Rule.mk, Fin, Option.some, Option.none, List.nil
4 instances, coercions and auxiliary constants left out.
```
def constitution : List (Rule 3) := [
…
```
Mentions: Hyperfields.Fields.Hyperorganization.Rule
def Hyperfields.Fields.Hyperorganization.cyclicConstitution A constitution with a cycle of rules line 266 source
A concrete constitution with a cycle: rule 0 is governed by rule 1 and rule 1 is governed by rule 0.
Neither rule has a finite authority height, and both have the same protection, because around a cycle every member is above every other.

A cycle of rules has no apex, so every height is omega, and that is the case Ross's paradox is about.

standard axioms: propext what this means
Statement uses: List, Hyperfields.Fields.Hyperorganization.Rule, OfNat.ofNat, Nat
Proof uses: List.cons, Hyperfields.Fields.Hyperorganization.Rule.mk, Fin, Option.some, List.nil
4 instances, coercions and auxiliary constants left out.
```
def cyclicConstitution : List (Rule 2) := [
…
```
Mentions: Hyperfields.Fields.Hyperorganization.Rule
theorem Hyperfields.Fields.Hyperorganization.chain_phases The chain graph's phases line 274 source
The chain graph has phases 2, 1, and 0.

The phase of a node in a chain is its distance from the node that relies on nothing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Prod, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperorganization.Phase, Hyperfields.Fields.Hyperorganization.phases, Hyperfields.Fields.Hyperorganization.chainEdges, List.cons, Prod.mk, Hyperfields.Fields.Hyperorganization.Phase.finite, List.nil
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 276
  before
```
⊢ phases chainEdges = [(0, Phase.finite 2), (1, Phase.finite 1), (2, Phase.finite 0)]
```
  after
  no goals remain
```
theorem chain_phases :
    phases chainEdges = [(0, .finite 2), (1, .finite 1), (2, .finite 0)] := by
…
```
Mentions: Hyperfields.Fields.Hyperorganization.phases, Hyperfields.Fields.Hyperorganization.chainEdges
theorem Hyperfields.Fields.Hyperorganization.cyclic_phases_are_omega A cycle has no finite phase line 281 source
Neither node of the cyclic graph has a finite phase.

Reliance that goes round in a circle never bottoms out, so the phase is omega rather than a large number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Prod, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperorganization.Phase, Hyperfields.Fields.Hyperorganization.phases, Hyperfields.Fields.Hyperorganization.cyclicEdges, List.cons, Prod.mk, Hyperfields.Fields.Hyperorganization.Phase.omega, List.nil
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 283
  before
```
⊢ phases cyclicEdges = [(0, Phase.omega), (1, Phase.omega)]
```
  after
  no goals remain
```
theorem cyclic_phases_are_omega :
    phases cyclicEdges = [(0, .omega), (1, .omega)] := by
…
```
Mentions: Hyperfields.Fields.Hyperorganization.phases, Hyperfields.Fields.Hyperorganization.cyclicEdges
theorem Hyperfields.Fields.Hyperorganization.a_node_above_a_cycle_is_omega A node that relies on a cycle has no finite phase either line 293 source
The node that relies on a cycle has no finite phase.
This is the propagation the Python source describes: a node never taken relies on a cycle, and so does everything that relies on it.

The phase of omega spreads to everything that relies on it, so a node downstream of a cycle is also omega.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Prod, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperorganization.Phase, Hyperfields.Fields.Hyperorganization.phases, Hyperfields.Fields.Hyperorganization.aboveCycleEdges, List.cons, Prod.mk, Hyperfields.Fields.Hyperorganization.Phase.omega, List.nil
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 295
  before
```
⊢ phases aboveCycleEdges = [(0, Phase.omega), (1, Phase.omega), (2, Phase.omega)]
```
  after
  no goals remain
```
theorem a_node_above_a_cycle_is_omega :
    phases aboveCycleEdges = [(0, .omega), (1, .omega), (2, .omega)] := by
…
```
Mentions: Hyperfields.Fields.Hyperorganization.phases, Hyperfields.Fields.Hyperorganization.aboveCycleEdges
theorem Hyperfields.Fields.Hyperorganization.constitution_authority_heights The authority heights of a constitution with an apex line 300 source
The constitution's authority heights are 2, 1, and 0.

The height of a rule is the number of governors above it before the chain ends at the apex.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Prod, Hyperfields.Fields.Hyperorganization.Phase, Prod.mk, Hyperfields.Fields.Hyperorganization.authorityHeight, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperorganization.constitution, Fin, Hyperfields.Fields.Hyperorganization.Phase.finite
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 304
  before
```
⊢ (authorityHeight constitution 0, authorityHeight constitution 1, authorityHeight constitution 2) =
    (Phase.finite 2, Phase.finite 1, Phase.finite 0)
```
  after
  no goals remain
```
theorem constitution_authority_heights :
    (authorityHeight constitution 0, authorityHeight constitution 1,
      authorityHeight constitution 2) =
      (.finite 2, .finite 1, .finite 0) := by
…
```
Mentions: Hyperfields.Fields.Hyperorganization.authorityHeight, Hyperfields.Fields.Hyperorganization.constitution
theorem Hyperfields.Fields.Hyperorganization.cyclic_authority_heights_are_omega A cycle of rules has no finite authority height line 309 source
Neither rule of the cyclic constitution has a finite authority height.

A constitution with no apex has no finite rank for validity at all, and the height of every rule is omega.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Prod, Hyperfields.Fields.Hyperorganization.Phase, Prod.mk, Hyperfields.Fields.Hyperorganization.authorityHeight, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperorganization.cyclicConstitution, Fin, Hyperfields.Fields.Hyperorganization.Phase.omega
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 312
  before
```
⊢ (authorityHeight cyclicConstitution 0, authorityHeight cyclicConstitution 1) = (Phase.omega, Phase.omega)
```
  after
  no goals remain
```
theorem cyclic_authority_heights_are_omega :
    (authorityHeight cyclicConstitution 0, authorityHeight cyclicConstitution 1) =
      (.omega, .omega) := by
…
```
Mentions: Hyperfields.Fields.Hyperorganization.authorityHeight, Hyperfields.Fields.Hyperorganization.cyclicConstitution
theorem Hyperfields.Fields.Hyperorganization.protection_is_the_weakest_link Protection is the weakest link line 324 source
The protection of rule 0 is 3, not 5.
Rule 0 is governed by rule 1, whose procedure costs 3. Satisfying rule 1's procedure is cheaper than satisfying rule 2's, which costs 9, so the weakest link is what protects rule 0. This is the whole content of the protection formula.

The cheapest way to change a rule is the cheapest procedure among the rules above it, so the weakest link governs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Option, Nat, Hyperfields.Fields.Hyperorganization.protection, OfNat.ofNat, Hyperfields.Fields.Hyperorganization.constitution, Fin, Option.some
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 326
  before
```
⊢ protection constitution 0 = some 3
```
  after
  no goals remain
```
theorem protection_is_the_weakest_link :
    protection constitution 0 = some 3 := by
…
```
Mentions: Hyperfields.Fields.Hyperorganization.protection, Hyperfields.Fields.Hyperorganization.constitution
theorem Hyperfields.Fields.Hyperorganization.the_apex_protects_the_rule_beneath_it An apex protects the rules beneath it line 331 source
The protection of rule 1 is 9, the price of the apex's procedure.

The apex is the only rule above the top of the chain, so its procedure price is the protection of everything beneath.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Option, Nat, Hyperfields.Fields.Hyperorganization.protection, OfNat.ofNat, Hyperfields.Fields.Hyperorganization.constitution, Fin, Option.some
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 333
  before
```
⊢ protection constitution 1 = some 9
```
  after
  no goals remain
```
theorem the_apex_protects_the_rule_beneath_it :
    protection constitution 1 = some 9 := by
…
```
Mentions: Hyperfields.Fields.Hyperorganization.protection, Hyperfields.Fields.Hyperorganization.constitution
theorem Hyperfields.Fields.Hyperorganization.an_ungoverned_rule_has_no_protection An ungoverned rule has no protection line 344 source
The apex's protection is absent rather than infinite.
The Python source reports inf for this case. Here the absence is represented by none, which is a stronger statement: there is no procedure that changes it, not merely an unboundedly expensive one.

A rule nothing governs cannot be changed through any procedure, so there is no price to report.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Option, Nat, Hyperfields.Fields.Hyperorganization.protection, OfNat.ofNat, Hyperfields.Fields.Hyperorganization.constitution, Fin, Option.none
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 346
  before
```
⊢ protection constitution 2 = none
```
  after
  no goals remain
```
theorem an_ungoverned_rule_has_no_protection :
    protection constitution 2 = none := by
…
```
Mentions: Hyperfields.Fields.Hyperorganization.protection, Hyperfields.Fields.Hyperorganization.constitution
theorem Hyperfields.Fields.Hyperorganization.a_cycle_gives_every_member_the_same_protection A cycle gives every member the same protection line 358 source
Both rules of the cyclic constitution have protection 4.
The cycle's procedures cost 4 and 7, and around a cycle every member is above every other, so the cheaper one protects both. This is Ross's paradox: an entrenched clause is protected by whatever the cheapest procedure on the cycle happens to be.

Around a cycle every member is above every other, so the cheapest procedure on the cycle protects them all equally.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Prod, Option, Nat, Prod.mk, Hyperfields.Fields.Hyperorganization.protection, OfNat.ofNat, Hyperfields.Fields.Hyperorganization.cyclicConstitution, Fin, Option.some
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
9 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 361
  before
```
⊢ (protection cyclicConstitution 0, protection cyclicConstitution 1) = (some 4, some 4)
```
  after
  no goals remain
```
theorem a_cycle_gives_every_member_the_same_protection :
    (protection cyclicConstitution 0, protection cyclicConstitution 1) =
      (some 4, some 4) := by
…
```
Mentions: Hyperfields.Fields.Hyperorganization.protection, Hyperfields.Fields.Hyperorganization.cyclicConstitution
def Hyperfields.Fields.Hyperorganization.entry Hyperorganization explainer entry line 371 source
The canonical Hyperorganization record used by the unified portal.

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

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.hyperorganization
```
def entry : Hyperfields.Entry := Hyperfields.hyperorganization
…
```
Mentions: Hyperfields.Entry, Hyperfields.hyperorganization