OAI/Combinatorics/HoneycombChords/Bridges.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Strict honeycomb bridges from a fixed bottom port, with critical mass summed over compatible top ports. The height-zero mass has the renewal normalization one.

The convention follows the finite inputs in Critical honeycomb chords with prescribed boundary endpoints.

  1. def OAI.CriticalHoneycomb.strip line 14

    Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:58 (same declaration text).

  2. def OAI.CriticalHoneycomb.StrictBridge line 15

    Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:59 (same declaration text).

  3. def OAI.CriticalHoneycomb.bridgeMass line 18

    Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:62 (same declaration text).