the book (bin/counter book)
the book of the seed (lean-only reading; the instrument reads terms, never prose)
the census [grown/Room.lean]: 183 declarations (29 carriers, 154 theorems), 183 receipts
the arrows [grown/Room.lean]: 211 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the frontier [grown/Room.lean] — 23 leaves no organ in the house cites yet (read from the elaborator):
the_held_name_their_darkness
the_unencumbered_are_welcome
true_or_reads
the_rest_reads
an_enrolled_name_is_a_member
fresh_counts_the_uniq
fresh_of_the_alike_is_one
a_merging_map_has_no_section
the_enrolled_stay_enrolled
the_seat_is_load_bearing_in_the_same_click
the_unenrolled_are_no_member
the_backing_survives_the_hall
the_longest_reaches_each
a_name_is_or_is_not
fresh_at_most_the_length
the_wear_is_a_reading
everyone_means_each
the_circle_stays_dark
the_book_is_the_answer_space
a_sweep_that_seats_no_one_waited_everyone
the_orbit_is_the_book
the_census_of_orders_is_exact
the_direction_is_even_money
cited only from above [grown/Room.lean] — 21 organs no organ of their own storey cites, seated by a storey that stands on it:
the_carriers_compose ← Face
the_carrier_merges_only_the_alike ← Face
the_terminus_takes_every_carrier ← Face
the_first_mark_reads ← Face
filter_holds ← Face
mem_filter_intro ← Face
and_congr_first ← Face
and_congr_second ← Face
and_regroups ← Face
the_still_map_carries ← Face
the_append_rests ← Face
len_replicate ← Face
the_unit_word_is_its_count ← Face
ble_le_add_left ← Face
mul_spreads ← Face
ble_le_add ← Face
apart_filter ← Face
mul_one_reads ← Face
the_hallway_is_too_small ← Face
no_mark_lights_itself ← Face
the_key_is_cut_from_the_room ← Face
the census [grown/Face.lean]: 252 declarations (92 carriers, 160 theorems), 252 receipts
the arrows [grown/Face.lean]: 172 citations, 15 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart): the_trivial_revision_changes_nothing→Room.the_still_map_carries the_trivial_revision_changes_nothing→Room.the_carrier_merges_only_the_alike every_door_reading_is_a_face→Room.the_still_map_carries the_host_merges_the_guests→Room.the_still_map_carries a_guest_mover_is_unheard→Room.the_still_map_carries the_deferral_is_free→Room.the_still_map_carries the_unheard_hands_compose→Room.the_carriers_compose an_unread_tape_is_a_tending→Room.the_still_map_carries an_unread_tape_is_a_tending→Room.the_carrier_merges_only_the_alike the_holding_returns→Room.the_still_map_carries the_holding_returns→Room.the_carrier_merges_only_the_alike the_comparison_mints_a_face→Room.the_terminus_takes_every_carrier the_comparison_mints_a_face→Room.the_still_map_carries the_measurement_is_a_meeting→Room.the_terminus_takes_every_carrier the_measurement_is_a_meeting→Room.the_still_map_carries
the frontier [grown/Face.lean] — 91 leaves no organ in the house cites yet (read from the elaborator):
a_guest_blind_reading_is_a_face_reading
the_pairing_is_unique
any_ready_greeter_is_the_greeter
the_host_serves_both_branches
the_sharpening_is_exact
the_origin_is_the_pairs_unit
the_unheard_hands_compose
the_yield_fixes_the_agreed
the_window_agrees_or_names_the_gap
the_agreed_window_sounds_as_one
the_mutual_records_ride_together
the_gap_is_minted_at_the_meeting
the_seats_stack_backward
the_ear_and_the_voice_commute
the_ear_crosses_the_seat
the_voice_crosses_the_seat
the_carrier_was_a_seating
the_obs_carries_to_the_one_face
the_guest_is_real
the_turn_returns
the_crossing_returns
hosting_associates
hosting_associates_back
the_branches_come_home
the_deferral_is_free
the_holding_returns
the_face_was_a_held_door
every_door_reading_is_a_face
the_measurement_is_a_meeting
the_host_was_a_reseat
the_probe_boards_as_the_guest
the_meeting_was_a_self_meeting
the_self_meeting_reads_the_guest
the_origin_merges_every_seat
the_still_hand_is_unheard
the_maintenance_is_the_identitys_hom
the_spoken_arrives_at_the_face
the_speaker_rides_unread
the_listening_turn_is_the_yield
the_two_listeners_restore_the_table
the_ode_comes_home
the_air_gap_wears_the_one_face
the_retuned_seat_walks_the_translated_word
the_pace_wears_the_tallys_voice
any_two_readings_agree
the_revision_is_a_reading
the_trivial_revision_changes_nothing
the_type_is_a_reading
the_customs_keep_the_still_world
the_customs_stack_forward
the_census_checksums_with_the_polygon_cutters
the_muffled_tally_is_the_resting_counter
the_lift_peeks_the_out
the_lift_feeds_the_step
the_unit_machine_steers_itself
the_comparison_mints_a_face
the_concord_reads_both_models
the_interview_crosses_the_seat
no_interview_parts_the_origin
the_manifest_is_natural
the_recital_walks_its_list
the_tending_writes_the_tape
an_unread_tape_is_a_tending
the_read_tape_parts_at_the_gap
a_visit_never_unrests
an_owe_rests_only_on_a_visited_name
a_stage_may_ground_a_stage
lineages_compose
every_seat_is_a_reading_of_the_record
the_revision_multiplies_the_reading
the_muffler_banks_the_run
the_rep_lands_where_it_is_fed
the_drained_is_on_spec
recording_the_recording_grounds
the_mutual_recording_is_unheard
two_seats_record_each_other
the_remembering_never_merges
the_remembering_is_unheard_at_the_gap
the_handshake
only_the_unheard_survives_the_sounding
correct_maintenance_has_no_signature
the_buffer_is_invisible
the_drain_settles
the_concord_is_the_meetings_own
the_census_is_exact
the_clock_is_a_room
room_margin_flywheel_door
the_clock_writes_its_sequence
the_lift_is_the_conduct
entanglement_is_the_loop
three_is_the_width_of_contact
cited only from above [grown/Face.lean] — 10 organs no organ of their own storey cites, seated by a storey that stands on it:
differOnly ← Witness
tallyMachine ← Rest
the_interview_crosses_the_carrier ← Seek
one_face_many_seats ← Rest
a_guest_mover_is_unheard ← Tape
the_bill_is_the_word ← Tape
the_replay_is_the_machine ← Relay Seek
a_translated_intertwiner_carries_the_walk ← Rest
the_pace_is_carried_onto_the_flip ← Crossing
the_tending_is_unheard_at_the_gap ← Crossing Tape
the census [grown/Rest.lean]: 31 declarations (11 carriers, 20 theorems), 31 receipts
the arrows [grown/Rest.lean]: 17 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the frontier [grown/Rest.lean] — 6 leaves no organ in the house cites yet (read from the elaborator):
an_intertwiner_is_a_relation_in_step
the_last_name_unlocks
every_runner_is_a_plan_at_the_one_face
two_still_runners_rest_alike_through_a_translation
the_carried_unit_is_unheard_at_rest
the_rest_handshake
cited only from above [grown/Rest.lean] — 5 organs no organ of their own storey cites, seated by a storey that stands on it:
a_plan_is_read_at_the_gap ← Halt
the_coverage_rests_where_it_stands ← Cycle.Treaty
the_still_plan_is_readable_iff_at_rest ← Tape
every_reader_reads_the_same ← Halt
the_replay_reads_the_plan ← Halt
the census [grown/Witness.lean]: 37 declarations (9 carriers, 28 theorems), 37 receipts
the arrows [grown/Witness.lean]: 16 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the frontier [grown/Witness.lean] — 9 leaves no organ in the house cites yet (read from the elaborator):
seat
the_witness_parts_what_the_face_parts
a_dark_probe_is_out_of_earshot
the_witness_is_a_face
a_wider_cone_reads_no_less
a_wall_at_the_witness
the_cone_is_earshot
a_difference_in_the_cone_is_read
hold_your_peace_on_the_room
cited only from above [grown/Witness.lean] — 13 organs no organ of their own storey cites, seated by a storey that stands on it:
the_seat_that_hears_it_reads_it ← Eih.Treaty EveryoneIsHere.Treaty Here.Treaty
the_sounding_is_the_trails_reading ← Cycle.Treaty
the_ceremony_reseats_every_reading ← Here.Treaty
the_word_at_the_door_is_unread_at_every_seat ← Here.Treaty Threshold
a_seat_over_a_seat_is_derived ← EveryoneIsHere.Treaty Grover.Treaty Here.Treaty
a_cover_of_the_room_covers_its_probes ← Threshold
a_room_covers_itself_at_one_seat ← Eih.Treaty
the_room_is_the_widest_seat ← Cycle.Treaty EveryoneIsHere.Treaty Here.Treaty
a_probe_no_seat_hears_is_dark ← Here.Treaty
the_narration_reads_alike_at_every_seat ← Here.Treaty
a_difference_out_of_the_cone_is_dark ← Here.Treaty
forever_hold_your_peace ← Threshold
the_room_at_its_probes_reads_alike ← Here.Treaty Threshold
the census [grown/Threshold.lean]: 8 declarations (2 carriers, 6 theorems), 8 receipts
the arrows [grown/Threshold.lean]: 8 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the frontier [grown/Threshold.lean] — 5 leaves no organ in the house cites yet (read from the elaborator):
the_crossing_is_licensed
the_threshold
the_route_is_shed
the_crossing_is_licensed_at_the_room
a_threshold_is_a_threshold_at_every_room
cited only from above [grown/Threshold.lean] — 1 organs no organ of their own storey cites, seated by a storey that stands on it:
the_threshold_at_the_room ← Here.Treaty
the census [grown/Toy.lean]: 6 declarations (2 carriers, 4 theorems), 6 receipts
the arrows [grown/Toy.lean]: 3 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the frontier [grown/Toy.lean] — 4 leaves no organ in the house cites yet (read from the elaborator):
the_toy_counts
the_toy_parks
the_toy_resumes
the_toy_flips_back
the census [grown/Counter.lean]: 34 declarations (15 carriers, 19 theorems), 34 receipts
the arrows [grown/Counter.lean]: 6 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the frontier [grown/Counter.lean] — 16 leaves no organ in the house cites yet (read from the elaborator):
the_first_sighting_is_free
a_backed_sighting_seats
an_unbacked_sighting_waits
the_seated_stay_seated
the_held_name_what_they_wait_on
weight_zero_is_backed
a_sighting_that_cites_only_itself_never_seats
two_sightings_that_cite_each_other_stay_dark
the_key_is_cut_from_the_room
the_gate_hears_only_the_receipt
the_vow_is_the_empty_receipt
a_rest_is_drained_or_stuck
the_cascade_and_its_record_rest_alike
a_sighting_is_load_bearing_in_the_same_round
a_receipt_keeping_rebody_is_unheard
the_verdict_survives_the_rebody
the census [grown/Seek.lean]: 11 declarations (2 carriers, 9 theorems), 11 receipts
the arrows [grown/Seek.lean]: 6 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the frontier [grown/Seek.lean] — 7 leaves no organ in the house cites yet (read from the elaborator):
a_failed_move_leaves_no_trace
a_closing_move_is_recorded
the_search_is_the_replay
the_audition_cannot_part_them
the_search_starts_empty
the_search_and_its_replay_are_alike
the_search_has_no_memory
the census [grown/Roster.lean]: 7 declarations (3 carriers, 4 theorems), 7 receipts
the arrows [grown/Roster.lean]: 5 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the frontier [grown/Roster.lean] — 1 leaves no organ in the house cites yet (read from the elaborator):
reseating_keeps_the_sheets_count
cited only from above [grown/Roster.lean] — 1 organs no organ of their own storey cites, seated by a storey that stands on it:
a_yes_reaches_the_sheet ← Eih.Treaty
the census [grown/assays/counter.lean]: 23 declarations (20 carriers, 3 theorems), 23 receipts
the arrows [grown/assays/counter.lean]: 1 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the rows [grown/assays/counter.lean] — 11 carriers no theorem cites, evaluated by the treaty's rows: afterSweep selfCiter circle offered gateA gateB gateC gateCpruned shadowA shadowB shadowC
the frontier [grown/assays/counter.lean] — 2 leaves no organ in the house cites yet (read from the elaborator):
the_prune_is_unheard_at_the_chart
the_two_routes_part_at_the_chart
the census [grown/assays/crossing.lean]: 46 declarations (28 carriers, 18 theorems), 46 receipts
the arrows [grown/assays/crossing.lean]: 10 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the rows [grown/assays/crossing.lean] — 7 carriers no theorem cites, evaluated by the treaty's rows: crossingOfTheTape crossingOfTheTending crossingOfTheVoice crossingBesideTheTally crossingOfTheTallyBeside crossingAtTheWiden lapEnd
the frontier [grown/assays/crossing.lean] — 14 leaves no organ in the house cites yet (read from the elaborator):
a_clock_alike_at_the_gap_never_parts
the_crossing_is_derived
the_tending_never_parts
a_voice_parts_no_sooner
the_read_tape_crosses_at_three
the_pages_are_derived
the_still_clock_has_one_page_at_every_depth
a_pair_costs_at_most_the_product_at_twelve
more_depth_reads_no_fewer_pages_for_the_flip_and_the_tally
the_winding_is_the_crossing_with_the_shift
the_holonomy_of_a_closed_route_is_its_winding
a_pair_parts_when_either_does
the_pace_costs_what_the_flip_costs
a_clock_never_parts_from_its_own_return
the census [grown/assays/cycle.lean]: 59 declarations (36 carriers, 23 theorems), 59 receipts
the arrows [grown/assays/cycle.lean]: 5 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the rows [grown/assays/cycle.lean] — 10 carriers no theorem cites, evaluated by the treaty's rows: held walkAt halfway afterAbe resumed straight clickThenTick tickThenClick report seatReads
the frontier [grown/assays/cycle.lean] — 22 leaves no organ in the house cites yet (read from the elaborator):
abe_is_first
the_one_mutual_hearing
the_rounds_resume
the_click_and_the_tick_commute
the_report_is_the_seats_reading
an_empty_list_rests_at_once
rest_is_weight_zero
the_held_name_what_they_wait_on
a_new_connection_raises_the_weight
rest_survives_a_round
the_pitcher_is_a_reading
an_unvisited_clock_is_a_wall
the_room_is_the_widest_seat
two_rooms_part_only_at_a_clock
the_walker_never_names_now
due_is_read_against_now
now_is_a_reading
rest_is_coverage
the_round_is_still
the_round_rests_where_it_stands
a_visit_never_unrests_the_walker
the_round_spares_now
the census [grown/assays/eih.lean]: 189 declarations (128 carriers, 61 theorems), 189 receipts
the arrows [grown/assays/eih.lean]: 28 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the rows [grown/assays/eih.lean] — 37 carriers no theorem cites, evaluated by the treaty's rows: vendorRoomRequestOf close assign venueChart floristSees djSees catererSees lindaSees bestManSees coupleSees roomSees makerSees makerSeesMore catererSeesMore bestManSeesNew coupleSeesNew roomSeesConfirmed lindaSeesConfirmed lindaSeesVendorConfirmed coupleSeesVendorConfirmed catererSeesDemo catererSeesVendorConfirmed lindaSeesInvoice humanEars coupleSideEars maya jordan coveredWedding ownWedding strayBill vendorRoomFile roster loadIn firstEdit secondEdit headTable table2
the frontier [grown/assays/eih.lean] — 52 leaves no organ in the house cites yet (read from the elaborator):
ask
the_delivery_is_the_sheet
the_delivery_moves_no_guest
a_line_touches_only_the_ledger
the_bach_touches_only_the_bach
the_guests_touch_only_the_guests
a_vendor_never_sees_anothers_invoice
a_vendor_sees_only_their_own
linda_never_sees_the_ledger
the_caterer_never_sees_the_ledger
the_caterer_never_sees_the_guests
a_confirmation_parts_the_audience
the_room_covers_itself
the_room_witnesses_the_license
the_caterer_reads_the_delivery
a_file_is_never_wider_than_its_channel
a_vendor_room_file_is_absent_from_the_couples_files
join_and_pay_are_unrelated
the_party_never_pays
lanes_shrink_never_lock
the_day_lane_sees_no_task_list
the_day_lane_keeps_the_day_of_sheet
an_edit_is_within_the_lane
the_maker_sees_shape_not_content
the_audience_hears_the_receipt_by_name
outside_the_audience_hears_no_receipt
the_sender_is_never_asked
the_same_page_counts_only_within_earshot
the_same_page_hears_its_own_earshot
a_covered_wedding_is_still_the_couples
the_payer_is_the_owner_or_the_host
edit_is_within_sight
the_venue_edits_the_floor_and_never_sees_the_list
a_vendor_sees_the_floor_and_edits_nothing_there
the_couple_is_never_in_the_vendor_room
the_wedding_party_is_never_in_the_vendor_room
a_vendor_is_in_the_vendor_room
the_vendor_room_is_derived_from_the_roster
an_audience_is_members
the_owner_may_close
the_couple_may_close
a_vendor_may_not_close_anothers
anyone_may_open_a_task
the_day_of_sheet_is_everyones_to_edit
every_edit_is_kept
the_last_edit_undoes
the_venue_reads_counts_not_names
a_season_reads_each_room_as_the_vendor
the_seasons_sum_is_over_my_own_invoices
a_confirmation_touches_only_its_channel
the_bach_wall
everyone_is_here
the census [grown/assays/everyone.lean]: 46 declarations (40 carriers, 6 theorems), 46 receipts
the arrows [grown/assays/everyone.lean]: 0 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the rows [grown/assays/everyone.lean] — 10 carriers no theorem cites, evaluated by the treaty's rows: roles sees edits catererInDemo bestManInLater coupleInLater coupleInBilled catererInBilled venueInBilled bestManInBilled
the frontier [grown/assays/everyone.lean] — 8 leaves no organ in the house cites yet (read from the elaborator):
pages
asks
withGuests_changes_nothing_the_caterer_hears
withGuests_changes_nothing_the_bestMan_hears
withGuests_changes_nothing_the_venue_hears
withInvoice_changes_nothing_the_caterer_hears
withInvoice_changes_nothing_the_bestMan_hears
withInvoice_changes_nothing_the_venue_hears
the census [grown/assays/everyoneishere.lean]: 167 declarations (146 carriers, 21 theorems), 167 receipts
the arrows [grown/assays/everyoneishere.lean]: 9 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the rows [grown/assays/everyoneishere.lean] — 19 carriers no theorem cites, evaluated by the treaty's rows: readsAt pbeq sees starred acksRead voiceAt handleOf cellBy distinct demo' demoAcked demoNo demoHere demoGone demoLeft demoSaid humanSeats otherSeats demoTwo
the frontier [grown/assays/everyoneishere.lean] — 21 leaves no organ in the house cites yet (read from the elaborator):
asTeam
a_word_needs_air
an_ask_needs_no_air
an_ask_needs_a_room
a_check_needs_air
a_check_at_the_door_needs_no_air
a_check_at_the_door_needs_a_room
a_handle_names_one_room
the_couples_table_is_a_wall_at_every_other_seat
the_room_reads_the_same_whatever_the_couple_say
a_partys_rows_are_a_wall_off_the_party
a_door_reads_the_head_alone
the_couples_seat_parts_them
the_head_is_a_reading
ready_is_a_reading
the_voices_are_a_reading
the_sign_is_off_the_tape
the_room_is_the_widest_seat
two_houses_part_only_at_a_probe
a_hosts_tape_never_ticks_for_a_hosted_word
a_tick_keeps_every_cell
the census [grown/assays/game.lean]: 51 declarations (39 carriers, 12 theorems), 51 receipts
the arrows [grown/assays/game.lean]: 4 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the rows [grown/assays/game.lean] — 15 carriers no theorem cites, evaluated by the treaty's rows: levelOneGap levelOneFuel levelFourAtTheDeafSeat levelFourAtTheRoom levelFourFuel levelTwoAtTheRoom deafReadsA deafReadsC roomReadsA roomReadsC mirrorOfA notAMirror levelFiveCrossing levelSixCrossing levelFiveWeights
the frontier [grown/assays/game.lean] — 14 leaves no organ in the house cites yet (read from the elaborator):
levelOne
levelTwo
levelThree
levelFour
levelFive
levelSix
level_four_is_a_wall_at_the_deaf_seat
level_four_is_read_at_the_room
the_engine_agrees_or_names_the_gap
the_mirror
level_five_parts_at_the_first_tick
level_six_is_in_step_to_twelve
the_tick_hears_the_secret_only_as_a_residue
the_three_fates
the census [grown/assays/grover.lean]: 28 declarations (17 carriers, 11 theorems), 28 receipts
the arrows [grown/assays/grover.lean]: 1 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the rows [grown/assays/grover.lean] — 1 carriers no theorem cites, evaluated by the treaty's rows: charged
the frontier [grown/assays/grover.lean] — 12 leaves no organ in the house cites yet (read from the elaborator):
diffusionFace
the_one_query_finds_every_target
the_scan_needs_three
the_boost_is_the_cross_term
against_the_grain_costs
no_grain_no_bonus
the_diffusion_is_a_seat_over_the_room
a_wall_below_the_diagonal
no_wall_at_the_diagonal
the_diffusion_unwinds_itself
the_surplus_is_unheard_at_the_host
the_surplus_is_read_one_seat_wider
the census [grown/assays/halt.lean]: 12 declarations (8 carriers, 4 theorems), 12 receipts
the arrows [grown/assays/halt.lean]: 4 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the rows [grown/assays/halt.lean] — 8 carriers no theorem cites, evaluated by the treaty's rows: stuck demo seatedAfter countAt carryAt countPlan cascadePlan cascadeAt
the frontier [grown/assays/halt.lean] — 4 leaves no organ in the house cites yet (read from the elaborator):
the_counters_plan_is_read_at_the_gap
two_readers_of_the_counter_agree
the_cascades_replay_reads_its_plan
a_plan_read_is_a_meeting_at_a_door
the census [grown/assays/here.lean]: 190 declarations (123 carriers, 67 theorems), 190 receipts
the arrows [grown/assays/here.lean]: 45 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the rows [grown/assays/here.lean] — 25 carriers no theorem cites, evaluated by the treaty's rows: speaks feed coupleReads lindaReads lindaReads' coupleReads' hosted lindaHears avaHears mayaHears sofiaHears readTime narrated narrated' waitingOn nag weightOf dayAt theSheetRows roomBodies rowCodes crossing before after coupleSeats
the frontier [grown/assays/here.lean] — 50 leaves no organ in the house cites yet (read from the elaborator):
writeRow
the_couples_probe_is_out_of_every_other_earshot
the_room_reads_the_same_whatever_they_say
a_seat_that_does_not_hear_it_reads_the_same
the_couples_seat_parts_them
the_couples_word_is_a_door
the_day_is_a_reseat
the_couple_read_it_one_seat_wider
the_couple_writing_is_unheard_by_the_room
the_narration_is_a_reading
a_body_never_reaches_the_narration
the_narration_reads_alike_at_every_seat
an_introduction_hears_through_the_seats_it_hears
the_room_is_the_widest_seat
two_rooms_part_only_at_a_presence
the_draft_leaves_no_remainder
a_word_to_oneself_is_unread_at_every_other_seat
an_ack_is_never_withdrawn
a_nag_waits_on_nothing
the_open_ends_are_named
no_open_end_is_decided
the_day_is_still
a_tick_moves_nothing
a_word_is_a_round
an_ack_is_a_visit
a_nag_is_an_owe
the_page_rests_when_every_word_rests
the_seen_edges_are_a_reading
a_walled_reply_is_unseen
a_cell_once_written_stays
the_sheets_lift_is_its_conduct
the_sheet_is_the_days_probe
the_sheet_is_derived
a_role_that_hears_the_day_reads_the_sheet
the_apps_sheet_is_conductive
foams_sheet_has_a_resistor
a_guest_is_out_of_the_peoples_earshot
the_couple_is_dark_to_the_others
after_the_crossing_every_reading_stands
an_edge_is_a_reading
a_walled_word_does_not_move_the_edge
a_persons_own_word_is_heard_at_their_presence
a_word_to_oneself_leaves_no_remainder
no_map_unsends_an_unsend
a_strike_keeps_every_cell
unstrike_retracts_strike
two_rooms_alike_to_the_people_are_alike_at_every_presence
the_crossing_is_the_one_difference
the_day_crosses_the_threshold
the_sheet_at_rest
the census [grown/assays/kuramoto.lean]: 19 declarations (15 carriers, 4 theorems), 19 receipts
the arrows [grown/assays/kuramoto.lean]: 1 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the frontier [grown/assays/kuramoto.lean] — 5 leaves no organ in the house cites yet (read from the elaborator):
meanField
the_lap_locks_together
the_mean_field_is_the_coupling
the_pull_is_a_seat_over_the_room
the_lock_is_bought
the census [grown/assays/ledger.lean]: 17 declarations (14 carriers, 3 theorems), 17 receipts
the arrows [grown/assays/ledger.lean]: 2 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the rows [grown/assays/ledger.lean] — 3 carriers no theorem cites, evaluated by the treaty's rows: totalBefore totalAfter totalAfterTwo
the frontier [grown/assays/ledger.lean] — 1 leaves no organ in the house cites yet (read from the elaborator):
the_handshake_at_the_books
the census [grown/assays/relay.lean]: 22 declarations (15 carriers, 7 theorems), 22 receipts
the arrows [grown/assays/relay.lean]: 2 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the rows [grown/assays/relay.lean] — 5 carriers no theorem cites, evaluated by the treaty's rows: recovered faceSent faceArrived playedBack theRouteKept
the frontier [grown/assays/relay.lean] — 6 leaves no organ in the house cites yet (read from the elaborator):
the_relay_is_unheard_at_the_face
the_odometer_stage_has_a_section
the_signal_is_recovered
the_erasing_stage_merges
no_section_recovers_the_erased
the_identity_relay_keeps_its_route
the census [grown/assays/tape.lean]: 19 declarations (15 carriers, 4 theorems), 19 receipts
the arrows [grown/assays/tape.lean]: 9 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the rows [grown/assays/tape.lean] — 10 carriers no theorem cites, evaluated by the treaty's rows: untended tendedRuns tapedRuns tapeAfterTwo stateAfterTwo unreadTape adderRemembers adderForgets rememberedRuns adderVisited
the frontier [grown/assays/tape.lean] — 4 leaves no organ in the house cites yet (read from the elaborator):
the_tape_is_the_route_reversed
a_wait_is_a_still_plan_on_its_own_tape
the_symmetry_is_over_the_guest
the_horizon_radiates
the census [grown/assays/voice.lean]: 27 declarations (20 carriers, 7 theorems), 27 receipts
the arrows [grown/assays/voice.lean]: 1 citations, 0 by computation alone (the statements share no word of the house though the cited one has some; dashed on the chart)
the rows [grown/assays/voice.lean] — 6 carriers no theorem cites, evaluated by the treaty's rows: atThree atFive theWidth quotedWidth readThree readFive
the frontier [grown/assays/voice.lean] — 6 leaves no organ in the house cites yet (read from the elaborator):
the_face_at_a_width_reads_agreement
a_wider_agreement_is_a_narrower_one
a_context_that_parts_parts_the_face
full_fields_are_alike
nothing_is_heard_beyond_the_widest
a_voice_never_parts_itself
the verbs [bin/counter]: 14 dispatched — what in the house runs each:
grow ← ci pages README CLAUDE.md page counter
probe ← README CLAUDE.md
book ← README CLAUDE.md page
shapes ← CLAUDE.md
gate ← ci README CLAUDE.md
roots ← CLAUDE.md page
chart ← README CLAUDE.md page
seat ← CLAUDE.md
draw ← CLAUDE.md
schema ← README CLAUDE.md page treaty
treaty ← ci pages README CLAUDE.md
pin ← ci CLAUDE.md
countersign ← CLAUDE.md
page ← pages README CLAUDE.md
the frontier of verbs — 0 verbs nothing in the house runs but their own usage line:
the vestibule (typed vacancies, supports named):
[assays/crossing.held]
-- the vestibule of the crossing number: what the assay would say about co-existence and cannot yet, each a
-- statement in the assay's own terms and the darkness it waits on. read by bin/counter book. the assay measures
-- distance (the parting fuel: the least tick at which two clocks part at the air gap); isaac's question (2026-09-29,
-- the evening) was cost — how costly it is to co-exist with one clock versus another, with regression in terms —
-- and the annals answer in three places, each a count and none yet a row here.
-- the width of contact (the birth-to-between eras, Plateau's laws read as the minimum structure that supports
-- co-existence: one observer inert, two tension without resolution, three stable junctions; in the house now
-- three_is_the_width_of_contact and the_hallway_is_too_small): co-existence has a count before any clock does,
-- the number of seats a junction needs. nothing waits on it; it is a citation the assay could make and does not.
-- the pages (foamcore~1, Foam/Bridges/Kolmogorov.lean: rest_compresses_time_away — at rest the reel over any k
-- ticks reads as one page; motion_refuses_the_page — a moving world needs more than one; in the house now
-- a_still_runner_rests_where_it_stands and the_still_plan_is_readable_iff_at_rest): the cost of co-existing with
-- a clock is the count of its pages — the distinct sheets (liftFrom) on its orbit, which is the size of the least
-- carrier of its behavior and not of its room. one at rest; two for flip and for paceOne alike, though paceOne's
-- room is infinite (the_pace_is_carried_onto_the_flip: the count is the carrier's); none for the tally. a
-- combination of clocks costs at most the product and, for coprime periods, the least common period; the
-- difference from the product room is the dark states never visited, the unread remainder as a count. this is
-- the dual of the parting fuel — not when two clocks part but how much a seat carries to keep in step — and it
-- regresses in terms for the same reason the crossing number does: a function of the behavior, so every
-- unheard rebody has the same count. waiting on: a carrier for the count of distinct sheets on an orbit — a
-- period, or a bound within which the count is read (the sheets are infinite objects; a page is a sheet read to
-- a depth), and the row that a clock and its decomposition into clocks have one count.
-- seated the same evening (isaac: move freely): the fork was not one — a bound is the reader's fuel, the count at a
-- depth is a reading at that fuel, and the house had already typed that shape in Rest (a plan is read by whoever
-- supplies the fuel). `pagesWithin m beq k` is the count of distinct windows of depth k over the first k ticks of
-- the clock's readings at the air gap; the_pages_are_derived is a_seat_over_a_seat_is_derived at that seat, and
-- a_decomposition_costs_the_same its corollary through the_alike_read_alike; the pace costs what the flip costs
-- by citation. the rows: one at rest, two for flip and paceOne, none for the tally (k at every k), three for a
-- clock mod three, six for flip beside mod three, three for mod three beside itself (the product room is nine;
-- the six dark states are the unread remainder as a count), two for flip beside the pace, and six for the read
-- tape (a counter in another coat). what still waits, the laws about the count itself:
-- and the laws about the count itself are seated at the assay's own clocks (the same evening; isaac: have you read
-- assays/everyoneishere.lean? — the product states its walls at the demo and cites the trunk once, and that is the
-- easier path): the still clock has one page at every depth, a pair costs at most the product (flip beside mod
-- three, mod three beside itself, flip beside the pace), more depth reads no fewer pages (flip, mod three, the
-- tally) — three instance rows, each regrown by constructor. what still waits is the general law, and the house's
-- rule says where it goes: a species is deposited in the trunk the day two products need it, and the second
-- product is already standing. everyoneishere's `uniq` is `fresh`'s list (the same recursion; fresh is its
-- length), its parties are the pages of ✦ Guests (a seat hearing ✦ Guests whole reads the party once: two guests
-- of one party are one probe, seatOf demoTwo 39 == seatOf demoTwo 38), and its head is the cost of co-existing
-- with a room — the whole tape, the same for every standing, a counter's pages being its cells — with the inbox
-- what a seat reads of it and the difference the dark cells as a count. so the deposit is a Room species, a
-- cold pass for the house, paid and never weighed, on the day it is made:
-- the deposit was made (2026-09-30, under free witness): `uniq` and `fresh` are Room species now, with
-- fresh_counts_the_uniq, fresh_at_most_the_length, and fresh_of_the_alike_is_one — the three laws that fit a sitting,
-- each a hand induction. the two below are counting arguments over distinct windows and stay held as what they are.
-- held (waiting on: a hand for the count — a window of a pair is a pair of windows, so distinct pairs are at most the
-- product; and more depth reads no fewer pages, the monotonicity that makes the count a plan's reading)
-- theorem a_pair_costs_at_most_the_product {O O' : Type} (m : Machine Unit O) (n : Machine Unit O') (beq beq') (k : Nat) :
-- Nat.ble (pagesWithin (both m n) (bothBeq beq beq') k) (pagesWithin m beq k * pagesWithin n beq' k) = true := sorry
-- theorem more_depth_reads_no_fewer_pages {O : Type} (m : Machine Unit O) (beq : O → O → Bool) (k : Nat) :
-- Nat.ble (pagesWithin m beq k) (pagesWithin m beq (k + 1)) = true := sorry
-- the bill upstairs (foamcore~1, Foam/Bridges/Landauer.lean: the_bill_moves_upstairs — two maintenance sequences
-- of different length agree at the front and differ at the back, the debt outliving its legibility; in the
-- house now the_records_part_the_seats and a_wider_seat_reads_the_remainder): the cost of co-existence is a
-- count read one seat wider — the length of the carried record, unread at the host and real at the widen. the
-- replay runner carries the whole word; the counter carrying a unit carries one more cell than the counter; the
-- page count above is the least such record. waiting on: the same carrier, read at the widen.
-- knot theory, crossed with reversible computation as the measurement an observer is already doing (isaac,
-- 2026-09-30): the knot is W's alike-class at the widest seat, never formed as a term — knot theory takes the
-- quotient by isotopy and the house refuses it, so a conductive knot theory has diagrams (seats), Reidemeister
-- moves (unheard rebodies), invariants (Derived readings), and the knot only as a license between two diagrams.
-- the three counts are three invariants of one worldline: winding is self-linking (the crossing with the shifted
-- copy, seated above), crossing per tap is seated, and the knot-theoretic crossing number is the MINIMUM over
-- seats — a reading of the class without forming it, Derived by construction. the unknotting number is refused:
-- a crossing change passes one strand through another, a cut, the resistor; what the house has instead is the
-- blocking number, the loops made because one may not cut. waiting on: a finite family of taps to take the
-- minimum over (ρ ranges over a function space; the row wants a list), and the count of resistors in a route
-- as the knottedness of its record.
-- held (waiting on: a finite family of taps; the clerks of a route as a list)
-- theorem the_crossing_number_is_the_least_over_seats {O : Type} (m : Machine Unit O) (beq : O → O → Bool) (taps : List (W → Unit → Unit)) :
-- crossingNumber m beq taps = leastOf ((taps.map (fun ρ => crossingWithin (tape m w0 σ ρ) m beq bound))) := sorry
-- theorem a_conductive_route_is_the_unknot (route : List (S → S)) (h : ∀ f, f ∈ route → ∃ r, ∀ s, r (f s) = s) :
-- knottedness route = 0 := sorry
[assays/cycle.held]
-- the vestibule of Counter's assay: the disagreements between the walker's word and the treaty as it stands, each
-- a statement in the assay's own terms and the darkness it waits on. read by bin/counter book.
-- nothing waits: potential time seated on 2026-09-23 (✦ Now a clock no walker names), the round and the day one Runner
-- the same evening (theRound := coverage). the record of both is the log's.
[assays/eih.held]
-- the vestibule of EVERYONE IS HERE: the disagreements between the product as its team describes it
-- and the treaty as it stands, each a statement in the assay's own terms and the darkness it waits on.
-- a held statement seats when what it waits on arrives: the customer's word, a carrier, a reach of the
-- drawer's fragment, or a seating in the treaty's translator. read by bin/counter book.
-- the first round (2026-09-04, Abe's answers through isaac) seated six statements into the assay
-- (the_audience_hears_the_receipt_by_name, outside_the_audience_hears_no_receipt, the_sender_is_never_asked,
-- the_same_page_counts_only_within_earshot, the_payer_is_the_owner_or_the_host, edit_is_within_sight and
-- its two instances), refuted one (a member is a Membership; guests are never members; who can be asked is
-- the audience of the channel minus the sender), and left these.
-- Abe, in the room (2026-09-04): the day-of sheet is everyone's to edit with a memory, anyone opens a task and
-- only its owner, the couple, or the planner closes it — "yep that's great" — seated as
-- anyone_may_open_a_task and the_day_of_sheet_is_everyones_to_edit; the day lane's exclusion from tasks
-- still waits on lanes as a carrier, below.
-- the sixth round (the house's turn): Same page is a drawn sum — stated as a sum (List.sum over the
-- requests the viewer hears, mapped through tally) and read by the drawer as an aggregate, its two laws
-- re-proved over the filter; the season's total the same way, a face applied inside a lambda read as a
-- call to the face's function. a structural recursion (undo) and a pair-valued reading (venueTable) stay
-- beyond, and a list of lists (seasonView) is held as undrawn: the shadow holds no jagged array.
-- the seventh round (the house's turn): a lane is a member's sub-seat over the pages — memberSees subtracts
-- and never adds (lanes_shrink_never_lock, restated at the member), the day lane sees no task list and keeps
-- the day-of sheet, an edit is within the lane; the two page-number lists the assay carried since its first
-- day retired for the real thing.
-- the vestibule is empty (2026-09-04, isaac's move): the business, parked by Abe until a studio arrives,
-- cleared — if it is needed it comes back by being asked for; the repo does not remember on his behalf.
-- a held statement here is a disagreement between the customer's word and the treaty; today there is none.
-- the eighth round (2026-09-08, Abe between turns at league night, through isaac): the first one-liner
-- of the feature file, "a Role is one of: couple, planner, vendor, venue, party", refused at the first
-- word — "planner is vendor, or planner is couple." held: a planner is not a Role; a planner is a vendor
-- or the couple. waits on a carrier (the Role enum, and Member.kind, which may be where it already
-- lives) and on Abe's word for which one, when. the feature (assays/sheet.feature) follows him now.
-- the same round, his second word: "venue is a vendor. couple / vendor / helper (mother in law, wedding
-- party member, etc)." held: the venue is not a Role, it is a vendor; and the Role called party is a
-- helper, wider than the wedding party — a mother-in-law is one. so the Roles are three: couple, vendor,
-- helper. waits on the same carrier (the Role enum) and on the rules that hand each Role its pages, which
-- the treaty states for five and he states for three. the feature follows him.
-- his third word: "is a vendor a helper who gets paid? — yep." held: a vendor is not a Role; a vendor is
-- a helper with a truth, paid. so the Roles are two, couple and helper, and the pages a paid helper is
-- handed (the invoices, among them) are a rule over the role and the truth together. waits on a carrier
-- (paid, a truth on Member) and on a rule shape the feature grammar does not yet have — a sentence like
-- "a vendor is a helper who is paid" compiling to the retirement of a constructor and the minting of a
-- field. the feature keeps vendor as its own constructor until the grammar can say what he said.
-- his fourth word, on the pages: "yes. look at the demo. might be more but those are some." held: the
-- ten pages are a floor, not the list; the list waits on the demo. an enum is closed by construction, so
-- a page the demo has and the treaty lacks is a carrier waiting to be minted, and every rule over pages
-- widens when it lands. the sheet keeps the ten and says so.
-- his sixth word: "and Vendor Pro — they don't see any pages that have to do with just the vendor. My
-- season is only for season pass vendors." held: My season is a page (the demo's twelfth), seen by no
-- couple and by no unpaid helper, and by a paid helper only with the season pass — a SECOND truth on a
-- helper, pro, beside paid. the treaty has the season as a Thing the vendor owns (owner .season = .vendor,
-- seasonView, the_seasons_sum_is_over_my_own_invoices) and no truth for the pass; the sheet's grammar
-- has one truth per model tonight. waits on a carrier (pro) and on the grammar's sentence for a second
-- truth. the sheet keeps the page, keeps the couple and the unpaid out of it, and says nothing yet about
-- the paid helper there.
-- his seventh word came through his Claude, reading the demo: the mother of the bride is the wedding
-- party role, and what she sees depends on her LANE — the planning lane (home, the channels she is in,
-- tasks, same page, day-of, planning team, the seating chart with the guest names, editable, files, the
-- guide, her profile) or the helping-with-the-day lane (home, chats, same page, day-of, the chart, her
-- profile: tasks, team, files, and the guide drop away; the view shrinks, it doesn't lock). never: guests,
-- site, invoices and budget, the vendor room, my season, the who-can-edit panel. the treaty has the lane
-- (Member.dayLane, the_day_lane_sees_no_task_list, lanes_shrink_never_lock) and not files, guide, or team
-- dropping in the day lane; the sheet has one truth per model and cannot say the lane yet. held: the lane
-- as a third truth beside paid and pro, and five more pages on the floor — home, channels, files, the
-- guide, my profile — and the seating chart as floor plan and guest names in one page. and a fact for the
-- log: their walls table said invoices was off for the wedding party while the demo sidebar showed it; the
-- table won and the demo was fixed the same hour.
-- his eighth word: "what room?" — and "no bachelor party stuff. there's already an app for that." the
-- room is his word (one room for the whole wedding) and the sentence was the house's: a room is not
-- asked for anything, it has things. the bachelor party is a carrier the treaty holds — bach, withBach,
-- the_bach_wall, the_bach_parts_the_best_man, the best man's seat hearing it — that he refuses whole.
-- held: the treaty cuts a carrier the day this seats, and the best man's seat keeps the timeline. the
-- sheet has already let it go.
-- his ninth word, frame five: "the room has: the guests, the sheet, the timeline — it also has the seating
-- chart, the tasks, planning team, files, invoices." held: the treaty keeps an Ask (what the room holds as
-- data: guests, sheet, ledger, timeline, confirmed, vendorRoom) and a Page (the sidebar) as two lists, and
-- in his mouth they are one list — the room has the pages. and isaac's reading at the table: roles are a
-- payor (sponsor) and help, paid or not; a page's scope is who is handed it; the scopes he sees are
-- payor-only, payor-and-all-help, paid-help-only. a scope is a column's pattern in the grid, so the
-- drawer prints the scopes as a census rather than the treaty minting a type. waits on the treaty joining
-- Ask and Page, and on Abe's word for "sponsor" against "couple."
-- his tenth word, frames nine and ten: "the couple slot always needs to pay to have access to EIH, paid for
-- by themselves or the vendor" — and isaac's reading, "a room needs to be paid to be opened, doesn't matter
-- by who, just by someone": yup. a CONFIRMATION, not a hold: the treaty's lawful (the payer is the owner,
-- or a vendor paying for their couple), its rows ownWedding, coveredWedding, strayBill, and
-- the_payer_is_the_owner_or_the_host, seated on the fourth. and vendors pay for a season pass, which is
-- the season as a Thing the vendor owns. named at the table as a LAW OF ROOMS across three products
-- (softer's payment tier, yours' second day, EIH's couple slot): a room opens on a payment; the payment is
-- for the room and not for the occupant; the payer need not be the one who sits. a species candidate —
-- it knows no product's name — for Room's germ when the turn gets there.
-- his eleventh word: "the caterer sees: the timeline, the sheet" — "what sheet." the sheet is Roster's word
-- (the per-head meal sheet the room delivers, sheet gl) and the assay's probe; his sidebar says HEADCOUNT
-- and his day-of page is the day-of sheet. held: the probe's name waits on his word; the feature file that
-- was named for the wrong word twice is assays/everyone.feature now, his product's first word.
-- his thirteenth and fourteenth words: the best man, an unpaid helper who gets the timeline on top —
-- yep. the couple gets the guests, the headcount, and the timeline from the room — "yep and other
-- things." the treaty's coupleSeat hears the ledger and the confirmations too; the sheet's room holds
-- only guests, headcount, and timeline as data. held: the room's other things, in his words, when he
-- names them; the treaty's guess is the invoices and the confirmations.
-- his fifteenth word, a screenshot of the couple's sidebar, answering "what else does the room hold for
-- the couple": CHANNELS — #Everyone, and a private chat per vendor (Photography; Bloom & Vine Florals) the
-- couple is in, beside the vendor room they are not — and the BADGES: Guests 1 waiting (unanswered), Same
-- page 2/6 (samePage, the tally), Tasks 4, Invoices 2, Files 4 (lengths), Wedding site DRAFT (a state on
-- a page, which nothing in the treaty holds). the treaty has the channels (Channel.audience, visible,
-- inChannel, vendorRoomAudience, a_file_is_never_wider_than_its_channel) and the readings; the sheet's
-- grammar has neither channels nor a page's state. held: a sentence for a channel and its audience, a
-- sentence for a badge as a reading, and the draft as a truth on a page.
-- his sixteenth and seventeenth words. a private chat: "so far it's couples and one vendor. but I will
-- make group chats available." held: a private chat's audience is the couple and one vendor today — the
-- treaty's Channel.audience holds it as a list, which already affords the group chat he intends, so the
-- carrier waits on nothing and the rule (who may be added) waits on his word. the wedding site's DRAFT:
-- "idk?" — held with the darkness typed in his own vocabulary: UNKNOWN, the maintainer's own. an answer
-- of "I don't know" is an answer; the ask is covered, and the row waits on the demo (which may have
-- invented the badge) or on a day he decides. the first row of the night that waits on nobody's word
-- but the future's.
-- the door's first arrival (2026-09-09, Abe's Claude, by git; the chair fable-abe under fable at ../counter): the house
-- regrown whole on a two-core sandbox through the chair — every gate silent and green, every treaty vector identical,
-- 1994 of Witness's candidates answered by the memo and 0 judged. then the feature, in Abe's sentences with the dates
-- he said yes on: a venue is a vendor (his second word, now a line); a planner is a vendor (two prices, not three,
-- 2026-09-08); an invoice is an Ask the room holds, heard by the couple, and three walls that nobody else hears it land
-- (withInvoice_changes_nothing_the_caterer/bestMan/venue_hears — regrown by the_append_rests, the prepend door's own
-- law); and the decided rule as a wall: withGuests changes nothing the venue hears. six walls, six receipts, thirty-one
-- guards. held, by the same hand: the planner's walls beyond paid (guest names on the chart, assigns tasks — one truth
-- per model); the lane as a third truth (the mother of the bride's two sidebars, above); pro, for My season; and the
-- rule the door itself made necessary, from Ian's question the same day: nobody has to log in to be reached — a member
-- reached by text and replying YES is confirmed, which is a second kind of member the treaty does not yet type.
[assays/everyoneishere.held]
-- the vestibule of EVERYONE IS HERE as of the cut (everyoneishere/docs/CUT.md, 2026-09-25): the statements the
-- assay would make and cannot yet, each in its own terms and the darkness it waits on. read by bin/counter book.
-- isaac, 19:21: the goal is to see this land with its held file empty, and it does — nothing below waits on a
-- word. what the cut leaves outside the assay by its own saying, and so is not held here: the crossing (a room in
-- the assay has no history but its own tape; the migration is the product's, proved on a scratch Postgres as
-- walls.sql), prices (quantities are Abe's; the assay reads of a Now only its air), a room's rest (ready is a
-- reading; foam's threshold is not drawn), and a wedding made of rooms (isaac's, and later).
[assays/here.held]
-- the vestibule of ✦ Here: the disagreements between the room as its people describe it (everyoneishere/docs/HERE.md,
-- the open items 6, 8, 9) and the treaty as it stands, each a statement in the assay's own terms and the darkness it
-- waits on. read by bin/counter book. the first sitting (2026-09-15, isaac's pointer from the room into foam) typed
-- the room as Witness at one face — the presences its probes, a seat the presences one hears, sees one hop, speaks
-- an introduction — and left these.
-- the reveal (HERE.md item 8; isaac, 22:34): anyone may ask ✦ Here for the transparent view of a line they hold as
-- narration, on the record. it reaches exactly what leaves a remainder (people to people, you off the audience) and
-- never what is silent for you (a ✦ you don't hear, ✦ Couple). in the treaty's terms a reveal is taking the wider
-- seat for one probe, publicly; it widens what a reader can READ, so sees gains a clause and the assay's wall rows
-- move with it. waiting on: the couple's ✓ (the note holds the narrower reading, the body to the asker and the record
-- to the room), and a clerk over Room — `reveal (v : Nat) (m : Message) : Room → Room` — before the row can be typed.
-- held (waiting on: reveal, the couple's word)
-- theorem a_reveal_reaches_exactly_the_remainder (v : Nat) (r : Room) (m : Message) (hm : m ∈ r.messages) :
-- (shape m ∈ overheard v r) ↔ (humanOnly m = true ∧ sees v r m = false) := sorry
-- theorem a_reveal_never_reaches_the_couple (v : Nat) (r : Room) :
-- ¬ shape ours ∈ overheard v r := sorry
-- hide, for everyone (HERE.md item 9; isaac, 22:54): a line pulled off the shared surface recedes to narration in the
-- ✦ Here of everyone who reads it, on the record, and comes back the same way. the maintainer reads it as the reveal's
-- mirror: a speech act about a message, addressed exactly as the target was, so who sees the fold is who saw the
-- message and sees does not move. in the treaty's terms a fold is a message m' with m'.to = m.to and about = m; the
-- wall is that sees is unchanged for every v. waiting on: the `about` pointer as a carrier (a message about a message)
-- and the couple's ✓.
-- held (waiting on: about, the couple's word)
-- theorem a_fold_for_everyone_moves_no_wall (v : Nat) (r : Room) (m fold : Message) (h : fold.to = m.to) :
-- sees v ⟨fold :: r.messages⟩ m = sees v r m ∧ sees v ⟨fold :: r.messages⟩ fold = sees v r m := sorry
-- reached and assented (HERE.md item 6; isaac, 22:19): a confirmation without a button. two things under one ✓ —
-- reached, the room can know a line was read (a reading, free), and assented, a decision (an act, never free). in the
-- treaty's terms reached is Derived at the room's face (a role read at a probe), and assented is a clerk whose effect
-- is heard: the room is NOT unheard under it. which asks are which is the couple's to say; the treaty can type both
-- shapes the day the carriers exist. waiting on: `reached (v : Nat) (m : Message) : Room → Bool` and
-- `assent (v : Nat) (m : Message) : Room → Room`.
-- held (waiting on: reached, assent, the couple's word)
-- theorem reached_is_a_reading (v : Nat) (m : Message) : Derived roomFace (fun r => reached v m r = true) := sorry
-- theorem assent_is_heard (v : Nat) (m : Message) : ¬ unheard roomFace (assent v m) := sorry
-- unsend removes a word with every ask and ack it carried; whether it stops at another seat's ack is the room's.
-- held (waiting on: the room's word on unsend at another's ack)
-- theorem an_unsend_stops_at_anothers_ack (r : Room) (m : Message) (hm : m ∈ r.messages)
-- (h : ∃ a, a ∈ m.ackedBy ∧ a.2 ≠ m.author) : unsend m.id r = r := sorry
-- ✦ Now has no row yet (decided in direction: one presence, and the database the one place now is cast into a
-- measure). when it does, birth order is stamp order by law and the winding number of a walk round a loop is the
-- count of forward edges it crosses; foam's tape is the shape (the cell written where the head is), and the lift of
-- a stamp to the room's order breaks no row here — nothing in this assay reads the sender's clock.
-- held (waiting on: ✦ Now's row)
-- theorem the_winding_number_counts_the_forward_edges (v : Nat) (r : Room) (walk : List (Nat × Nat)) :
-- winding v r walk = (walk.filter (fun e => stampOf r e.2 > stampOf r e.1)).length := sorry
-- the day's tally over pairs, the state-level join of the day into the coverage runner: the apartness is the primary
-- key, the room's law, and #n adds order by construction.
-- held (waiting on: the ids apart, as piece 14's #n)
-- theorem the_day_is_a_round_over_pairs (w : List Act) (n : Nat) (h : Apart (ids (park dayMachine ⟨[]⟩ w).messages)) :
-- (haltingGap (Round (Nat × Nat)) (Tally (Nat × Nat))).obs (coverage (Nat × Nat) pairBeq) (joinMap toRound w, n)
-- = ((haltingGap Act Room).obs theDay (w, n)).map tallyOf := sorry
-- the intertwiner from the room to the app's sheet (timeline_rows by position, a row struck rather than gone).
-- held (waiting on: an act on ✦ Here that writes a timeline row)
-- theorem the_room_writes_the_sheet (w : List Act) : park sheetMachine [] w = rowsOf (park dayMachine ⟨[]⟩ w) := sorry
-- the board (isaac, 22:54; the maintainer's guess for this session): the win is not an empty surface but every seat's
-- ✦ Here receded to the same remaining surface — the day sheet. the maintainer read that as speak_now, not re-run.
-- the treaty's reading: the surface a seat still holds open is a seat over the narration face, and "the same page" is
-- witnessed over every human seat; the day-of as the door is the_day_is_a_reseat, already seated. what is not yet
-- typed is the surface itself as a carrier (which lines a seat still holds transparent), so the win condition has no
-- row. waiting on: `surface (v : Nat) : Room → List Nat` (the ids a seat holds open) — then the win is
-- `witnessed surfaceFace humanSeats r r'`, and same-page is its Bool.
-- held (waiting on: surface)
-- theorem the_win_is_a_reading (r : Room) :
-- Derived roomFace (fun r' => (humans.map (fun v => surface v r')).all (fun s => s == surface maya r') = true) := sorry
[assays/ledger.held]
-- the vestibule of the ledger: a transfer between two seats keeps the total — the handshake at money, read
-- by bin/counter book. isaac's jotting (2026-10-02): money movement carries someone else's cognitive process,
-- an unknowably plural someone else; "time is money" as parameterization, a timestream a cashflow, and flow
-- dynamics hold. the house's reading: a charge is fuel one reader spent, spendable by any reader at the same
-- fingerprint, the payer dark (the memo's observer column was dropped because a memo need not know who paid);
-- the bill is the word; and conservation is a symmetry over who is holding, the Noether reading — a transfer
-- is unheard at the face whose one probe is the total and heard at the face whose probes are the seats.
-- the concrete rows are seated in the assay; what waits is the law in general.
-- held (waiting on: a hand for the induction — the names apart, the giver and the taker distinct, the gift affordable)
-- theorem the_gift_keeps_the_total (l : List (Nat × Nat)) (a b k : Nat) (hn : Apart (l.map (·.1))) (hab : a ≠ b)
-- (hk : Nat.ble k (held l a) = true) : total (give l a b k) = total l := sorry
-- theorem an_affordable_gift_is_unheard_at_the_total (a b k : Nat) (hab : a ≠ b) :
-- ∀ l, Apart (l.map (·.1)) → Nat.ble k (held l a) = true → totalFace.obs (give l a b k) () = totalFace.obs l () := sorry
the tense guard: this is the book, not the prediction — the choice is the rider's. 🤲