

STATIC CONSTRAINT PROFILE -- problem windtunnel-topo
generated by tech/constraint-profile.lisp -- NEVER HAND-EDITED


MC  MECHANIC COVERAGE  [grade 1]
--------------------------------------------------------------

  public technologies spliced (8): 8 covered, 0 UNCOVERED
    beam-relay        COVERED    contract (also S6 RC; RL scenario)
    gate              COVERED    extractors S1 S3 S4
    plate             COVERED    extractors S1 S2 T6
    recorder          COVERED    contract (also S2 RO CP)
    step              COVERED    extractors S2 T6; boarding a fixed floor blower in the floor-blower contract, a gears-mounted fan in the floor-gears contract
    visibility        COVERED    infrastructure -- line of sight; read by S6
    walkability       COVERED    infrastructure -- derives walk-kind facts; read by S3
    wall-blower       COVERED    contract (also S1 S3 RC CC)

  UNCOVERED (0):
    READING: UNCOVERED means no static contract is declared for that technology.  The coverage gate (Problem-Solving Guide, Phase 0 step 2) requires a hand contract in the Briefing, or a component, before going on.  COVERED by extractors or infrastructure means the named components carry its static consequences; it is not a contract.

  contract beam-relay
    controls  the derived COLOR of every relay (connector or repeater), recomputed in each propagation after the crossing set, and each receiver's ACTIVE fact (RECORDING-ACTIVE in the recording view)
    moves     connectors only: PICKUP-CONNECTOR lifts one and deletes every PAIRED fact it owns and every one naming it; PICKUP-CONNECTOR-RETAINING-PAIRINGS keeps them, but a held connector has no location and neither receives nor sends a beam; PUT-CONNECTOR places without pairing; CONNECT-CONNECTOR places the held connector at a location the agent reaches and stores 1 to *max-connector-pairings* outgoing PAIRED facts, to termini structurally visible from any location the agent can walk to, never to a connector at the placement location
    requires  lighting runs in propagation layers from every transmitter (layer 0). A relay settles in the first layer in which any clear link from a lit source reaches it: one hue lights it; two or more hues in that layer leave it dark, and a dark relay feeds nothing; a hue arriving in a later layer is ignored. A connector is also dark when a connector at its location is already lit. Clear link: a stored PAIRED fact in either direction (COUPLED for fixed apparatus), a live sightline in the reading view, and no cut by an active crossing (physical view only). Pairings persist while their beam is blocked or cut; only pickup clears them. Capacity counts a connector's outgoing pairings; incoming links are unlimited. A receiver is reached only by a relay of its hue whose own outgoing pairing (or coupling) names it, visible and uncut; beam-direct may reach it independently. CONNECT-CONNECTOR needs no lit connector of the same recorder layer at the placement location. Layers are propagation order, not travel time or action order
    capacity: 2 outgoing pairings per connector (*max-connector-pairings*); incoming links unlimited
    transmitters by hue: blue transmitter1
    receivers by hue: blue receiver1
    connectors (2): connector1, connector1*
    repeaters (1):
      repeater1: coupled from none, coupled to none
    start-state links (0 stored pairings): none
    direct feeds by RC station (1 with a visible transmitter; 0 COMPETING HUES), each transmitter with the gates it requires open:
      location1@1: blue transmitter1 requires open gate1
    Pairing one connector to two hues settles it in layer 1 with a CONFLICT (dark, feeds nothing). A direct transmitter link reaches a connector in layer 1, ahead of any relayed hue, so a relayed hue lights it only while that direct link is unpaired, blocked or cut. Separately possible per-hue routes are not claimed to compose; a joint arrangement needs REPORT-RELAY-LIGHTING-SCENARIO.

  contract recorder
    controls  the recording session, not a device (no CONTROLS entry): START-RECORDER opens a cycle -- a live agent at a recorder's position, empty-handed, no ghost left from a closed cycle, within *max-recorder-cycles*; STOP-RECORDER (by a ghost agent) or CANCEL-PLAYBACK (by a live agent) closes it
    moves     at START-RECORDER each live mobile object's ghost appears where the live one is, with its holding, ON and pairing state; while the cycle is open live and ghost bodies both act, each manipulating only its own side's objects; closing removes every ghost and every fact naming one, and rebuilds the recording view from live state
    requires  STOP: every ghost agent at a recorder's position and empty-handed, and no HOLDING or ON between a live and a ghost object; CANCEL: the live agent at a recorder's position and empty-handed, ghost dependencies discarded.  Devices and plates are read in each object's own view: physical counts every body present, ghosts included; recording counts ghost occupants only.  A live body may stand on a ghost-held tray; a ghost never uses a live support.  A closed cycle must leave persistent progress.  Initialization rejects beam crossings, floor gears, angled blowers, threats, receiver-controlled blower drives and movable wall-fan copies
    cycles allowed  1 (*max-recorder-cycles*)
    live -> ghost (2): agent1 -> agent1*, connector1 -> connector1*
    recorder1  at location1

  contract wall-blower
    controls  its CONTROLS aggregate (uncontrolled default on), unless jammed; a fan must be present. Live objects read TURNING, ghosts read RECORDING-TURNING; the two views need not agree
    moves     horizontal sweep from HAS-POSITION to AIMED-AT when base < stream <= top; detach from support, relocate the occupant and its stack, with held cargo following its agent; land on a flush-floor support or ground. Pairing and jamming facts persist, effects recomputed at the destination
    requires  own-view fan activity and body contact with the stream; fans are never swept. Wall-mounted fans have no HAS-LOCATION and are not standing supports. Walk-kind clauses naming the drive require it inactive in the actor's view. Directly unswept bodies may still move with swept supports; transport cycles must converge
    blower1  fixed complete fixture
      horizontal   location3 -> location6
      stream       elevation 1; width 4; base < stream <= top
      control      ((plate1)) normal, separately in each environmental view


S0  TYPE EXTENT CENSUS  [grade 1]
--------------------------------------------------------------

  type extents (59 types)
    agent  2  authored
    angled-blower  0  optional  EMPTY
    angled-blower+angled-gears+floor-blower+floor-gears+wall-blower+wall-gears  1  synthesized  SINGLETON  components floor-gears wall-gears angled-gears floor-blower wall-blower angled-blower
    angled-blower+floor-blower  0  synthesized  EMPTY  components floor-blower angled-blower
    angled-gears  0  optional  EMPTY
    beam-blocker  4  authored  components agent box jammer connector
    beam-node  9  authored  components transmitter receiver floor-repeater wall-repeater location
    blower  1  authored  SINGLETON  components floor-blower wall-blower angled-blower
    box  0  optional  EMPTY
    cargo  2  authored  components box jammer connector fan tray
    connector  2  authored
    edge  0  optional  EMPTY
    edge+wall  2  synthesized  components wall edge
    elevated-object  14  authored  components location gate screen wall edge transmitter receiver gun switch wall-gears wall-blower floor-repeater wall-repeater
    fan  0  optional  EMPTY
    fixed-beam-sink  2  authored  components floor-repeater wall-repeater receiver
    fixed-beam-source  2  authored  components transmitter floor-repeater wall-repeater
    fixed-position-object  3  authored  components pressure-plate toggle-plate ladder floor-gears wall-gears angled-gears floor-blower wall-blower angled-blower recorder
    floor-blower  0  optional  EMPTY
    floor-gears  0  optional  EMPTY
    floor-repeater  1  authored  SINGLETON
    gate  2  authored
    gate+screen  2  synthesized  components gate screen
    gears  0  authored  EMPTY  components floor-gears wall-gears angled-gears
    gun  0  optional  EMPTY
    heighted-object  9  authored  components box gate agent screen wall edge jammer connector floor-repeater wall-repeater
    hue  1  authored  SINGLETON
    jammer  0  optional  EMPTY
    ladder  0  optional  EMPTY
    location  6  authored
    los-endpoint  9  authored  components transmitter receiver floor-repeater wall-repeater gun location
    mobile-object  4  authored  components agent box jammer connector fan tray
    mode  2  authored
    plate  1  authored  SINGLETON  components pressure-plate toggle-plate
    pressure-plate  0  optional  EMPTY
    reach-target  6  authored  components location switch
    receiver  1  authored  SINGLETON
    recorder  1  authored  SINGLETON
    recording-blower-drive  1  authored  SINGLETON  components floor-blower wall-gears wall-blower
    relay  3  authored  components connector floor-repeater wall-repeater
    repeater  1  authored  SINGLETON  components floor-repeater wall-repeater
    screen  0  optional  EMPTY
    steppable-object  1  authored  SINGLETON  components pressure-plate toggle-plate fan floor-blower angled-blower
    support  1  authored  SINGLETON  components pressure-plate toggle-plate box fan tray floor-blower angled-blower
    support-occupant  4  authored  components agent box jammer connector fan tray
    switch  0  optional  EMPTY
    terminus  5  authored  components transmitter receiver connector floor-repeater wall-repeater
    threat  0  authored  EMPTY  components gun
    toggle-plate  1  authored  SINGLETON
    transmitter  1  authored  SINGLETON
    tray  0  optional  EMPTY
    vertical-object  18  authored  components location agent box connector jammer tray fan gate screen wall edge floor-repeater wall-repeater transmitter receiver gun switch pressure-plate toggle-plate floor-blower angled-blower
    visibility-object  11  authored  components gate transmitter receiver floor-repeater wall-repeater gun location
    wall  2  authored
    wall-blower  1  authored  SINGLETON
    wall-blower+wall-gears  1  synthesized  SINGLETON  components wall-gears wall-blower
    wall-gears  0  optional  EMPTY
    wall-repeater  0  optional  EMPTY
    window  0  optional  EMPTY

  empty types (20)
    angled-blower  optional
    angled-blower+floor-blower  synthesized  alias over floor-blower angled-blower
    angled-gears  optional
    box  optional
    edge  optional
    fan  optional
    floor-blower  optional
    floor-gears  optional
    gears  authored  alias over floor-gears wall-gears angled-gears
    gun  optional
    jammer  optional
    ladder  optional
    pressure-plate  optional
    screen  optional
    switch  optional
    threat  authored  alias over gun
    tray  optional
    wall-gears  optional
    wall-repeater  optional
    window  optional

  singleton types (15)
    angled-blower+angled-gears+floor-blower+floor-gears+wall-blower+wall-gears == blower1  synthesized
    blower == blower1  authored
    floor-repeater == repeater1  authored
    hue == blue  authored
    plate == plate1  authored
    receiver == receiver1  authored
    recorder == recorder1  authored
    recording-blower-drive == blower1  authored
    repeater == repeater1  authored
    steppable-object == plate1  authored
    support == plate1  authored
    toggle-plate == plate1  authored
    transmitter == transmitter1  authored
    wall-blower == blower1  authored
    wall-blower+wall-gears == blower1  synthesized

  relations over an empty type (8 relations, 9 positions)
    lethal  dynamic  position 1 of (threat)  empty type (threat)
    mounted-on  dynamic  position 2 of (fan gears)  empty type (gears)
    mounted-on  dynamic  position 1 of (fan gears)  empty type (fan)
    recording-switched-on  dynamic  position 1 of (switch)  empty type (switch)
    switched-on  dynamic  position 1 of (switch)  empty type (switch)
    edge-segment>  static  position 1 of (edge rational rational rational rational rational)  empty type (edge)
    screen-segment>  static  position 1 of (screen rational rational rational rational rational)  empty type (screen)
    threatens  static  position 1 of (threat location)  empty type (threat)
    window-segment>  static  position 1 of (window rational rational rational rational rational)  empty type (window)

  constant quantifier sites (15)
    blower-present  exists (?fan fan)  ->  false
    edge-segment-records  doall (?edge edge)  ->  true
    initialize-recording-switch-state!  doall (?switch switch)  ->  true
    physical-supports-at  doall (?fan fan)  ->  true
    physical-supports-at  doall (?fixed (either floor-blower angled-blower))  ->  true
    physical-supports-at  doall (?box box)  ->  true
    physical-supports-at  doall (?tray tray)  ->  true
    recording-jammed  exists (?jammer jammer)  ->  false
    safe  exists (?t threat)  ->  false
    screen-segment-records  doall (?screen screen)  ->  true
    terrain-edge-spans  doall (?edge edge)  ->  true
    update-blower-status!  exists (?j jammer)  ->  false
    update-blower-status!  doall (?f fan)  ->  true
    update-gate-status!  exists (?j jammer)  ->  false
    window-segment-records  doall (?window window)  ->  true

  constant predicates (2)
    recording-jammed == false
    safe == true


S1  CONTROL ALGEBRA  [grade 1]
--------------------------------------------------------------

  control table (3 entries)
    blower1 == plate1
    gate1 == plate1
    gate2 == receiver1

  device state axioms (4)
    open asserted by update-gate-status!
      condition  (or (exists (?j jammer) (jamming ?j ?gate)) (control-on ?gate nil))
      aggregate  (control-on ?gate nil)
      reading    state == aggregate  premise: jammer empty
    recording-open asserted by update-recording-gate-status!
      condition  (or (recording-jammed ?gate) (recording-control-on ?gate nil))
      aggregate  (recording-control-on ?gate nil)
      reading    state == aggregate  premise: jammer empty
    recording-turning asserted by update-recording-blower-status!
      condition  (and (recording-control-on ?drive t) (not (recording-jammed ?drive)))
      aggregate  (recording-control-on ?drive t)
      reading    state == aggregate  premise: jammer empty
    turning asserted by update-blower-status!
      condition  (and (control-on ?drive t) (not (exists (?j jammer) (jamming ?j ?drive))))
      aggregate  (control-on ?drive t)
      reading    state == aggregate  premise: jammer empty

  exclusion pairs (0)

  equivalence pairs (1)
    {blower1, gate1}  on ((plate1))

  pair qualification
    UNCONDITIONAL, on a stated premise.  All 4 device state axioms reduce to their control aggregate because jammer is empty, so the table and the pairs are claims about device state.  Populate that type and both become false.

  primitive controllers (2)
    plate1  ground  status relation latched
    receiver1  device-mediated  status relation active

  device depth
    blower1  depth 1
    gate1  depth 1
    gate2  depth 2

  cycles: none

  notes
    receiver1 is device-mediated through its status relation active, which an update derives from another device's derived output.  The extra level is recorded; the identity of the supplying device is not decidable from the control algebra and is deferred to the sightline extractor.


S2  FUNCTIONAL-RELATION CENSUS  [grade 1 -> 2]
--------------------------------------------------------------

  functional relations (27: 6 dynamic, 21 static)
    4 bijective index relations excluded, as S0 excludes them
    aimed-at  static  key (1)  value (2)  signature ((either angled-blower angled-gears floor-blower floor-gears wall-blower wall-gears) location)
    apparatus-coords>  static  key (1)  value (2 3 4)  signature ((either floor-repeater gun receiver switch transmitter wall-repeater) rational rational rational)
    beam-via  static  key (1 3)  value (2)  signature (fixed-beam-source list fixed-beam-sink)
    boundary-wall  static  key none -- keyless global fluent  value (1)  signature (list)
    color  dynamic  key (1)  value (2)  signature (relay hue)
    controls  static  key (2)  value (1 3)  signature (list (either angled-blower angled-gears floor-blower floor-gears gate gun wall-blower wall-gears) mode)
    edge-segment>  static  key (1)  value (2 3 4 5 6)  signature (edge rational rational rational rational rational)
    gate-segment>  static  key (1)  value (2 3 4 5 6)  signature (gate rational rational rational rational rational)
    has-chroma  static  key (1)  value (2)  signature ((either receiver transmitter) hue)
    has-elevation  static  key (1)  value (2)  signature (elevated-object rational)
    has-height  static  key (1)  value (2)  signature (heighted-object rational)
    has-location  dynamic  key (1)  value (2)  signature (mobile-object location)
    has-position  static  key (1)  value (2)  signature (fixed-position-object location)
    holding  dynamic  key none -- bijective, functional both ways  value (1 2)  signature (agent cargo)
    location-coords>  static  key (1)  value (2 3 4)  signature (location rational rational rational)
    los-barrier-crossings>  static  key (1 3)  value (2)  signature (los-endpoint list visibility-object)
    los-via  static  key (1 3)  value (2)  signature (visibility-object list visibility-object)
    mounted-on  dynamic  key (1)  value (2)  signature (fan gears)
    on  dynamic  key (1)  value (2)  signature (support-occupant support)
    recorder-cycles-used  dynamic  key none -- keyless global fluent  value (1)  signature (fixnum)
    recording-copy>  static  key none -- bijective, functional both ways  value (1 2)  signature (mobile-object mobile-object)
    screen-segment>  static  key (1)  value (2 3 4 5 6)  signature (screen rational rational rational rational rational)
    stream-width  static  key (1)  value (2)  signature ((either wall-blower wall-gears) rational)
    traverse-via  static  key (1 3)  value (2)  signature (location list location)
    traverse-via>  static  key (1 3)  value (2)  signature (location list location)
    wall-segment>  static  key (1)  value (2 3 4 5 6)  signature (wall rational rational rational rational rational)
    window-segment>  static  key (1)  value (2 3 4 5 6)  signature (window rational rational rational rational rational)

  occupancy pools (7 placement relations; 2 layer pairs)
    layer pair: agent1 -> agent1*
    layer pair: connector1 -> connector1*
    aimed-at  static  (either angled-blower angled-gears floor-blower floor-gears wall-blower wall-gears) at 1  ->  location at 2
        key   pool (either angled-blower angled-gears floor-blower floor-gears wall-blower wall-gears) (1): 0 live, 0 ghost, 1 unpaired
              blower1[unpaired]
        value pool location (6): 0 live, 0 ghost, 6 unpaired
              location1[unpaired] location2[unpaired] location3[unpaired] location4[unpaired] location5[unpaired] location6[unpaired]
    color  dynamic  relay at 1  ->  hue at 2
        key   pool relay (3): 1 live, 1 ghost, 1 unpaired
              connector1[live] connector1*[ghost] repeater1[unpaired]
        value pool hue (1): 0 live, 0 ghost, 1 unpaired
              blue[unpaired]
    has-chroma  static  (either receiver transmitter) at 1  ->  hue at 2
        key   pool (either receiver transmitter) (2): 0 live, 0 ghost, 2 unpaired
              receiver1[unpaired] transmitter1[unpaired]
        value pool hue (1): 0 live, 0 ghost, 1 unpaired
              members listed above
    has-location  dynamic  mobile-object at 1  ->  location at 2
        key   pool mobile-object (4): 2 live, 2 ghost, 0 unpaired
              agent1[live] agent1*[ghost] connector1[live] connector1*[ghost]
        value pool location (6): 0 live, 0 ghost, 6 unpaired
              members listed above
    has-position  static  fixed-position-object at 1  ->  location at 2
        key   pool fixed-position-object (3): 0 live, 0 ghost, 3 unpaired
              blower1[unpaired] plate1[unpaired] recorder1[unpaired]
        value pool location (6): 0 live, 0 ghost, 6 unpaired
              members listed above
    mounted-on  dynamic  fan at 1  ->  gears at 2
        key   pool fan (0): 0 live, 0 ghost, 0 unpaired
        value pool gears (0): 0 live, 0 ghost, 0 unpaired
    on  dynamic  support-occupant at 1  ->  support at 2
        key   pool support-occupant (4): 2 live, 2 ghost, 0 unpaired
              agent1[live] agent1*[ghost] connector1[live] connector1*[ghost]
        value pool support (1): 0 live, 0 ghost, 1 unpaired
              plate1[unpaired]

  cardinality bounds  [grade 2: the keying is structural, so no action moves it]
    color: relay -> hue
      |occupied hue| <= 3 - |unavailable relay|
      injective: the relation is keyed by its relay argument, so two distinct occupied values need two distinct witnesses
      BODIES by layer, not yet a claim about any predicate: live + unpaired 2, ghost + unpaired 2, total 3
      consumers (1 relation): the bound each one actually reads
        active [derived]  asserted by update-receiver-status!  via beam-reaches-receiver
          site in relay-beam-reaches-receiver: NONE -- layer-blind, it reads every occupant
          witnesses it reads: 3 -- the whole pool
      NOTE: assertion side only.  A query used in an action's precondition is not listed here.
      NOTE: the switch walk descends AND, OR, NOT, IF and the queries those call.  A switch inside any other form is not found, so "no switch found" is weaker than "no switch".
      *start-state* reading, NOT the bound: 0 of 3 keys assigned, 0 distinct values occupied
    has-location: mobile-object -> location
      |occupied location| <= 4 - |unavailable mobile-object|
      injective: the relation is keyed by its mobile-object argument, so two distinct occupied values need two distinct witnesses
      BODIES by layer, not yet a claim about any predicate: live + unpaired 2, ghost + unpaired 2, total 4
      consumers (3 relations): the bound each one actually reads
        active [derived]  asserted by update-receiver-status!  via beam-reaches-receiver
          site in relay-beam-reaches-receiver: NONE -- layer-blind, it reads every occupant
          site in base: NONE -- layer-blind, it reads every occupant
          site in beam-blocker-occludes-location: OTHER -- restricted by something that is not a layer by (beam-blocker-spans-elevation ?blocker ?beam-elevation)
          site in beam-blocker-occludes-location-for-object: LAYER, STATE-SELECTED by (recorder-cycle-closed) in recording-shadow-object-present
          witnesses it reads: 4 -- the whole pool
        on [not derived]  asserted by sweep-occupants-away!  via top
          site in base: NONE -- layer-blind, it reads every occupant
          witnesses it reads: 4 -- the whole pool
        recording-active [derived]  asserted by update-recording-receiver-status!  via recording-shadow-beam-reaches-receiver
          site in base: NONE -- layer-blind, it reads every occupant
          site in beam-blocker-occludes-location: OTHER -- restricted by something that is not a layer by (beam-blocker-spans-elevation ?blocker ?beam-elevation)
          site in beam-blocker-occludes-location-for-object: LAYER, STATE-SELECTED by (recorder-cycle-closed) in recording-shadow-object-present
          witnesses it reads: 4 -- the whole pool
      NOTE: assertion side only.  A query used in an action's precondition is not listed here.
      NOTE: the switch walk descends AND, OR, NOT, IF and the queries those call.  A switch inside any other form is not found, so "no switch found" is weaker than "no switch".
      *start-state* reading, NOT the bound: 2 of 4 keys assigned, 1 distinct value occupied
    mounted-on: fan -> gears
      |occupied gears| <= 0 - |unavailable fan|
      injective: the relation is keyed by its fan argument, so two distinct occupied values need two distinct witnesses
      BODIES by layer, not yet a claim about any predicate: live + unpaired 0, ghost + unpaired 0, total 0
      consumers (1 relation): the bound each one actually reads
        on [not derived]  asserted by sweep-occupants-away!  via blower-active-for-object
          site in blower-present: NONE -- layer-blind, it reads every occupant
          witnesses it reads: 0 -- the whole pool
      NOTE: assertion side only.  A query used in an action's precondition is not listed here.
      NOTE: the switch walk descends AND, OR, NOT, IF and the queries those call.  A switch inside any other form is not found, so "no switch found" is weaker than "no switch".
      *start-state* reading, NOT the bound: 0 of 0 keys assigned, 0 distinct values occupied
    on: support-occupant -> support
      |occupied support| <= 4 - |unavailable support-occupant|
      injective: the relation is keyed by its support-occupant argument, so two distinct occupied values need two distinct witnesses
      BODIES by layer, not yet a claim about any predicate: live + unpaired 2, ghost + unpaired 2, total 4
      consumers (7 relations): the bound each one actually reads
        active [derived]  asserted by update-receiver-status!  via beam-reaches-receiver
          site in base: NONE -- layer-blind, it reads every occupant
          witnesses it reads: 4 -- the whole pool
        depressed [derived]  asserted by update-plate-status!  via support-occupied
          site in support-occupied: NONE -- layer-blind, it reads every occupant
          witnesses it reads: 4 -- the whole pool
        latched [not derived]  asserted by update-plate-status!  via support-occupied
          site in support-occupied: NONE -- layer-blind, it reads every occupant
          witnesses it reads: 4 -- the whole pool
        on [not derived]  asserted by sweep-occupants-away!  via top
          site in base: NONE -- layer-blind, it reads every occupant
          witnesses it reads: 4 -- the whole pool
        recording-active [derived]  asserted by update-recording-receiver-status!  via recording-shadow-beam-reaches-receiver
          site in base: NONE -- layer-blind, it reads every occupant
          witnesses it reads: 4 -- the whole pool
        recording-depressed [derived]  asserted by update-recording-plate-status!  via recording-plate-occupied
          site in recording-plate-occupied: LAYER, STATE-SELECTED by (recorder-cycle-closed)
          witnesses it reads: 2, either class -- the class is chosen at run time
        recording-latched [derived]  asserted by update-recording-plate-status!  via recording-plate-occupied
          site in recording-plate-occupied: LAYER, STATE-SELECTED by (recorder-cycle-closed)
          witnesses it reads: 2, either class -- the class is chosen at run time
      NOTE: assertion side only.  A query used in an action's precondition is not listed here.
      NOTE: the switch walk descends AND, OR, NOT, IF and the queries those call.  A switch inside any other form is not found, so "no switch found" is weaker than "no switch".
      *start-state* reading, NOT the bound: 0 of 4 keys assigned, 0 distinct values occupied


T6  MECHANIZED BUDGET ARITHMETIC  [grade 1 -> 2]
--------------------------------------------------------------
  no body-cost devices found.


S5  HEIGHT AND REACH LATTICE  [grade 2]
--------------------------------------------------------------
  type heights (21 types; 0 authored overrides)
    location  height 0  axis NONE  base 0
    agent  height 3/2  axis VERTICAL  base 0
    box  height 1  axis VERTICAL  base 0
    connector  height 1  axis VERTICAL  base 0
    jammer  height 1  axis VERTICAL  base 0
    tray  height 0  axis VERTICAL  base 0
    fan  height 0  axis VERTICAL  base 0
    pressure-plate  height 0  axis VERTICAL  base 0
    toggle-plate  height 0  axis VERTICAL  base 0
    floor-blower  height 0  axis VERTICAL  base 0
    angled-blower  height 0  axis VERTICAL  base 0
    gate  height 4  axis VERTICAL  base 0
    screen  height 4  axis VERTICAL  base 0
    wall  height 4  axis VERTICAL  base 0
    edge  height 3/2  axis VERTICAL  base 0
    floor-repeater  height 1  axis VERTICAL  base 0
    wall-repeater  height 1  axis HORIZONTAL  base 1
    transmitter  height 0  axis NONE  base 1
    receiver  height 0  axis NONE  base 1
    switch  height 0  axis NONE  base 1
    gun  height 0  axis NONE  base 1

  location levels
    location1  0
    location2  0
    location3  0
    location4  0
    location5  0
    location6  0

  achievable carried-object tops
    connector1  1
    connector1*  1

  placement legality matrix (agent base -> support top)
    agent1 0 -> ground 0  YES
    agent1* 0 -> ground 0  YES

  unreachable from ground (placement reach limit 1)
    none


S6  BEAM SIGHTLINE TABLE  [grade 2]
--------------------------------------------------------------
  direct gate subsets: 4; no propagation applied

  visibility rows
    location1 @ 1 -> transmitter1  CONDITIONAL  requires open gate1
    location1 @ 1 -> receiver1  NEVER
    location1 @ 1 -> repeater1  ALWAYS
    location2 @ 1 -> transmitter1  NEVER
    location2 @ 1 -> receiver1  NEVER
    location2 @ 1 -> repeater1  ALWAYS
    location3 @ 1 -> transmitter1  NEVER
    location3 @ 1 -> receiver1  ALWAYS
    location3 @ 1 -> repeater1  ALWAYS
    location4 @ 1 -> transmitter1  NEVER
    location4 @ 1 -> receiver1  ALWAYS
    location4 @ 1 -> repeater1  NEVER
    location5 @ 1 -> transmitter1  NEVER
    location5 @ 1 -> receiver1  CONDITIONAL  requires open gate2
    location5 @ 1 -> repeater1  NEVER
    location6 @ 1 -> transmitter1  NEVER
    location6 @ 1 -> receiver1  NEVER
    location6 @ 1 -> repeater1  ALWAYS

  location-occluder kill list
    none


RC  RELAY CHAIN TABLE  [grade 2]

  SUPPLIED RELAY SCENARIO (T33): CLEAR is conditional, not stable/reachable/validated.
    PHYSICAL UNRESOLVED: no explicit scenario supplied
    RECORDING UNRESOLVED: no explicit scenario supplied
--------------------------------------------------------------
  GEOMETRIC ENUMERATION SCOPE: physical view only; supplied scenario views are separate.  Hops are
  tested on start-state copies with gate OPEN bits forced and no propagation.  A
  hop's required gates are those whose closing alone blocks it (monotone reading).
  Stations are placements, not reachability claims.  Bodies count the connector and
  its riser (ground 0, held tray 2, other support 1); a station with a plate is
  counted as keeping it, so off-plate counts are least values within this enumeration.
  GEOMETRIC CANDIDATES: stable simultaneous occupancy and support motion UNRESOLVED.
  BOOTSTRAP/LATCH are geometric classes, not validated realizations. Connector height
  is that used by station enumeration; differing connector heights are not enumerated.
  connectors 2; fixed couplings 0 (not enumerated); exclusion pairs 

  stations (6): location, then top (supports) per achievable connector top
    location1  1 (ground)
    location2  1 (ground)
    location3  1 (ground)
    location4  1 (ground)
    location5  1 (ground)
    location6  1 (ground)

  station-to-endpoint hops (8 visible)
    location1@1 -> transmitter1  requires open gate1
    location1@1 -> repeater1  ALWAYS
    location2@1 -> repeater1  ALWAYS
    location3@1 -> receiver1  ALWAYS
    location3@1 -> repeater1  ALWAYS
    location4@1 -> receiver1  ALWAYS
    location5@1 -> receiver1  requires open gate2
    location6@1 -> repeater1  ALWAYS

  station-to-station hops (14 visible, 14 groups): source -> target, source>target tops, gates required
    location1 -> location2  all tops  ALWAYS
    location1 -> location6  all tops  ALWAYS
    location2 -> location1  all tops  ALWAYS
    location2 -> location6  all tops  ALWAYS
    location3 -> location4  all tops  ALWAYS
    location3 -> location5  all tops  requires open gate2
    location3 -> location6  all tops  ALWAYS
    location4 -> location3  all tops  ALWAYS
    location4 -> location5  all tops  requires open gate2
    location5 -> location3  all tops  requires open gate2
    location5 -> location4  all tops  requires open gate2
    location6 -> location1  all tops  ALWAYS
    location6 -> location2  all tops  ALWAYS
    location6 -> location3  all tops  ALWAYS

  chains to receiver1 (1); LATCH needs a device this receiver controls
    1  transmitter1 -> location1@1 -> repeater1 -> location3@1 -> receiver1  BOOTSTRAP
        gates gate1; plates for them  (none)
        connectors 2; risers ground, ground; bodies 2, on plates 0, off plates 2
        GEOMETRIC CANDIDATE, physical sightlines only; recording sightlines, body/view assignment and occupancy stability UNRESOLVED
        blower1 at location3: base 0, top 1, stream 1; SWEPT if a fan is present and turns in the occupant's view; destination location6; LIVE STATION CONFLICT while physical gate1 open (S1 state/aggregate equivalence); ghost fan state independent

  summary for receiver1
    chains 1: bootstrap 1, latch 0, excluded 0, infeasible 0
    gates open in every bootstrap chain: gate1
    least off-plate bodies over bootstrap chains: 2
    with 2 connectors: 1 chain, least off-plate bodies 2, receiver-end stations location3@1


S7  LANDMARK GRAPH AND ORDERINGS  [grade 4]
--------------------------------------------------------------
  relaxation: delete relaxation; achieved landmarks persist.
  no simultaneous-role, keeper-return, segment, or route claim is emitted.

  explicit goal landmarks
    (has-location agent1 location5)  movement/query landmark; S1 expansion unavailable.

  S1 controller expansions
    none: the explicit goal has no controlled-device condition.

  greedy-necessary orderings
    none: route/order extraction needs a separately stated movement relaxation.


S3  GATE-LABELLED REGION QUOTIENT  [grade 2]
--------------------------------------------------------------

  traversal arcs read (18)
    12 symmetric (traverse-via), 6 directed (traverse-via>)
    kind walk: 18 arcs, 5 with an empty family

  contraction rule: two endpoints share a region when an arc of traverse-via joins them with an EMPTY door family.  Static separators -- staircases, edges, floor drives -- are not doors.  Arcs of traverse-via> are never contracted, whatever their family.
  NOTE: a region is a set of endpoints NO DOOR separates.  Each kind carries its own predicate -- a jump's reach limit, a ladder's position -- which this extractor does not evaluate, having no state to evaluate it in.  Two endpoints in one region therefore need not be mutually reachable.

  regions (4 over 6 endpoints of type location)
    R1  (3): location1 location2 location6
    R2  (1): location3
    R3  (1): location4
    R4  (1): location5

  region crossings (12 rows: 5 spine, 7 composed)
    NOTE: these rows are the transitive CLOSURE, one minimal door-set per location pair. The spine preserves reachability; it is not a physical doorway count.
    R1 <-> R2  kind walk  family ((blower1))  2 location arcs  composed
    R1 --> R2  kind walk  family ((blower1))  1 location arc  composed
    R1 <-> R3  kind walk  family ((blower1))  2 location arcs  composed
    R1 --> R3  kind walk  family ((blower1))  1 location arc  SPINE
    R1 <-> R4  kind walk  family ((blower1 gate2))  2 location arcs  composed
    R1 --> R4  kind walk  family ((blower1 gate2))  1 location arc  composed
    R2 --> R1  kind walk  family () direct  1 location arc  SPINE
    R2 <-> R3  kind walk  family ((blower1))  1 location arc  SPINE
    R2 <-> R4  kind walk  family ((blower1 gate2))  1 location arc  composed
    R3 --> R1  kind walk  family () direct  1 location arc  SPINE
    R3 <-> R4  kind walk  family ((gate2))  1 location arc  SPINE
    R4 --> R1  kind walk  family ((gate2))  1 location arc  composed

  adjacency spine (5)
    R1 --> R3  kind walk  family ((blower1))
    R2 --> R1  kind walk  family () direct
    R2 <-> R3  kind walk  family ((blower1))
    R3 --> R1  kind walk  family () direct
    R3 <-> R4  kind walk  family ((gate2))

  doors on arcs (2)
    blower1 gate2

  controlled devices labelling NO traversal arc (1 of 3)
    gate1
    READING: such a device is movement-irrelevant, meaning that no traversal clause names it.  It is NOT a claim that the device is inert -- a device may act on objects rather than on passage -- and it is NOT a claim about reaching, which a separate relation carries and this extractor does not read.

  doors that are NOT controlled devices (0)
    
    these are obstacles with no CONTROLS entry, so no plate or switch opens them and S1's algebra says nothing about them.


S4  CUT-KEEPER TABLE  [conditional bounds; graph candidates]
--------------------------------------------------------------
  SCOPE: graph reachability relaxes all other doors, elevation and cargo conditions.
  It omits non-traversal relocation, support transitions and recorder lifecycle.
  Graph cuts and approach-only regions therefore do NOT prove concrete stranding.
  Pressure counts require ON's functional key and the relevant view's occupancy semantics.
  Device-state conclusions additionally require the printed S1 axiom premises.

  controlled devices (3); spine rows (5); spine check :VERIFIED-AGAINST-QUOTIENT

    blower1 == plate1
      state recording-turning: state == aggregate; empty-type premises (jammer)
      state turning: state == aggregate; empty-type premises (jammer)
      controller plate1: LATCH; position location2; region R1
        persistent state; no continuous weight requirement inferred.
      positive pressure alternatives (nil); individually mandatory nil
      conditional shortage: available eligible ON witnesses < 0 implies
        this normal aggregate cannot activate (minimum simultaneous plate demand).
      spine kind walk, family ((blower1))
        R1 -> R3, device absent: source reaches ("R1"); destination reaches ("R1" "R3" "R4")
          graph cut in this direction: YES
      spine kind walk, family ((blower1))
        R2 -> R3, device absent: source reaches ("R1" "R2"); destination reaches ("R1" "R3" "R4")
          graph cut in this direction: YES
        R3 -> R2, device absent: source reaches ("R1" "R3" "R4"); destination reaches ("R1" "R2")
          graph cut in this direction: YES

    gate1 == plate1
      state open: state == aggregate; empty-type premises (jammer)
      state recording-open: state == aggregate; empty-type premises (jammer)
      controller plate1: LATCH; position location2; region R1
        persistent state; no continuous weight requirement inferred.
      positive pressure alternatives (nil); individually mandatory nil
      conditional shortage: available eligible ON witnesses < 0 implies
        this normal aggregate cannot activate (minimum simultaneous plate demand).
      no movement-spine occurrence; nonmovement function UNRESOLVED, not inert.

    gate2 == receiver1
      state open: state == aggregate; empty-type premises (jammer)
      state recording-open: state == aggregate; empty-type premises (jammer)
      controller receiver1: RECEIVER; position unresolved; region UNRESOLVED
        beam dependency unresolved; requires sightline analysis.
      positive pressure alternatives (nil); individually mandatory nil
      conditional shortage: available eligible ON witnesses < 0 implies
        this normal aggregate cannot activate (minimum simultaneous plate demand).
      spine kind walk, family ((gate2))
        R3 -> R4, device absent: source reaches ("R1" "R2" "R3"); destination reaches ("R4")
          graph cut in this direction: YES
        R4 -> R3, device absent: source reaches ("R4"); destination reaches ("R1" "R2" "R3")
          graph cut in this direction: YES

  explicit goal destinations (1); goal form (and (has-location agent1 location5))
    agent1: location1 (R1) -> location5 (R4)
      GRAPH-REQUIRED candidates (blower1 gate2); concrete necessity UNRESOLVED.
    connector1: initially location1; no explicit destination, crossings UNRESOLVED.

  keeper supply from S2
    on: support-occupant -> support
      |occupied support| <= 4 - |unavailable support-occupant|
      injective: the relation is keyed by its support-occupant argument, so two distinct occupied values need two distinct witnesses
      BODIES by layer, not yet a claim about any predicate: live + unpaired 2, ghost + unpaired 2, total 4
      consumers (7 relations): the bound each one actually reads
        active [derived]  asserted by update-receiver-status!  via beam-reaches-receiver
          site in base: NONE -- layer-blind, it reads every occupant
          witnesses it reads: 4 -- the whole pool
        depressed [derived]  asserted by update-plate-status!  via support-occupied
          site in support-occupied: NONE -- layer-blind, it reads every occupant
          witnesses it reads: 4 -- the whole pool
        latched [not derived]  asserted by update-plate-status!  via support-occupied
          site in support-occupied: NONE -- layer-blind, it reads every occupant
          witnesses it reads: 4 -- the whole pool
        on [not derived]  asserted by sweep-occupants-away!  via top
          site in base: NONE -- layer-blind, it reads every occupant
          witnesses it reads: 4 -- the whole pool
        recording-active [derived]  asserted by update-recording-receiver-status!  via recording-shadow-beam-reaches-receiver
          site in base: NONE -- layer-blind, it reads every occupant
          witnesses it reads: 4 -- the whole pool
        recording-depressed [derived]  asserted by update-recording-plate-status!  via recording-plate-occupied
          site in recording-plate-occupied: LAYER, STATE-SELECTED by (recorder-cycle-closed)
          witnesses it reads: 2, either class -- the class is chosen at run time
        recording-latched [derived]  asserted by update-recording-plate-status!  via recording-plate-occupied
          site in recording-plate-occupied: LAYER, STATE-SELECTED by (recorder-cycle-closed)
          witnesses it reads: 2, either class -- the class is chosen at run time
      NOTE: assertion side only.  A query used in an action's precondition is not listed here.
      NOTE: the switch walk descends AND, OR, NOT, IF and the queries those call.  A switch inside any other form is not found, so "no switch found" is weaker than "no switch".
      *start-state* reading, NOT the bound: 0 of 4 keys assigned, 0 distinct values occupied
    Available eligible witnesses are a parameter for each view and segment.
    Total sequential crossers are NOT simultaneous body demand.

  UNCONDITIONAL STRANDING: unresolved; no verdict emitted.


CC  COUPLING CENSUS  [grade 1; occluder role grade 2]
--------------------------------------------------------------
  subsystems: route (barrier), beam (occluder, beam-driven), lift (lift), transport (horizontal-transport, transport), occupancy (support-controller)

  role table (5 objects)
    blower1  device  barrier horizontal-transport  subsystems route transport
    gate1  device  occluder  subsystems beam
    gate2  device  barrier occluder  subsystems route beam
    plate1  primitive  support-controller  subsystems occupancy
    receiver1  primitive  beam-driven  subsystems beam

  K1 fan-out (1)
    plate1  subsystems route beam transport occupancy
      blower1 == plate1  barrier horizontal-transport
      gate1 == plate1  occluder
      {blower1, gate1}  EQUIVALENCE

  K2 multi-role (2)
    blower1  route transport
    gate2  route beam

  K3 beam feedback (1)
    receiver1  drives gate2
      last-hop gates (1)
        gate2  controllers receiver1  SELF

  G15 lift-barrier couplings (0)
    none


NH  NECESSITY HINTS  [grade per hint]

  SUPPLIED RELAY SCENARIO (T33): CLEAR is conditional, not stable/reachable/validated.
    PHYSICAL UNRESOLVED: no explicit scenario supplied
    RECORDING UNRESOLVED: no explicit scenario supplied
--------------------------------------------------------------
  READING: a hint restates static limits as a candidate plan element for the Briefing (Problem-Solving Guide, Phase 1 step 3).  NECESSARY: every plan meets it, under the grade shown.  CANDIDATE: one way to meet a limit; others may exist.  A hint is not a plan, and a graph candidate is not a proof.

  hints (2): 1 NECESSARY, 1 CANDIDATE

  H1 body budget (0)
    none

  H2 keepers left behind (0)
    none

  H3 beam-held devices (2)
    H3.1  NECESSARY  [grade 2; S1 RC]
      limit  gate2 == receiver1 holds only while receiver1 is active; within RC's enumerated physical geometric candidates, every chain to receiver1 (1 bootstrap, 0 latch) needs gate1 open
      hint   within those geometric candidates for gate2, at least 2 bodies are off plates for the beam
      note   S1's receiver condition is necessary; RC gate/body bounds are conditional on its physical geometric enumeration, not all recording-view beams
      note   Recording sightlines, body/view assignment, forced transport and occupancy stability UNRESOLVED; geometric chains are not validated realizations
    H3.2  CANDIDATE  [grade 2; RC]
      limit  physical geometric candidates to receiver1 with last connector at location3 (R2): least off-plate bodies 2
      hint   transmitter1 -> location1@1 -> repeater1 -> location3@1 -> receiver1  risers ground, ground; bodies 2, off plates 2
      note   GEOMETRIC CANDIDATE, physical sightlines only; recording sightlines, body/view assignment and occupancy stability UNRESOLVED
      note   blower1 at location3: base 0, top 1, stream 1; SWEPT if a fan is present and turns in the occupant's view; destination location6; LIVE STATION CONFLICT while physical gate1 open (S1 state/aggregate equivalence); ghost fan state independent

  H4 controllers off the goal route (0)
    none

  H5 lift landings (0)
    none

  H6 active at the start (0)
    none

  H7 placement limits (0)
    none


SD  SERVICES AND SETUP DEPENDENCIES  [grade 2]
--------------------------------------------------------------
  SCOPE: a monotone premise closure over passage services (every gate; each drive a traversal clause names) and receiver literals.  Providers: S1 CONTROL options, MC jam sites (OVERRIDE), gears with no fan (EQUIPMENT), RC chains and fixed corridors to a receiver.  No ordering, simultaneity, bodies, reach, occupancy or view is checked.
  CLASSES: DIRECT no premise; SUPPORTED premises available without this service; NEEDS <service> FIRST: installing this provider needs the service it will provide (a setup dependency); UNSUPPORTED IN SCOPE.  A service with only NEEDS-FIRST options is a SETUP QUESTION, not an impossibility.  "Through standing providers" repeats the test with premises supplied only by CONTROL, chains, corridors and equipment, never another jam, and is printed when that exposes a setup dependency a further jammer would hide.
  RECORDER SPLICED: physical view only; recording-view providers are not read.

  goal actor agent1: start location1 (R1) -> goal location5 (R4)
    transit door sets (R1 -> R4, 1): (blower1 gate2)
      necessary: blower1 gate2
    return door sets (R4 -> R1, 1): (gate2)
      necessary: gate2
    final services: none (the goal names no receiver or controlled device)
    temporary services (in some transit set, not final): blower1 via plate1, gate2 via receiver1
      READING: TEMPORARY means needed while crossing and expendable afterward, unless a return or a later crossing needs it again.

  access from R1 (minimal door sets to each region; kind predicates not evaluated)
    R1  ()
    R2  (blower1)
    R3  (blower1)
    R4  (blower1 gate2)

  retrieval (start places of jammers, connectors and fans)
    connector1  location1 (R1)
    connector1*  absent

  services (4): 4 SUPPORTED, 0 SETUP QUESTION, 0 NO PROVIDER IN SCOPE
    gate1 open  == plate1  start BLOCKED  verdict SUPPORTED
      CONTROL DIRECT: plate1 latched
    gate2 open  == receiver1  start BLOCKED  verdict SUPPORTED  route TRANSIT necessary, RETURN necessary, TEMPORARY
      CONTROL SUPPORTED: receiver1 active
    blower1 clear  == plate1  start PASSABLE  verdict SUPPORTED  route TRANSIT necessary, TEMPORARY
      CONTROL DIRECT: plate1 not latched
    receiver1 active  start INACTIVE  verdict SUPPORTED
      CHAINS SUPPORTED: 1 RC chain (bootstrap); gate1 open

  opposed controls (a primitive needed in both states by different services)
    plate1: on for gate1; off for blower1

  setup dependencies (options whose premises lead back to their own service)
    none
    setup questions: none

  NOT CLAIMED: an order, simultaneous availability, a body or reach allocation, occupancy, view or a realized setup.  A premise-free provider still needs placing, and a NEEDS-FIRST provider needs another provider in force while it is installed (a handover).  Access is to a site's own region; placement or pickup from another location within reach is not modelled.  For concrete consequences use REPORT-SERVICE-TRANSITION on two settled states.
RO requires an explicit segment input and is not generated; call
REPORT-ROLE-OBLIGATIONS with a stated scenario.
