`Hyperfields/Bridges.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.

FORM: Used in an explanation or its source, but not expanded by this annotation. Follow its linked source.
JSON: Used in an explanation or its source, but not expanded by this annotation. Follow its linked source.
L4DEL: Lean4 Domain Explanation Language

19 declarations, 0 contain sorry, 0 axioms

Cross-field integration bridges, as typed declarations

Hyperstratum's integration-registry.json declares three bridges between fields. Each one is a declaration of intent, not a proven correspondence, and each carries an explicit OPEN status.

This module encodes those declarations in Lean. The point is not to prove any of them. The point is to make the declarations typed, so that the properties hyperstratum's own checker enforces are properties of the data rather than properties of a Python function that has to be run.

Three refusals are preserved exactly, because losing any of them would turn a declaration into a claim:

A bridge whose target is classified FORM cannot be certified here. A declaration checker does not certify a native closed account; that needs an independent derivation elsewhere.
A bridge cannot self-certify. Its status is OPEN or UNKNOWN and nothing here promotes it to a closed state.
A bridge needs explicit content. Every mapping carries a meaning, and the preserves, excludes, and obligations lists are nonempty.

The third refusal is the one that keeps the declarations honest. A bridge with an empty "preserves" list would look like a correspondence and carry none of the content that makes it meaningful.

Imports (1)

Imported by 2 files

inductive Hyperfields.Bridges.BridgeStatus The declared status of a bridge line 50 source
The declared status of a bridge.
There is deliberately no member for a certified bridge. A correspondence that has been proved does not become one by a status change in a declaration; it needs an independent derivation.

A bridge is either still open or its own declaration is unsettled; neither is a closed correspondence.

no axioms what this means
```
inductive BridgeStatus where
…
```
inductive Hyperfields.Bridges.BridgeRelation The role a bridge claims to play line 58 source
The role a bridge claims to play.

A bridge must state its role, because "these two fields correspond" and "these two fields are used together" are different claims.

no axioms what this means
```
inductive BridgeRelation where
…
```
inductive Hyperfields.Bridges.FieldClass The classification of a bridge endpoint line 73 source
The classification of a bridge endpoint.
openClass renders to the published string OPEN; the identifier differs only because open is a Lean keyword.

A native closed account, a declared incomplete account, an unsettled account, and a multi-level candidate are four different things.

no axioms what this means
```
inductive FieldClass where
…
```
structure Hyperfields.Bridges.Mapping One named correspondence line 88 source
One named correspondence between a source concept and a target concept.
The meaning field is not commentary. It is the part that says what the correspondence does and does not license.

A mapping between two concepts must carry the meaning it is meant to preserve, or it is an uninterpreted pair of names.

no axioms what this means
```
structure Mapping where
…
```
structure Hyperfields.Bridges.Bridge One declared cross-field correspondence line 102 source
One declared cross-field correspondence.
The status is part of the record rather than an inference, so a reader can see at a glance that no correspondence has been established.

A bridge is a declaration with explicit endpoints, an explicit status, and explicit content; none of it is inferred.

no axioms what this means
```
structure Bridge where
…
```
def Hyperfields.Bridges.Bridge.wellShaped A declaration checker cannot certify a native target line 132 source
Whether a bridge is well-shaped as a declaration.
A bridge is well-shaped when it has two distinct endpoints, a target that is not a native FORM account, at least one mapping with a nonempty meaning, and nonempty preserves, excludes, and obligations lists.
This is the conjunction of hyperstratum's three refusals, expressed as one predicate on the record so it can be checked by decide over the finite bridge list.

A `FORM` endpoint is a closed native account, and a declaration has no standing to certify one.

no axioms what this means
Statement uses: Hyperfields.Bridges.Bridge, Bool
Proof uses: Bool.and, bne, String, Hyperfields.Bridges.Bridge.source, Hyperfields.Bridges.Bridge.target, Hyperfields.Bridges.FieldClass, Hyperfields.Bridges.Bridge.targetClass, Hyperfields.Bridges.FieldClass.form, Bool.not, List.isEmpty, Hyperfields.Bridges.Mapping, Hyperfields.Bridges.Bridge.mappings, Hyperfields.Bridges.Bridge.preserves, Hyperfields.Bridges.Bridge.excludes, Hyperfields.Bridges.Bridge.obligations, List.all, String.isEmpty, Hyperfields.Bridges.Mapping.source, Hyperfields.Bridges.Mapping.target, Hyperfields.Bridges.Mapping.meaning
3 instances, coercions and auxiliary constants left out.
```
def Bridge.wellShaped (bridge : Bridge) : Bool :=
…
```
Mentions: Hyperfields.Bridges.Bridge
def Hyperfields.Bridges.Bridge.isOpen A bridge is still an open declaration line 151 source
Whether a bridge is still an open declaration.
A bridge that was UNKNOWN is unsettled; a bridge that is OPEN is declared but not established. Neither is a correspondence that has been proved.

A declaration cannot certify itself, so every bridge keeps an explicit status and none of them is closed.

no axioms what this means
Statement uses: Hyperfields.Bridges.Bridge, Bool
Proof uses: BEq.beq, Hyperfields.Bridges.BridgeStatus, Hyperfields.Bridges.Bridge.status, Hyperfields.Bridges.BridgeStatus.declaredOpen
1 instances, coercions and auxiliary constants left out.
```
def Bridge.isOpen (bridge : Bridge) : Bool :=
…
```
Mentions: Hyperfields.Bridges.Bridge
def Hyperfields.Bridges.declaredBridges The declared bridges line 170 source
The three declared cross-field bridges.
Every one of them is OPEN, and every one of them has a FRAME target, so no declaration here is a claim of a closed correspondence.

Each bridge names what it maps, what it preserves, what it refuses, and what it still owes.

no axioms what this means
Statement uses: List, Hyperfields.Bridges.Bridge
Proof uses: List.cons, Hyperfields.Bridges.Bridge.mk, Hyperfields.Bridges.BridgeRelation.interpretation, Hyperfields.Bridges.FieldClass.frame, Hyperfields.Bridges.BridgeStatus.declaredOpen, Hyperfields.Bridges.Mapping, Hyperfields.Bridges.Mapping.mk, List.nil, String, Hyperfields.Bridges.BridgeRelation.application
```
def declaredBridges : List Bridge := [
…
```
Mentions: Hyperfields.Bridges.Bridge
theorem Hyperfields.Bridges.declared_bridges_are_well_shaped Every bridge is well shaped line 289 source
Every declared bridge clears the declaration contract.

A bridge with an empty preserves list would look like a correspondence and carry none of the content that makes it one, so each is checked to have all three lists.
Prerequisites: Hyperfields.Bridges.declaredBridges, Hyperfields.Bridges.Bridge.wellShaped

no axioms what this means
Statement uses: Eq, List, Hyperfields.Bridges.Bridge, List.filter, Bool.not, Hyperfields.Bridges.Bridge.wellShaped, Hyperfields.Bridges.declaredBridges, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
1 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 291
  before
```
⊢ List.filter (fun bridge => !bridge.wellShaped) declaredBridges = []
```
  after
  no goals remain
```
theorem declared_bridges_are_well_shaped :
    declaredBridges.filter (fun bridge => !bridge.wellShaped) = [] := by
…
```
theorem Hyperfields.Bridges.no_declared_bridge_targets_form No declared bridge targets a native closed account line 298 source
No declared bridge has a FORM target.

A declaration has no standing to certify a `FORM` account, so none of the three may have one as a target.

no axioms what this means
Statement uses: Eq, List, Hyperfields.Bridges.Bridge, List.filter, BEq.beq, Hyperfields.Bridges.FieldClass, Hyperfields.Bridges.Bridge.targetClass, Hyperfields.Bridges.FieldClass.form, Hyperfields.Bridges.declaredBridges, List.nil
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 300
  before
```
⊢ List.filter (fun bridge => bridge.targetClass == FieldClass.form) declaredBridges = []
```
  after
  no goals remain
```
theorem no_declared_bridge_targets_form :
    declaredBridges.filter (fun bridge => bridge.targetClass == .form) = [] := by
…
```
theorem Hyperfields.Bridges.no_declared_bridge_is_closed No declared bridge is closed line 311 source
No declared bridge is a closed correspondence.
The BridgeStatus type has no closed member, and every declared bridge carries the OPEN status, so this is a statement about the data and about the vocabulary together.

A correspondence that has been proved needs an independent derivation, not a status change in a declaration.

no axioms what this means
Statement uses: Eq, List, Hyperfields.Bridges.Bridge, List.filter, Bool.not, Hyperfields.Bridges.Bridge.isOpen, Hyperfields.Bridges.declaredBridges, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
1 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 313
  before
```
⊢ List.filter (fun bridge => !bridge.isOpen) declaredBridges = []
```
  after
  no goals remain
```
theorem no_declared_bridge_is_closed :
    declaredBridges.filter (fun bridge => !bridge.isOpen) = [] := by
…
```
theorem Hyperfields.Bridges.there_are_three_declared_bridges There are three declared bridges line 318 source
The integration registry declares exactly three bridges.

The list is explicit, so Lean can reduce its length exactly.

no axioms what this means
Statement uses: Eq, Nat, List.length, Hyperfields.Bridges.Bridge, Hyperfields.Bridges.declaredBridges, OfNat.ofNat
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 319
  before
```
⊢ declaredBridges.length = 3
```
  after
  no goals remain
```
theorem there_are_three_declared_bridges : declaredBridges.length = 3 := by
…
```
theorem Hyperfields.Bridges.declared_bridges_join_distinct_fields The declared bridges join distinct fields line 324 source
No declared bridge joins a field to itself.

A bridge needs two fields, so no declared bridge may begin and end at the same field.

no axioms what this means
Statement uses: Eq, List, Hyperfields.Bridges.Bridge, List.filter, BEq.beq, String, Hyperfields.Bridges.Bridge.source, Hyperfields.Bridges.Bridge.target, Hyperfields.Bridges.declaredBridges, List.nil
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 326
  before
```
⊢ List.filter (fun bridge => bridge.source == bridge.target) declaredBridges = []
```
  after
  no goals remain
```
theorem declared_bridges_join_distinct_fields :
    declaredBridges.filter (fun bridge => bridge.source == bridge.target) = [] := by
…
```
theorem Hyperfields.Bridges.every_bridge_carries_an_obligation Every declared bridge names an open obligation line 331 source
Every declared bridge carries at least one outstanding obligation.

A bridge that owes nothing has not said what it is waiting for, so each one carries at least one outstanding obligation.

no axioms what this means
Statement uses: Eq, Bool, List.all, Hyperfields.Bridges.Bridge, Hyperfields.Bridges.declaredBridges, Bool.not, List.isEmpty, String, Hyperfields.Bridges.Bridge.obligations, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
1 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 333
  before
```
⊢ (declaredBridges.all fun bridge => !bridge.obligations.isEmpty) = true
```
  after
  no goals remain
```
theorem every_bridge_carries_an_obligation :
    declaredBridges.all (fun bridge => !bridge.obligations.isEmpty) = true := by
…
```
def Hyperfields.Bridges.BridgeStatus.string The published string of a bridge status line 346 source
The published string of a bridge status.

The published vocabulary is fixed, so each status renders to exactly one string.

no axioms what this means
Statement uses: Hyperfields.Bridges.BridgeStatus, String
Proof uses: Hyperfields.Bridges.instReprBridgeStatus.repr.match_1, Unit
```
def BridgeStatus.string : BridgeStatus → String
  | .declaredOpen => "OPEN"
  | .unknown => "UNKNOWN"

-- L4DEL: title: The published string of a bridge relation
-- L4DEL: intuition: The published vocabulary is fixed, so each relation renders to exactly one string.
/-- The published string of a bridge relation. -/
```
Mentions: Hyperfields.Bridges.BridgeStatus

def Hyperfields.Bridges.BridgeRelation.string The published string of a bridge relation line 353 source

The published string of a bridge relation.

The published vocabulary is fixed, so each relation renders to exactly one string.

no axioms what this means

Statement uses: Hyperfields.Bridges.BridgeRelation, String

Proof uses: Hyperfields.Bridges.instReprBridgeRelation.repr.match_1, Unit

def BridgeRelation.string : BridgeRelation → String
  | .interpretation => "interpretation"
  | .transport => "transport"
  | .application => "application"
  | .representation => "representation"

-- L4DEL: title: The published string of a field classification
-- L4DEL: intuition: The published vocabulary is fixed, so each classification renders to exactly one string.
/-- The published string of a field classification. -/

Mentions: Hyperfields.Bridges.BridgeRelation

def Hyperfields.Bridges.FieldClass.string The published string of a field classification line 362 source

The published string of a field classification.

The published vocabulary is fixed, so each classification renders to exactly one string.

no axioms what this means

Statement uses: Hyperfields.Bridges.FieldClass, String

Proof uses: Hyperfields.Bridges.instReprFieldClass.repr.match_1, Unit

def FieldClass.string : FieldClass → String
  | .form => "FORM"
  | .frame => "FRAME"
  | .openClass => "OPEN"
  | .hyper => "HYPER"

-- L4DEL: title: Render one bridge as a JSON object
-- L4DEL: intuition: A consumer must be able to see the status, the content, and the obligations without reconstructing them.
/--
Render one bridge as a JSON object.

The status is published as data, never inferred. A consumer that reads this

Mentions: Hyperfields.Bridges.FieldClass

def Hyperfields.Bridges.Bridge.render Render one bridge as a JSON object line 376 source
Render one bridge as a JSON object.
The status is published as data, never inferred. A consumer that reads this file cannot mistake a declared bridge for a proved correspondence.

A consumer must be able to see the status, the content, and the obligations without reconstructing them.

standard axioms: propext what this means
Statement uses: Hyperfields.Bridges.Bridge, String
Proof uses: HAppend.hAppend, List, String.intercalate, List.map, Hyperfields.Bridges.Mapping, Prod, List.cons, Prod.mk, Hyperfields.Bridges.Mapping.source, Hyperfields.Bridges.Mapping.target, Hyperfields.Bridges.Mapping.meaning, List.nil, Hyperfields.Bridges.Bridge.render.match_1, Hyperfields.Bridges.Bridge.source, Hyperfields.Bridges.Bridge.target, Hyperfields.Bridges.BridgeRelation.string, Hyperfields.Bridges.Bridge.relation, Hyperfields.Bridges.FieldClass.string, Hyperfields.Bridges.Bridge.sourceClass, Hyperfields.Bridges.Bridge.targetClass and 6 more
2 instances, coercions and auxiliary constants left out.
```
def Bridge.render (bridge : Bridge) : String :=
…
```
Mentions: Hyperfields.Bridges.Bridge
def Hyperfields.Bridges.renderBridges Render the whole bridge record line 408 source
Render the whole bridge record.

The bridge record is a single document, so a consumer reads it in one place rather than assembling it from parts.

standard axioms: propext what this means
Statement uses: String
Proof uses: HAppend.hAppend, String.intercalate, List.map, Hyperfields.Bridges.Bridge, Hyperfields.Bridges.Bridge.render, Hyperfields.Bridges.declaredBridges
2 instances, coercions and auxiliary constants left out.
```
def renderBridges : String :=
…
```